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

Fixed author-weighted G12 ledger. The full actual JR positive constant is retained; this does not assert a rational numerical estimate or net positivity.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorIntegralConstant_eq_split : goldbachG12AuthorIntegralConstant = 564383 / 1000000 * Real.log (9 / 4) * ((36 / 5 * ∫ (r : ℝ) in 4 / 53..1 / 10, (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r) / (r * (1 - r))) + 8 * ∫ (r : ℝ) in 1 / 10..4 / 33, (1 / (4 / 33) + (Real.log (4 / 33 / r) - 1) / r) / r)

Exact one-dimensional author split for the constant actually used above. Both branches retain the uniform proved Buchstab majorant.