theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeight_quadruple_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 ^ γ)) - ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β)) - ↑(goldbachWeightG12 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β) (↑N ^ γ)) - ↑(goldbachWeightT14 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β)) - ↑(goldbachWeightT15 (goldbachDifferenceCarrier N ε) N (↑N ^ α) (↑N ^ β) (↑N ^ γ)) - 42 * ↑N ^ (1 - α)

The actual first refinement after the two proved quadruple comparisons. The positive triple resources T14/T15 remain explicit; S6 coverage is not assumed.