theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayZero_n_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ T : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a P R S ξ b K) j positive) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) : 2 ^ j 2 ≤ 2 * T

The first beta scale is bounded using its own original support member.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directPayZero_scalar {D k r s H n f T x Z R S : ℝ} (hD : 1 ≤ D) (hk : 0 < k) (hr : 0 < r) (hs : 0 < s) (hH : 0 ≤ H) (_hn : 0 ≤ n) (hf : 0 ≤ f) (hT : 0 < T) (hx : 0 < x) (hZ : 0 ≤ Z) (hR : 0 ≤ R) (hS : 0 ≤ S) (hfreq : H ≤ 32 * (D * k * r * s) * Z * T / x) (hnT : n ≤ 2 * T) (hfT : f ≤ 2 * T) (hkRS : k ≤ R * S) (hrR : r ≤ R) : (D * k * r * s)⁻¹ ^ 2 * (8 * k * r * T) * (k * (r * n * H * f * s)) / (T ^ 2) ^ 2 ≤ 1024 * Z * (R ^ 2 * S / x)

Pure scalar cancellation; hypotheses are the local geometric coordinates.