theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryCenter_eq_density (N : ℕ) (S : Finset ℕ) (L U : ℝ) (d : ℕ) : goldbachG11OrdinaryCenter N S L U d = ∑ m ∈ S, ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * (Wu2004MeanValue.realPrimeCount U - Wu2004MeanValue.realPrimeCount L) * (LiLiuPrereqWF.progressionDensity m) d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryCenter_externalDensity (N : ℕ) (S P : Finset ℕ) (L U D θ z : ℝ) : ∑ t ∈ LiLiuPrereqWF.externalTags true P D θ z, ∑ d ∈ (P.prod id).divisors, (LiLiuPrereqWF.externalTerm true P D θ z t) d * goldbachG11OrdinaryCenter N S L U d = ∑ m ∈ S, ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * (Wu2004MeanValue.realPrimeCount U - Wu2004MeanValue.realPrimeCount L) * LiLiuPrereqWF.externalDensity true P D θ z (LiLiuPrereqWF.progressionDensity m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGrid_sifted_upper {N : ℕ} {ε ρ Q θ z : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hPN : ∀ p ∈ P, p.Coprime N) (hQ : 1 ≤ Q) (hD : 2 ≤ LiLiuPrereqWF.externalInternalLevel Q θ) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hcut : ∀ p ∈ P, ↑p < z) : goldbachG11AllPrimeSiftedMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) P ≤ ∑ m ∈ goldbachG11GridLong N ε ρ k, ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * (Wu2004MeanValue.realPrimeCount (goldbachG11GridProfileHi ρ k) - Wu2004MeanValue.realPrimeCount (goldbachG11GridProfileLo N ρ k)) * LiLiuPrereqWF.externalDensity true P (LiLiuPrereqWF.externalInternalLevel Q θ) θ z (LiLiuPrereqWF.progressionDensity m) + Real.exp (8 * θ⁻¹ ^ 3) * ∑ d ∈ goldbachG11LinkedModuli N ⌊Q⌋₊, |goldbachG11OrdinaryRectangleResidual N ε ρ k d N|

The genuine high-band all-prime sieve envelope. Its error is paired only on squarefree reduced moduli; the main term is the ordinary pi-centered one.