theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2MainMassUpperSum_eq_goldbachS2SwitchedMainMass (N : ℕ) (τ : ℝ) : goldbachS2MainMassUpperSum N τ = goldbachS2SwitchedMainMass N (↑N ^ τ)

The literal main-mass endpoint sum is definitionally the switched main mass at cutoff T = N^τ.

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

The actual switched S2 sieve product is the same normalized Euler product already controlled in the mature B10 library.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2SwitchedSiftedCount_normalized_upper_nine_nineteen_sub (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → have Z := ↑N ^ (1 / 4); have T := ↑N ^ (9 / 19 - ε); ↑(goldbachS2SwitchedSiftedCount N T Z) ≤ (8 * Real.log ((1 - (9 / 19 - ε)) / (9 / 19 - ε)) + δ) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The real switched S2 count at Z = N^(1/4) is fully normalized against the Liu singular series and the genuine S2 main-mass logarithmic kernel.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS2_normalized_upper_nine_nineteen_sub (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε))) ≤ (8 * Real.log ((1 - (9 / 19 - ε)) / (9 / 19 - ε)) + δ) * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The genuine finite S2 count inherits the normalized switched upper bound after paying the small-partner loss and the prime-factor bad set.