theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RectangleSmallMass_nonneg (N : ℕ) (U V : Finset ℕ) (z : ℝ) : 0 ≤ goldbachG11RectangleSmallMass N U V z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_prime_outputs_paid (A : ℕ) {ε δ θ ρ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (z : ℝ), 0 ≤ z → z ≤ √↑N → ∑ k ∈ goldbachG11LowGridUsed N ε ρ, goldbachG11RectanglePrimeMass N (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) ≤ (goldbachG11LowGridDensityMain N ε δ θ ρ (fun (x : ℕ × ℕ) => fouvryG9SievePrimes N z) fun (x : ℕ × ℕ) => z) + 3 * ↑N / Real.log ↑N ^ A

Low-grid actual prime outputs, after fully paying both distribution and small-output losses, with the canonical output sieve and no external premises.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11LowGrid_mother_outputs_paid (A : ℕ) {ε δ θ ρ : ℝ} (hε : 0 < ε) (hεu : ε ≤ 1) (hδ : 0 < δ) (hδu : δ < 1 / 2) (hθ : 0 < θ) (hθu : θ < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (z : ℝ), 0 ≤ z → z ≤ √↑N → ∑ k ∈ goldbachG11LowGridUsed N ε ρ, goldbachG11RectangleMotherCount N ε (goldbachG11GridLong N ε ρ k) (goldbachG11GridShort N ρ k) ≤ (goldbachG11LowGridDensityMain N ε δ θ ρ (fun (x : ℕ × ℕ) => fouvryG9SievePrimes N z) fun (x : ℕ × ℕ) => z) + 3 * ↑N / Real.log ↑N ^ A

The original restricted first-prime fibres inherit the paid estimate; all product-coefficient multiplicities are the existing literal ones.