The occupied outer image costs K1rT, not HK1rT or K1r*T². Every carrier below is the existing coprime fiber of an actual dyadic subset.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_outer_image_card {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S T : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) (hT : 0 ≤ T) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) (c : Finset (ℕ × ℕ)) : ↑(Finset.image wCorrelationOuter (wCoprimeFiber x N S U c)).card ≤ 8 * 2 ^ j 1 * 2 ^ j 3 * T

A bound on the image, not on the frequency-tuples projecting onto it.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_outerMass_fixedOrder (k m : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (x η R S T : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, 0 < n) → (∀ q ∈ Q, 0 < q) → (∀ n ∈ N, ↑n ≤ X) → (∀ q ∈ Q, ↑q ≤ X) → 0 ≤ R → 0 ≤ S → R ≤ X → S ≤ X → 0 ≤ T → (∀ n ∈ N, ↑n ≤ 2 * T) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau m) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau m) n)) → U ⊆ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive → wCorrelationOuterMass x N S U c K (betaClean β a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ≤ (C * X ^ δ) ^ 6 * (8 * 2 ^ j 1 * 2 ^ j 3 * T)

Fixed-order payment on the literal outer image of the original carrier.