theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_strict_triple_lower_bound_eventually (ε : ℝ) (hε : 0 < ε) (hεupper : ε < 2 / 15) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (κ σ : ℝ), 1 / 21 < κ → κ < σ → σ ≤ 1 / 3 → 2 * goldbachS1 (goldbachDifferenceCarrier N ε) N (↑N ^ κ) - 2 * goldbachS2 (goldbachDifferenceCarrier N ε) N (↑N ^ (9 / 19 - ε)) - goldbachS3HalfOpen (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) - 2 * goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ σ) - goldbachS5HalfOpen (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) + goldbachWStrict (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) - (2 * goldbachBadCount (goldbachDifferenceCarrier N ε) N + goldbachQ (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ)) ≤ 2 * ↑(D19 N)

Two actual basic estimates followed by H1, H2 and H3. The triple sum is still strict; diagonal Q and noncoprime X remain actual counts. No analytic positive-main-term estimate, repeated-triple or endpoint payment is asserted here. The threshold is uniform in kappa and sigma.