theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusBoundingSieve_product_eq_goldbachPrimeProduct (N : ℕ) (hEven : Even N) (Z : ℝ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachB10BoundingSieve N hEven 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z (goldbachB9PlusMainMass N)) = goldbachB10PrimeProduct N Z

The production identity only identifies the density at primes in the strict product.

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

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Plus_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) ∧ Z ≤ √↑N ∧ Real.log Δ / Real.log Z = 2 ∧ 0 < Real.log Z ∧ Real.log ↑N / Real.log Z ≤ 4 * (1 + τ)

Reuse the public scalar geometry, without imposing the B8 carrier window on B9.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedCount_normalized_mainMass (δ η : ℝ) (hδ : 0 < δ) (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 ∧ ↑(goldbachB10SiftedCount N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z) ≤ (8 + δ) * SingularSeries.liuSingularSeries N * goldbachB9PlusMainMass N / Real.log ↑N + η * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Independent main-term and error tolerances keep the final S5 budget exact.

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

Actual S5Closed on the original epsilon carrier; no free sieve parameter remains.