theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_strictEndpoint_mainMass_upper (ε η : ℝ) (hε : 0 < ε) (hεu : ε < 1) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) ≤ (1 - ε + η) * (↑N / Real.log ↑N)

The genuine mass at the strict endpoint retains its factor 1 - epsilon. The rounding, logarithm transport, and genuine-minus-proxy remainder are paid before choosing the uniform natural-number threshold.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve_sieveProduct_eq_S1 (N : ℕ) (hEven : Even N) (ε z : ℝ) (p : ℕ) : AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS3BoundingSieve N hEven ε z p) = AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε z)

Conditioning the carrier does not change either nu or prodPrimes.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_li_mul_eulerProduct_upper (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), BombieriVinogradov.trueLogarithmicIntegral ↑(goldbachS1Endpoint N ε) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors (goldbachS1BoundingSieve N hEven ε (↑N ^ (4 / 53))) ≤ ((1 - ε) * (53 / 2) * Real.exp (-Real.eulerMascheroniConstant) + δ) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The strict S3 Li prefactor times the actual Euler product at N^(4/53), with a fully paid additive budget on the genuine Liu singular-series scale.