noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal (N : ℕ) (ε z b c : ℝ) : ℤ

Exact good cross count after grouping by its true product coefficient.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductPrimeTotal N ε z b c = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductSupport N z b c, ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ProductCoefficient N z b c m) * ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11ProductFirstPrimeFiber N ε z m).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_roughSum_le_productPrime_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 0 ≤ ε → ∀ (b c : ℝ), ↑(∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) b c, goldbachG11RoughCount N ε v) ≤ ↑(goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) b c) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

An additional, explicitly paid exception budget for the good-body switch. Only the bad part is enlarged; the surviving product sum remains on the cross.