theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputFiber_injOn (N p : ℕ) (ε : ℝ) : Set.InjOn (fun (x : GoldbachG12LinkedAtom) => x.snd) ↑({x ∈ goldbachG12LinkedAtoms N ε | goldbachG12LinkedOutput N x = p})

A fixed output determines m after the prime r has been retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputFiber_card_le_twenty {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (p : ℕ) : {x ∈ goldbachG12LinkedAtoms N ε | goldbachG12LinkedOutput N x = p}.card ≤ 20

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputWeight_le_twenty {N : ℕ} (hN : 2 ≤ N) (ε : ℝ) (p : ℕ) : goldbachG12LinkedOutputWeight N ε p ≤ 20

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedSmallOutputMass (N : ℕ) (ε Z : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedSmallOutputMass N ε Z = ∑ p ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputSupport N ε with p < ⌈Z⌉₊, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedOutputWeight N ε p

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedSmallOutputMass_le {N : ℕ} (hN : 2 ≤ N) (ε Z : ℝ) : goldbachG12LinkedSmallOutputMass N ε Z ≤ 20 * ↑⌈Z⌉₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12LinkedPrimeOutput_le_sifted_add_small (N : ℕ) (ε Z : ℝ) : ∑ p ∈ goldbachG12LinkedOutputSupport N ε with Nat.Prime p, goldbachG12LinkedOutputWeight N ε p ≤ goldbachG12LinkedSiftedMass N ε Z + goldbachG12LinkedSmallOutputMass N ε Z

Prime outputs survive the sieve unless they lie below its cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12OutputTotal_le_linkedSifted {N : ℕ} (hN : 2 ≤ N) (ε Z : ℝ) : 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ 400 * goldbachG12LinkedSiftedMass N ε Z + 8000 * ↑⌈Z⌉₊

The literal original output-prime fibres on the G12 active support.