theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_crossProductLedger (ρ δ : ℝ) (hρ : 0 < ρ) (hρK : ρ < 53 / (2 * Real.exp Real.eulerMascheroniConstant)) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ((53 / (2 * Real.exp Real.eulerMascheroniConstant) - ρ) * (goldbachPairIdealSum N (2 * ρ) (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + goldbachPairIdealSum N (2 * ρ) (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))) + 124341093 / 200000000 - goldbachB9PaperSplitIntegral - 10385101 / 100000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) - ↑(goldbachG12ProductPrimeTotal N ε (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) ≤ 4 * ↑(D19 N)

The original weight ledger now uses the exact good cross product count. The additional bad-body loss is separately paid, not reused for free.