noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassGood (N : ℕ) (ε : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassGood N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | ¬r ∣ N}.card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassBad (N : ℕ) (ε : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassBad N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12ActiveProductSupport N, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | r ∣ N}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WindowWeightSum_eq_good_add_bad (N : ℕ) (ε : ℝ) : ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11LinkedPrimeWindow N ε m).card = goldbachG12MainMassGood N ε + goldbachG12MainMassBad N ε

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient_mul_four_hundred (N m : ℕ) : 400 * goldbachG12NormalizedCoefficient N m = ↑(goldbachG12ProductCoefficient N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) m)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMass_window_data {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG12ActiveProductSupport N) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε m) : Nat.Prime r ∧ ↑N ^ (4 / 53) ≤ ↑r ∧ r ≤ m.minFac ∧ r * m ≤ N

Closed upper product and prime-coordinate bounds of the actual relaxed window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMass_good_pair_mem {N r : ℕ} {ε : ℝ} {u : GoldbachG11SwitchedBody} (hu : u ∈ goldbachG12GoodCrossBodies N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) (hm : goldbachG11SwitchedBodyProd u ∈ goldbachG12ActiveProductSupport N) (hr : r ∈ goldbachG11LinkedPrimeWindow N ε (goldbachG11SwitchedBodyProd u)) (hrN : ¬r ∣ N) : ⟨u.fst, ⟨u.snd.fst, ⟨r, u.snd.snd.fst⟩⟩⟩ ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)) ∧ u.snd.snd.snd ∈ LiLiuPrereqBuchstab.roughNumbers (↑N / ↑(goldbachG11LabelProd ⟨u.fst, ⟨u.snd.fst, ⟨r, u.snd.snd.fst⟩⟩⟩)) ↑u.snd.snd.fst

The coordinate permutation lands on the original cross, not the larger G11 domain.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassGood_le_fullRough (N : ℕ) (ε : ℝ) : 400 * goldbachG12MainMassGood N ε ≤ goldbachG12FullRoughMass N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12MainMassBad_le {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : goldbachG12MainMassBad N ε ≤ 21 * ↑N / ↑N ^ (4 / 53)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WindowWeightSum_le_fullRough {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11LinkedPrimeWindow N ε m).card ≤ goldbachG12FullRoughMass N + 8400 * ↑N / ↑N ^ (4 / 53)

The lower window endpoint is discarded only for an upper bound. The exceptional prime divisors of N are paid separately.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12WindowWeightSum_le_buchstab (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (ε : ℝ), 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11LinkedPrimeWindow N ε m).card ≤ goldbachG12BuchstabUpperMass N η + 8400 * ↑N / ↑N ^ (4 / 53)

The same cross mother now has the uniform Buchstab upper mass. This still precedes the output-prime sieve, which supplies another logarithm.