theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67_movingKernel_paid (U : ℝ) (hU : 0 < U) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ρ : ℝ), 0 < ρ → ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), goldbachPairMovingMain N hEven ε B ρ (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) - C * ↑N / Real.log ↑N ^ U ≤ ↑(goldbachWeightG6 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ∧ goldbachPairMovingMain N hEven ε B ρ (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) - C * ↑N / Real.log ↑N ^ U ≤ ↑(goldbachWeightG7 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))

The same BV constants pay each original G6 and G7 family. They remain separate families: their common closed endpoint is counted in each original term.