theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_idealKernelLedger (ρ δ : ℝ) (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) - ↑(∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), goldbachG11RoughCount N ε v) ≤ 4 * ↑(D19 N)

The actual weight ledger with ideal-coordinate, scalar-normalized pair sums. The sieve level and its logarithmic shrink no longer appear in the conclusion. The finite pair sums and original cross rough sum are not yet replaced by integrals.