theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_span (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) : ↑(wKSectionGridUpper R S K j cap + 1) ≤ 2 * 2 ^ j 1

The literal inclusive upper endpoint, not an interval assumption on a mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_modulus (j : Fin 5 → ℕ) : ↑(2 ^ (j 2 + 1) * (2 ^ (j 3 + 1) - 1) * 2 ^ (j 4 + 1) * 2 ^ (j 4 + 1)) ≤ 16 * 2 ^ j 2 * 2 ^ j 3 * (2 ^ j 4) ^ 2

True upper modulus used by the main completion factor.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_mean_identity {N m s H A B L : ℝ} (hN : 0 ≤ N) (_hm : 0 ≤ m) (_hs : 0 ≤ s) (_hH : 0 ≤ H) (hA : 0 ≤ A) (_hB : 0 ≤ B) (hL : 0 ≤ L) : √(N * m ^ 2 * s ^ 2 * H ^ 2 * (A * L)) * √(N * m ^ 2 * H ^ 2 * (B * s ^ 2 * L)) = N * m ^ 2 * s ^ 2 * H ^ 2 * √(A * B) * L

Exact square-root arithmetic identity used for the actual joint mean.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayMain_mean_eq (δ Cτ Cjoint : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (hCτ : 0 ≤ Cτ) (hCjoint : 0 ≤ Cjoint) : wGramMainJointMean δ Cτ Cjoint a K F j = ↑(2 ^ (j 3 + 1) - 1) * (2 ^ (j 2 + 1) * ↑(F / K.1.1) ^ 2 * (2 ^ (j 4 + 1)) ^ 2 * (2 ^ j 0) ^ 2 * √(Cτ * Cjoint) * ↑(mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ^ δ * √(1 + Real.log (2 ^ (j 4 + 1))))

No sum remains, and the genuine logarithm and arithmetic maximum remain explicit.