theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstIntegral_publicAudit : 0 ≤ goldbachB9HighMainIntegral ∧ (∀ (n : ℕ), 0 < n → goldbachB9HighLogGridUpperSum n - goldbachB9HighMainIntegral ≤ 10000 / ↑n) ∧ (∀ (δ : ℝ), 0 < δ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachK9High N ≤ goldbachB9HighMainIntegral + δ) ∧ ∀ (δ ε : ℝ), 0 < δ → 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) ≤ (8 * goldbachB9HighMainIntegral + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachK9High_expanded_integralAudit (δ : ℝ) (hδ : 0 < δ) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), 1 / (↑rs.1 * ↑rs.2 * (1 - Real.log (↑rs.1 * ↑rs.2) / Real.log ↑N)) ≤ (∫ (u : ℝ) in 1 / 10..1 / 3, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))) + δ

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstNormalized_inputAudit (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) ≤ ((8 + δ) * ∑ rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)), 1 / (↑(goldbachC10Prod rs) * (1 - Real.log ↑(goldbachC10Prod rs) / Real.log ↑N)) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirst_expanded_integralAudit (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(∑ rs ∈ goldbachS4Pairs N (↑N ^ (1 / 10)) with ↑rs.1 ≤ ↑N ^ (1 / 3) ∧ ↑N ^ (1 / 3) ≤ ↑rs.2, literalH (Finset.image (fun (p : ℕ) => N - p) (goldbachPrimeCarrier N ε)) (N * rs.1) (rs.1 * rs.2) ↑rs.2) ≤ ((8 * ∫ (u : ℝ) in 1 / 10..1 / 3, ∫ (v : ℝ) in 1 / 3..(1 - u) / 2, 1 / (u * v * (1 - u - v))) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstBoundary_gridAudit (n N : ℕ) (hn : 0 < n) (hN : 2 ≤ N) (rs : ℕ × ℕ) (hrs : rs ∈ goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) (hboundary : ↑N ^ (1 / 10) = ↑rs.1) : LiuWeight.primeLogExponent N rs.1 = 1 / 10 ∧ ∃ q ∈ goldbachB9HighLogGridCells n, LiuWeight.LiuPairInLogRectangle N (goldbachB9AlphaGridPoint n ↑q.1) (goldbachB9AlphaGridPoint n (↑q.1 + 1)) (goldbachB9BetaGridPoint n ↑q.2) (goldbachB9BetaGridPoint n (↑q.2 + 1)) rs