noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryCenter (N : ℕ) (S : Finset ℕ) (L U : ℝ) (d : ℕ) : ℝ

The ordinary source's literal pi-centered main term. Only the long coefficient is filtered by coprimality with d; no short-prime gate is invented.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryCenter N S L U d = ∑ m ∈ S, if m.Coprime d then ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m) * ((Wu2004MeanValue.realPrimeCount U - Wu2004MeanValue.realPrimeCount L) / ↑d.totient) else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryDivCount_centered (N d : ℕ) (S : Finset ℕ) (L U : ℝ) (hS : ∀ m ∈ S, 0 < m) (hL : 0 ≤ L) (hLU : L ≤ U) (hNd : N.Coprime d) : LiLiuPrereqWF.weightedDivCount (S ×ˢ AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWInterval L U) (fun (v : ℕ × ℕ) => (↑N - ↑v.1 * ↑v.2).natAbs) (goldbachG11AllPrimeWeight N) d - goldbachG11OrdinaryCenter N S L U d = Wu2004MeanValue.primeCenteredAPSum S (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (x : ℕ) => U) d N - Wu2004MeanValue.primeCenteredAPSum S (fun (m : ℕ) => ↑(goldbachG11ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) m)) (fun (x : ℕ) => L) d N

Exact actual divisibility count minus the original prime-count main term is the two-prefix residual. Inverse residues, zero and negative overhang survive.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11OrdinaryGrid_centered_eq {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) (d : ℕ) (hNd : N.Coprime d) : LiLiuPrereqWF.weightedDivCount (goldbachG11GridLong N ε ρ k ×ˢ goldbachG11GridShort N ρ k) (fun (v : ℕ × ℕ) => (↑N - ↑v.1 * ↑v.2).natAbs) (goldbachG11AllPrimeWeight N) d - goldbachG11OrdinaryCenter N (goldbachG11GridLong N ε ρ k) (goldbachG11GridProfileLo N ρ k) (goldbachG11GridProfileHi ρ k) d = goldbachG11OrdinaryRectangleResidual N ε ρ k d N

Specialize the exact identity to the same occupied G11 grid consumed by ordinary distribution; there is no conditional count or residue adapter left.