theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9PrimeOutput_coprime {N r : ℕ} {z : ℝ} (hr : Nat.Prime r) (hz : z ≤ ↑r) : r.Coprime ((fouvryG9SievePrimes N z).prod id)

A prime output at or above the cutoff survives the literal sieve carrier. No coprimality of the output with N is needed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9PrimeOutput_indicator (N r : ℕ) (z : ℝ) : (if Nat.Prime r then 1 else 0) ≤ (if r.Coprime ((fouvryG9SievePrimes N z).prod id) then 1 else 0) + if ↑r < z then 1 else 0

The exact pointwise split retains small prime outputs as an explicit cost.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherPrimeOutput (N : ℕ) (e : ℝ) : ℝ

Prime-output count on the original labelled positive-prefix atoms.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherPrimeOutput N e = ∑ a ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAtoms N e, if Nat.Prime (↑N - ↑(a.fst.2 * a.snd) * ↑a.fst.1).natAbs then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9SmallOutput_mother_le_rectangles {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (z : ℝ) (hbig : ∀ k ∈ fouvryG9GridUsed N e ρ, 3 ≤ ρ ^ k.1) : (∑ a ∈ goldbachB9LowPositivePrefixAtoms N e, if ↑(↑N - ↑(a.fst.2 * a.snd) * ↑a.fst.1).natAbs < z then 1 else 0) ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9SmallOutputRectangle N ρ k z

The real positive-cover theorem, applied to the small-output indicator.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherPrimeOutput_le_sifted_add_small {N : ℕ} {e ρ : ℝ} (hN : 1 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (z : ℝ) (hbig : ∀ k ∈ fouvryG9GridUsed N e ρ, 3 ≤ ρ ^ k.1) : fouvryG9MotherPrimeOutput N e ≤ fouvryG9MotherSifted N e (fouvryG9SievePrimes N z) + ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9SmallOutputRectangle N ρ k z

Correct replacement for the false claim that every prime output is sifted.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9MotherPrimeOutput_total (A : ℕ) {e ε δ η ρ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ < 1 / 2) (hη : 0 < η) (hηu : η < 1 / 8) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (z : ℝ), 0 ≤ z → z ≤ √↑N → fouvryG9MotherPrimeOutput N e ≤ ∑ k ∈ fouvryG9GridUsed N e ρ, fouvryG9RectangleMain N ρ δ η k (fouvryG9SievePrimes N z) z + ↑N / Real.log ↑N ^ A

The corrected prime-output upper sieve. Both error budgets use A+1.