theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKMain_bound (Cscale κ δ ρ η Cnonzero Cτ Cjoint Ca Ccoeff Couter : ℝ) (hscale : 1 ≤ Cscale) (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| ≤ Cscale * 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 * Cscale ^ (2 * δ))) * x ^ (100 * (κ + δ + ρ + η)) * (T ^ (5 / 4) * R ^ (7 / 4) * S ^ 2 / x)

Pointwise main payment on the actual nonempty retained block. The fixed arithmetic multiplier does not change the floor, mask, key box or physical x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayKMain_uniform (Cscale κ δ ρ η Cnonzero Cτ Cjoint Ca Ccoeff Couter : ℝ) (hscale : 1 ≤ Cscale) (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| ≤ Cscale * 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 for a fixed arithmetic multiplier. 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.