theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_sharpG9CertifiedLedger (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (goldbachG67IntegralConstant + 124341093 / 200000000 - 527231 / 100000 - 10385101 / 100000000 - goldbachG12SharpIntegralConstant - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

The actual D19 ledger now consumes the certified G9 constant.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.sharp_margin_lower_of_two_integral_bounds (h67 : 54233 / 10000 ≤ 4 * G67SumCoordinate.piecewiseIntegral) (h12 : goldbachG12SharpIntegralConstant ≤ 66821 / 100000) : 1 / 2000 ≤ goldbachSharpElementaryMargin

Only the G67 and G12 scalar bounds remain as premises here.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.eventually_onePlusOneNine_source_of_two_integral_bounds (h67 : 54233 / 10000 ≤ 4 * G67SumCoordinate.piecewiseIntegral) (h12 : goldbachG12SharpIntegralConstant ≤ 66821 / 100000) : ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ ↑r ≤ ↑q ^ (19 / 10 - 1)

A conditional exit in the paper's literal real-exponent syntax. The two scalar premises are deliberately explicit and are not proved here.