@[instance_reducible]

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS5SwitchedCarrier (P : Prop) : Decidable P

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.instDecidableGoldbachS5SwitchedCarrier P = Classical.propDecidable P

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

The literal closed S5 sum, retaining both the pair and the original integer.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms N eps = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs N).sigma fun (rs : ℕ × ℕ) => Finset.filter (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint (N * rs.1) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod rs) ↑rs.2) (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.goldbachDifferenceCarrier N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS5ActualAtoms_iff {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachS5ActualAtoms N eps ↔ x.fst ∈ goldbachC9Pairs N ∧ x.snd ∈ goldbachDifferenceCarrier N eps ∧ literalHPoint (N * x.fst.1) (goldbachC9Prod x.fst) (↑x.fst.2) x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_eq_card_actualAtoms (N : ℕ) (eps : ℝ) : goldbachS5Closed (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) = ↑(goldbachS5ActualAtoms N eps).card

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5BadAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5BadAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms N eps | ¬x.snd.Coprime N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms N eps | x.snd.Coprime N}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodAtoms N eps | x.fst.1 ^ 2 ∣ x.snd}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodNonsquareAtoms (N : ℕ) (eps : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodNonsquareAtoms N eps = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodAtoms N eps | ¬x.fst.1 ^ 2 ∣ x.snd}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareSet (N : ℕ) : Finset ℕ

A set of integers, not a sum over square witnesses or a labelled atom count.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareSet N = {n ∈ Finset.range N | 0 < n ∧ ∃ (r : ℕ), Nat.Prime r ∧ ↑N ^ (4 / 53) ≤ ↑r ∧ r ^ 2 ∣ n}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachS5SquareSet_iff {N n : ℕ} : n ∈ goldbachS5SquareSet N ↔ 0 < n ∧ n < N ∧ ∃ (r : ℕ), Nat.Prime r ∧ ↑N ^ (4 / 53) ≤ ↑r ∧ r ^ 2 ∣ n

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareCount (N : ℕ) : ℤ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareCount N = ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareSet N).card

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Cofactor (x : (_ : ℕ × ℕ) × ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Cofactor x = x.snd / MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod x.fst

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtom_factorization {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS5ActualAtoms N eps) : x.snd = goldbachC9Prod x.fst * goldbachS5Cofactor x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Cofactor_prime {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hx : x ∈ goldbachS5GoodNonsquareAtoms N eps) : Nat.Prime (goldbachS5Cofactor x)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms (N : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

The full prime-cofactor prefix: no order or coprimality condition is imposed on q.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms N = (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Pairs N).sigma fun (rs : ℕ × ℕ) => {q ∈ Finset.range (N + 1) | Nat.Prime q ∧ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod rs * q < N}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9PlusAtoms_iff {N : ℕ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB9PlusAtoms N ↔ x.fst ∈ goldbachC9Pairs N ∧ Nat.Prime x.snd ∧ goldbachC9Prod x.fst * x.snd < N

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutput (N : ℕ) (x : (_ : ℕ × ℕ) × ℕ) : ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutput N x = N - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC9Prod x.fst * x.snd

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedAtoms (N : ℕ) (Z : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedAtoms N Z = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms N | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalHPoint N 1 Z (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutput N x)}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachB9PlusSiftedAtoms_iff {N : ℕ} {Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB9PlusSiftedAtoms N Z ↔ x ∈ goldbachB9PlusAtoms N ∧ SurvivesSieve N Z (goldbachB9PlusOutput N x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusSiftedAtoms_eq_coprime_filter (N : ℕ) (Z : ℝ) : goldbachB9PlusSiftedAtoms N Z = {x ∈ goldbachB9PlusAtoms N | (goldbachB10ProdPrimes N Z).Coprime (goldbachB9PlusOutput N x)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusPrimeAtoms (N : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusPrimeAtoms N = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms N | Nat.Prime (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutput N x)}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutputFiber (N p : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutputFiber N p = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusAtoms N | MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutput N x = p}

def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Switch (x : (_ : ℕ × ℕ) × ℕ) : (_ : ℕ × ℕ) × ℕ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Switch x = ⟨x.fst, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Cofactor x⟩

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Switch_output {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS5ActualAtoms N eps) : goldbachB9PlusOutput N (goldbachS5Switch x) = N - x.snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Switch_injOn {N : ℕ} {eps : ℝ} : Set.InjOn goldbachS5Switch ↑(goldbachS5ActualAtoms N eps)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Switch_mem_primeAtoms {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hx : x ∈ goldbachS5GoodNonsquareAtoms N eps) : goldbachS5Switch x ∈ goldbachB9PlusPrimeAtoms N ∧ eps * ↑N < ↑(goldbachC9Prod x.fst * goldbachS5Cofactor x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5GoodNonsquareAtoms_outputFiber_card_le {N p : ℕ} {eps : ℝ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) : {x ∈ goldbachS5GoodNonsquareAtoms N eps | N - x.snd = p}.card ≤ {x ∈ goldbachB9PlusPrimeAtoms N | goldbachB9PlusOutput N x = p}.card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms_fiber_card_le_fourHundred {N n : ℕ} {eps : ℝ} (hn1 : 1 ≤ n) (hnN : n < N) : {x ∈ goldbachS5ActualAtoms N eps | x.snd = n}.card ≤ 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5BadAtoms_card_le {N : ℕ} {eps : ℝ} (heps : 0 < eps) : ↑(goldbachS5BadAtoms N eps).card ≤ 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5SquareAtoms_card_le {N : ℕ} {eps : ℝ} (heps : 0 < eps) : ↑(goldbachS5SquareAtoms N eps).card ≤ 400 * goldbachS5SquareCount N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusOutputFiber_card_le_fourHundred (N p : ℕ) : (goldbachB9PlusOutputFiber N p).card ≤ 400

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Plus_low_card_le (N : ℕ) {Z : ℝ} (hZ : 1 ≤ Z) : ↑{x ∈ goldbachB9PlusAtoms N | ↑(goldbachB9PlusOutput N x) < Z}.card ≤ 400 * ↑⌊Z⌋₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9Plus_highPrime_subset_sifted (N : ℕ) (Z : ℝ) : {x ∈ goldbachB9PlusPrimeAtoms N | Z ≤ ↑(goldbachB9PlusOutput N x)} ⊆ goldbachB9PlusSiftedAtoms N Z

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9PlusPrimeAtoms_card_le_sifted (N : ℕ) {Z : ℝ} (hZ : 1 ≤ Z) : ↑(goldbachB9PlusPrimeAtoms N).card ≤ ↑(goldbachB9PlusSiftedAtoms N Z).card + 400 * ↑⌊Z⌋₊

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_le_sifted_B9Plus {N : ℕ} {eps Z : ℝ} (hN : 2 ≤ N) (heps : 0 < eps) (hcut : ↑N ^ (2 / 3) ≤ eps * ↑N) (hZ : 1 ≤ Z) : goldbachS5Closed (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ≤ ↑(goldbachB9PlusSiftedAtoms N Z).card + 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N + 400 * goldbachS5SquareCount N + 400 * ↑⌊Z⌋₊

All three losses count labelled fibers, with the square set left unpaid asymptotically.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_eventually_le_sifted_B9Plus (eps : ℝ) : 0 < eps → ∃ (N0 : ℕ), 2 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (Z : ℝ), 1 ≤ Z → goldbachS5Closed (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ≤ ↑(goldbachB9PlusSiftedAtoms N Z).card + 400 * goldbachBadCount (goldbachDifferenceCarrier N eps) N + 400 * goldbachS5SquareCount N + 400 * ↑⌊Z⌋₊