Local bounds for the secondary terms, retaining the long-interval fractions.

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

inclusive grid endpoint must be paid, not discarded.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_count (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : wGramSecondaryBaseCountBound K F j = 8 * 2 ^ j 0 * 2 ^ j 2 * ↑(F / K.1.1) ^ 2 * 2 ^ j 4 * (1 + Real.log (2 * 2 ^ j 0))

Actual ratio count is H s log(2H), with both independent beta supports.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPaySecondary_envelope {κ δ C Cτ : ℝ} (hκ : 0 ≤ κ) (hC : 0 ≤ C) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (F : ℕ) (j cap : Fin 5 → ℕ) : wGramSecondaryScaleEnvelope κ δ C Cτ a R S K F j cap ≤ C * ↑a.natAbs.divisors.card * (↑K.D' + 2 * 2 ^ j 1 / (2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4)) * (16 * 2 ^ j 2 * 2 ^ j 3 * 2 ^ j 4 * 2 ^ j 4) ^ (1 / 2 + κ) * (2 * 2 ^ j 3 * √(8 * 2 ^ j 2 * 2 ^ j 4 * 2 ^ j 4 * (Cτ * ↑(wGramSecondaryNumeratorMax a K F j) ^ δ)))

Both natural subtraction and the exact lower q=nrs² are respected.