theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayZero_uniform (ε ρ η Czero Ccoeff Couter : ℝ) (hε : 0 ≤ ε) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hη1 : η ≤ 1) (hCz : 0 ≤ Czero) (hCc : 0 ≤ Ccoeff) (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 ℕ) (a : ℤ) (b : ℕ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (positive : Bool) (t : WExtractedTuple × ℤ), (∀ n ∈ N, 0 < n) → (∀ n ∈ N, ↑n ≤ 2 * T) → ↑F ≤ 2 * T → K ∈ wExtractedKeyBox (x ^ η) → 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) * √(directJoinedZero ε ρ Czero Ccoeff x K F j) / T ^ 2 ≤ C * x ^ (100 * (ε + ρ + η)) * (R * √S / √x)

Uniform payment of the actual joined zero contribution. The constant precedes all varying data. Neither energy nor mass nor a target-sized envelope is an input.