theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RectangleMass_nonneg (N : ℕ) (ρ : ℝ) (k : ℕ × ℕ × ℕ) : 0 ≤ fouvryG9RectangleMass N ρ k

Nonnegativity of the actual labelled rectangle mass.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9S5Low_normalized_mass_upper (τ : ℝ) (hτ : 0 < τ) (A : ℕ) (e ε δ ρ ζ : ℝ) : 0 < e → e ≤ 1 → 0 < ε → ε < 4 / 53 → ε < δ → δ < 1 / 4 → 1 < ρ → ρ ≤ 5 / 4 → 0 < ζ → ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → Even N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N e) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ 4 * (1 + τ) * SingularSeries.liuSingularSeries N * ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMass N ρ k / Real.log (↑N ^ (5 / 9 - δ) / (2 / 3 * ρ ^ k.1) ^ (5 / 9)) + ↑N / Real.log ↑N ^ A + ζ * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

The original low S5 count, with all sieve-scalar and Euler corrections paid. Only the explicitly displayed weighted prime-rectangle mass remains analytic.