theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_global_square {C L x T R S ρ p η : ℝ} (hC : 0 ≤ C) (hL : 0 ≤ L) (hx : 0 < x) (hT : 0 ≤ T) (hR : 0 ≤ R) : 25165824 * (C * x ^ ρ) * (L * x ^ p) * (x ^ η) ^ 7 * T ^ (5 / 2) * R ^ (7 / 2) * S ^ 4 / x ^ 2 = (√(25165824 * C * L) * x ^ ((ρ + p + 7 * η) / 2) * (T ^ (5 / 4) * R ^ (7 / 4) * S ^ 2 / x)) ^ 2

Exact exponent bookkeeping for the squared, normalized main contribution.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_bound (κ δ ρ η Cnonzero Cτ Cjoint Ca Ccoeff Couter : ℝ) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hη1 : η ≤ 1) (hC : 0 ≤ Cnonzero) (hCτ : 0 ≤ Cτ) (hCjoint : 0 ≤ Cjoint) (hCa : 0 ≤ Ca) (hCo : 0 ≤ Couter) {x M T R S : ℝ} (hx : 4 ≤ x) (hM : 1 ≤ M) (hT : 1 ≤ T) (hxMT : x = 4 * M * T) (hR : 1 ≤ R) (hS : 1 ≤ S) (hRS : R * S ≤ x) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) (a : ℤ) (ha : |↑a| ≤ x) (F : ℕ) (hF : ↑F ≤ 2 * T) {b : ℕ} {K : WExtractedKey} (hK : K ∈ wExtractedKeyBox (x ^ η)) (j cap : Fin 5 → ℕ) {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) : wBlockAmplitude K j * √(directJoinedMass ρ Couter x T j) * √(directJoinedMain κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a R S K F j cap) / T ^ 2 ≤ √(25165824 * Couter * directPayMainLossConstant κ δ Cnonzero Cτ Cjoint Ca Ccoeff) * x ^ (100 * (κ + δ + ρ + η)) * (T ^ (5 / 4) * R ^ (7 / 4) * S ^ 2 / x)

Pointwise main payment on the actual nonempty retained block. The squared proof keeps and pays the span/q summand before global enlargement.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_uniform (κ δ ρ η Cnonzero Cτ Cjoint Ca Ccoeff Couter : ℝ) (hκ : 0 ≤ κ) (hδ : 0 < δ) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hη1 : η ≤ 1) (hC : 0 ≤ Cnonzero) (hCτ : 0 ≤ Cτ) (hCjoint : 0 ≤ Cjoint) (hCa : 0 ≤ Ca) (hCo : 0 ≤ Couter) : ∃ (C : ℝ), 0 < C ∧ ∀ (x M T R S : ℝ), 4 ≤ x → 1 ≤ M → 1 ≤ T → x = 4 * M * T → 1 ≤ R → 1 ≤ S → R * S ≤ x → ∀ (N : Finset ℕ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ 2 * T) → ∀ (a : ℤ), |↑a| ≤ x → ∀ (F : ℕ), ↑F ≤ 2 * T → ∀ (b : ℕ), ∀ K ∈ wExtractedKeyBox (x ^ η), ∀ (j cap : Fin 5 → ℕ) (positive : Bool), ∀ t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M (x ^ η)) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive, wBlockAmplitude K j * √(directJoinedMass ρ Couter x T j) * √(directJoinedMain κ δ ρ Cnonzero Cτ Cjoint Ca Ccoeff x a R S K F j cap) / T ^ 2 ≤ C * x ^ (100 * (κ + δ + ρ + η)) * (T ^ (5 / 4) * R ^ (7 / 4) * S ^ 2 / x)

Uniform actual main-term bound. The positive constant is chosen before all varying scales, arithmetic inputs, finite sets, keys, and block witnesses. No energy, mass, logarithmic, or target-envelope assumption is present.