@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB9CommonRemainder (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachB9CommonRemainder P = Classical.propDecidable P

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

The common mass is the genuine full Li prefix, not the old B10 endpoint difference.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusCommonRemainder N d = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDivCount N d) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass N / ↑d.totient

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDeletedMain N d = ∑ m ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) with ¬m.Coprime d, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusLiWeight N m

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusMainMass_eq_gated_add_deleted (N d : ℕ) : goldbachB9PlusMainMass N = goldbachB9PlusGatedMainMass N d + goldbachB9PlusDeletedMain N d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusCommonRemainder_eq_gated_sub_deleted (N d : ℕ) : goldbachB9PlusCommonRemainder N d = goldbachB9PlusGatedRemainder N d - goldbachB9PlusDeletedMain N d / ↑d.totient

The deleted main term has a negative sign and is not discarded.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDeletedMain_one (N : ℕ) : goldbachB9PlusDeletedMain N 1 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusCommonRemainder_one (N : ℕ) : goldbachB9PlusCommonRemainder N 1 = goldbachB9PlusGatedRemainder N 1

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusDeletedMain_div_abs_eq_gateLoss (N d : ℕ) : |goldbachB9PlusDeletedMain N d / ↑d.totient| = gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.abs_goldbachB9PlusCommonRemainder_le (N d : ℕ) : |goldbachB9PlusCommonRemainder N d| ≤ |goldbachB9PlusGatedRemainder N d| + gateLoss N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (goldbachB9PlusLiWeight N) d

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusCommonRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d.Coprime N, |goldbachB9PlusCommonRemainder N d| ≤ C * ↑N / Real.log ↑N ^ U

B and the threshold precede N; the gate budget is consumed only after proving D <= N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_rem_eq_commonRemainder {N d : ℕ} (hEven : Even N) {Z : ℝ} (hd : d ∣ goldbachB10ProdPrimes N Z) : BoundingSieve.rem d = goldbachB9PlusCommonRemainder N d

Only the production squarefree sieve-divisor identification of nu is used. There is no restriction comparing Z with either prime factor of m.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_remainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z : ℝ), ∑ d ∈ Finset.Icc 1 (LiuWeight.panModulusCutoff N B) with d ∣ goldbachB10ProdPrimes N Z, |BoundingSieve.rem d| ≤ C * ↑N / Real.log ↑N ^ U

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_levelSupport_subset (N : ℕ) (Z Δ : ℝ) (Q : ℕ) (hQ : ⌊Δ⌋₊ ≤ Q) : {d ∈ (goldbachB10ProdPrimes N Z).divisors | d < ⌊Δ⌋₊ + 1} ⊆ {d ∈ Finset.Icc 1 Q | d ∣ goldbachB10ProdPrimes N Z}

Inclusion of the actual strict-level divisor support, still including d = 1.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_levelRemainderSum_le (N : ℕ) (hEven : Even N) (Z Δ : ℝ) (Q : ℕ) (hQ : ⌊Δ⌋₊ ≤ Q) : have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N); ∑ d ∈ S.prodPrimes.divisors with d < ⌊Δ⌋₊ + 1, |BoundingSieve.rem d| ≤ ∑ d ∈ Finset.Icc 1 Q with d ∣ goldbachB10ProdPrimes N Z, |BoundingSieve.rem d|

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_levelRemainder_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z Δ : ℝ), ⌊Δ⌋₊ ≤ LiuWeight.panModulusCutoff N B → have S := goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N); ∑ d ∈ S.prodPrimes.divisors with d < ⌊Δ⌋₊ + 1, |BoundingSieve.rem d| ≤ C * ↑N / Real.log ↑N ^ U

Ready for the next sieve consumer; no Rosser main term or density estimate is asserted.