@[instance_reducible]

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

Equations

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_product_eq_goldbachPrimeProduct (N : ℕ) (hEven : Even N) (Z : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachB8PlusBoundingSieve N hEven Z) = goldbachB10PrimeProduct N Z

Only the prime values of the actual B8 density enter this identity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusBoundingSieve_product_log_le_liuSingularSeries (η : ℝ) (hη : 0 < η) : ∃ (Z₀ : ℝ), 2 ≤ Z₀ ∧ ∀ (N : ℕ), 4 ≤ N → ∀ (hEven : Even N) (Z : ℝ), Z₀ ≤ Z → AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachB8PlusBoundingSieve N hEven Z) * Real.log Z ≤ 2 * Real.exp (-Real.eulerMascheroniConstant) * (1 + η) * SingularSeries.liuSingularSeries N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_normalized_cutoff_geometry (B K τ : ℝ) (hB : 0 ≤ B) (hτ : 0 < τ) (hτ1 : τ ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have Z := √Δ; max 2 K ≤ Z ∧ Z ≤ ↑N ^ (1 / 4) ∧ ↑N ^ (1 / 4) ≤ ↑N ^ (3 / 11) ∧ Z ≤ √↑N ∧ Real.log Δ / Real.log Z = 2 ∧ 0 < Real.log Z ∧ Real.log ↑N / Real.log Z ≤ 4 * (1 + τ)

The real paid level gives ratio exactly two, with both production cutoff windows.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedCount_normalized_mainMass (δ : ℝ) (hδ : 0 < δ) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → have Z := √(↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)); 2 ≤ Z ∧ Z ≤ √↑N ∧ ↑(goldbachB8PlusSiftedAtoms N Z).card ≤ (8 + δ) * SingularSeries.liuSingularSeries N * goldbachB8PlusMainMass N / Real.log ↑N + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The selected B8 sieve, normalized on its unchanged sum of logarithmic integrals.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS4_normalized_upper_mainMass (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ (3 / 11))) ≤ (8 + δ) * SingularSeries.liuSingularSeries N * goldbachB8PlusMainMass N / Real.log ↑N + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The actual S4 consumer: no cutoff, level, free mass, or unpaid error remains.