theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAudit_actualLow {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachS5LowFirstActualAtoms N eps ↔ x.fst ∈ goldbachC10Pairs N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) ∧ x.snd ∈ goldbachDifferenceCarrier N eps ∧ literalHPoint (N * x.fst.1) (x.fst.1 * x.fst.2) (↑x.fst.2) x.snd ∧ ↑x.fst.1 < ↑N ^ (1 / 10)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAudit_rightMother {N : ℕ} {eps Z : ℝ} {x : (_ : ℕ × ℕ) × ℕ} : x ∈ goldbachB9LowPositivePrefixSiftedAtoms N eps Z ↔ Nat.Prime x.fst.1 ∧ Nat.Prime x.fst.2 ∧ (x.fst.1 * x.fst.2).Coprime N ∧ ↑N ^ (4 / 53) ≤ ↑x.fst.1 ∧ ↑x.fst.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑x.fst.2 ∧ x.fst.1 * x.fst.2 ^ 2 ≤ N ∧ x.snd ∈ Finset.range (N + 1) ∧ Nat.Prime x.snd ∧ eps * ↑N / ↑(x.fst.1 * x.fst.2) < ↑x.snd ∧ ↑x.snd < ↑N / ↑(x.fst.1 * x.fst.2) ∧ literalHPoint N 1 Z (N - x.fst.1 * x.fst.2 * x.snd) ∧ ↑x.fst.1 < ↑N ^ (1 / 10)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAudit_retainedEpsilon {N : ℕ} {eps : ℝ} {x : (_ : ℕ × ℕ) × ℕ} (heps : 0 < eps) (hx : x ∈ goldbachS5LowFirstActualAtoms N eps) : x.snd = (goldbachS5Switch x).fst.1 * (goldbachS5Switch x).fst.2 * (goldbachS5Switch x).snd ∧ eps * ↑N < ↑((goldbachS5Switch x).fst.1 * (goldbachS5Switch x).fst.2 * (goldbachS5Switch x).snd) ∧ eps * ↑N / ↑((goldbachS5Switch x).fst.1 * (goldbachS5Switch x).fst.2) < ↑(goldbachS5Switch x).snd

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9LowPositivePrefixAudit_terminal (delta : ℝ) (hdelta : 0 < delta) (eps : ℝ) (heps : 0 < eps ∧ eps < 2 / 15) : ∃ (N0 : ℕ), 4 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ ↑(goldbachB9LowPositivePrefixSiftedAtoms N eps Z).card + delta * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)