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

The full positive rough mother, with actual prime labels and no output-prime filter.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FullRoughMass N = ∑ v ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ↑(LiLiuPrereqBuchstab.roughCount (↑N / ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LabelProd v)) ↑v.snd.snd.snd)

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MainMassGood N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | ¬r ∣ N}.card

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MainMassBad N ε = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductSupport N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EffectiveProductCoefficient N ε m * ↑{r ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LinkedPrimeWindow N ε m | r ∣ N}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11FullRoughMass_nonneg (N : ℕ) : 0 ≤ goldbachG11FullRoughMass N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass_eq_good_add_bad (N : ℕ) (ε : ℝ) : goldbachG11PrimeWindowMainMass N ε = goldbachG11MainMassGood N ε + goldbachG11MainMassBad N ε

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MainMass_window_data {N m r : ℕ} {ε : ℝ} (hm : m ∈ goldbachG11EffectiveProductSupport 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.goldbachG11_largePrimeDivisors_card_le_twenty_one {N : ℕ} (hN : 4 ≤ N) : (largePrimeDivisors N (↑N ^ (4 / 53))).card ≤ 21

Remove one prime divisor before applying the existing strict n < N bound.

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

Coordinate permutation retains every body label and its positive rough cofactor.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MainMassGood_le_fullRough (N : ℕ) (ε : ℝ) : 400 * goldbachG11MainMassGood N ε ≤ goldbachG11FullRoughMass N

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeWindowMainMass_le_fullRough {N : ℕ} (hN : 4 ≤ N) (ε : ℝ) : 400 * goldbachG11PrimeWindowMainMass N ε ≤ goldbachG11FullRoughMass 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.