theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_movingKernelLedger : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ρ : ℝ), 0 < ρ → ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), goldbachPairMovingMain N hEven ε B ρ (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) + goldbachPairMovingMain N hEven ε B ρ (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) - ↑(∑ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), goldbachG11RoughCount N ε v) + (124341093 / 200000000 - goldbachB9PaperSplitIntegral - 10385101 / 100000000 - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ 4 * ↑(D19 N)

Actual moving JR kernels in the strongest weight ledger. The independent positive parameter rho is the density tolerance; delta pays all additive errors.