theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9ProgressionDensity_upper : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (η : ℝ), 0 < η → η < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (Q : ℝ), Q₀ ≤ Q → ∀ (v : ℕ) (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p ∧ 2 < p) → ∀ (z : ℝ), 2 ≤ z → z ≤ Q ^ 2 → (∀ p ∈ P, ↑p < z) → LiLiuPrereqWF.externalDensity true P (LiLiuPrereqWF.externalInternalLevel Q η) η z (LiLiuPrereqWF.progressionDensity v) ≤ (∏ p ∈ P, (1 - (LiLiuPrereqWF.progressionDensity v) p)) * (JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log z) + C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))))

The actual progression density enters the extended upper theorem with a single dimension constant selected before all products and carriers.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SievePrimes_odd {N : ℕ} (hEven : Even N) (z : ℝ) (p : ℕ) : p ∈ fouvryG9SievePrimes N z → Nat.Prime p ∧ 2 < p

Evenness removes the prime 2 from the literal sieve carrier.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g9WF_sqrt_cutoff {N T δ : ℝ} (hN : 4 ≤ N) (hT : 1 ≤ T) (hTu : T ≤ N ^ (1 / 10)) (hδ : 0 ≤ δ) (hδu : δ < 1 / 4) : 2 ≤ √N ∧ √N ≤ (N ^ (5 / 9 - δ) / T ^ (5 / 9)) ^ 2

The actual sqrt(N) cutoff lies in the extended, not necessarily old, domain.