theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareCount_le_QA (N : ℕ) : goldbachS5SquareCount N ≤ goldbachQA ({n ∈ Finset.range N | 0 < n}) N (↑N ^ (4 / 53))

A union of square-divisibility fibres is at most their actual QA mass. The ambient carrier is all positive integers below N, not the prime difference set.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareCount_normalized (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → 400 * ↑(goldbachS5SquareCount N) ≤ δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_le_B10ZeroPrefix_normalized (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) ≤ ↑(goldbachB10SiftedCount N 0 (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) Z) + δ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Original S5Closed to the existing zero-prefix B10 sieve, with all finite losses paid. The threshold precedes the moving sieve cutoff Z, and the left carrier keeps epsilon.