theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachFiniteError_le_446_of_growth (N : ℕ) (ε κ y : ℝ) (hN : 1 ≤ N) (hlarge : 1 < ε * ↑N) (hκ : 1 / 21 < κ) (hκupper : κ ≤ 1 / 3) (hz : 2 ≤ ↑N ^ κ) (hzy : ↑N ^ κ ≤ y) : ↑(goldbachFiniteError (goldbachDifferenceCarrier N ε) N (↑N ^ κ) y) ≤ 446 * ↑N ^ (1 - κ)

The actual four error counts, with all component bounds supplied by proofs. The carrier is the actual prime-difference carrier, not an arbitrary count.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachFiniteError_446_eventually (ε : ℝ) (hε : 0 < ε) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (κ σ : ℝ), 1 / 21 < κ → κ < σ → σ ≤ 1 / 3 → 0 ≤ goldbachFiniteError (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) ∧ ↑(goldbachFiniteError (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ)) ≤ 446 * ↑N ^ (1 - κ)

A single epsilon-dependent threshold controls the actual error uniformly in kappa and sigma. No evenness or analytic distribution input is needed.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachbig_finite_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 - ε)) - goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) - 2 * goldbachS4 (goldbachDifferenceCarrier N ε) N (↑N ^ σ) - goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ) + goldbachS6Closed (goldbachDifferenceCarrier N ε) N (↑N ^ κ) (↑N ^ σ)) - 446 * ↑N ^ (1 - κ) ≤ 2 * ↑(D19 N)

Finite Goldbachbig with the actual D19 count and a proved explicit error. This is a signed sieve lower bound, not positivity or the final 1+1.9 theorem.