theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachG67_integral_tolerance (δ : ℝ) (hδ : 0 < δ) : ∃ (ρ : ℝ), 0 < ρ ∧ ρ < 53 / (2 * Real.exp Real.eulerMascheroniConstant) ∧ goldbachG67IntegralConstant - δ ≤ (53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (goldbachG67JRIntegral 0 - 2 * ρ * goldbachG67LogRectangleMass - ρ)

Choose the density tolerance before epsilon and N, paying all truncation losses.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_pairIntegralLedger (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (goldbachG67IntegralConstant + 124341093 / 200000000 - goldbachB9PaperSplitIntegral - 10385101 / 100000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) - 400 * ∑ m ∈ goldbachG12ActiveProductSupport N, goldbachG12NormalizedCoefficient N m * ↑(goldbachG11ProductFirstPrimeFiber N ε (↑N ^ (4 / 53)) m).card ≤ 4 * ↑(D19 N)

The actual G6/G7 pair sums are replaced by their fixed JR integrals. The original G12 output-prime fibres remain explicit: no output upper sieve is assumed.