theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_initial_paid_eventually (ε : ℝ) (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (α β γ : ℝ), 1 / 21 < α → α ≤ β → β ≤ γ → ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ β)) - ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ β) (↑N ^ γ)) ≥ ↑(goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ α)) - ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ γ)) + ↑(goldbachWeightG6 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β)) + ↑(goldbachWeightG7 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β) (↑N ^ γ)) - ↑(goldbachWeightG14 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β)) - ↑(goldbachWeightG15 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β) (↑N ^ γ)) - 42 * ↑N ^ (1 - α)

The paid first weight refinement on the actual prime-difference carrier. One epsilon-dependent threshold precedes all three exponent parameters. This is not the full twelve-term inequality or positivity of D19.