theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayZero_square {ε ρ Czero Ccoeff Couter x T Z R S : ℝ} (hCz : 0 ≤ Czero) (_hCc : 0 ≤ Ccoeff) (hCo : 0 ≤ Couter) (hx : 0 < x) (hT : 0 < T) (hZ : 0 ≤ Z) (hR : 0 ≤ R) (hS : 0 ≤ S) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (hD : 0 < K.D) (hF : ↑F ≤ 2 * T) (hn : 2 ^ j 2 ≤ 2 * T) (hk : 2 ^ j 1 ≤ R * S) (hr : 2 ^ j 3 ≤ R) (hfreq : 2 ^ j 0 ≤ 32 * (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) * Z * T / x) : (wBlockAmplitude K j * √(directJoinedMass ρ Couter x T j) * √(directJoinedZero ε ρ Czero Ccoeff x K F j) / T ^ 2) ^ 2 ≤ 1024 * (Ccoeff ^ 4 * Couter * Czero) * x ^ (5 * ρ) * wGramResonanceScaleEnvelope K F j ε * Z * (R ^ 2 * S / x)

Literal mass and zero term, with all local geometry paid before taking roots.