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

The genuine full-prefix Li weight, with no lower-endpoint subtraction.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight N m = MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑m)

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

The full-prefix mass on the actual closed C10 product support.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass N = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight N m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass_eq_pair_sum (N : ℕ) : goldbachB9PlusMainMass N = ∑ rs ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), LiuWeight.liuLogarithmicIntegral (2 / Real.log 2) (↑N / ↑(goldbachC10Prod rs))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9ProductSupport_bounds {N m : ℕ} (hN : 2 ≤ N) (hm : m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) : 0 < m ∧ ↑m ≤ ↑N ^ (2 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑N / ↑m

The closed gamma = 1/3 endpoint uses only the generic S4 product geometry.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight_bounds_eventually : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ m ∈ goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)), 2 ≤ ↑N / ↑m ∧ 0 ≤ goldbachB9PlusLiWeight N m ∧ |goldbachB9PlusLiWeight N m| ≤ 2 * ↑N / ↑m

One threshold works for every member of the actual support; the fixed weight constant is T = 2. Positivity comes from the genuine Li lower bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass_nonneg_eventually : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 0 ≤ goldbachB9PlusMainMass N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight_sum_gateLoss_le_logCube : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d ≤ 4 * 2 * ↑N / ↑N ^ (4 / 53) * (1 + Real.log ↑N) ^ 3

The real non-coprime gate is paid, not identified with zero. The generic budget receives T * N = 2 * N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight_sum_gateLoss_log_saving_one (U : ℝ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d ≤ ↑N / Real.log ↑N ^ U

Every real log exponent is absorbed, with fixed payment constant C = 1 and a threshold chosen before the modulus cutoff Q.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight_sum_gateLoss_log_saving (U : ℝ) (_hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ Q ≤ N, ∑ d ∈ Finset.Icc 1 Q, gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d ≤ C * ↑N / Real.log ↑N ^ U