theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_paperG11_budget_identity : 661251229 / 200000000 + 10191 / 100000 = 681633229 / 200000000

Exact budget for the proposed G11 coefficient, not a proof of its count bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachD19_small_epsilon_lower_with_error_of_actual_estimates (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (δ : ℝ) (hδ : 0 < δ) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (r - g - 661251229 / 200000000 - δ) / 4 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

CONDITIONAL assembly only. Both missing analytic inputs remain explicit parameters. All three epsilon windows and all thresholds are reconciled before using the chosen Z.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachD19_small_epsilon_lower_of_actual_estimates (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (hgap : 0 < r - g - 661251229 / 200000000) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 2 / 15 ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (r - g - 661251229 / 200000000) / 8 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

A convenient positive-margin specialization; the preceding theorem retains arbitrary error.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachD19_eventually_lower_of_actual_estimates (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (hgap : 0 < r - g - 661251229 / 200000000) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (r - g - 661251229 / 200000000) / 8 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

Eliminate the auxiliary epsilon, retaining a quantitative lower bound on distinct p.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach19_eventually_representation_of_actual_estimates (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (hgap : 0 < r - g - 661251229 / 200000000) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

Literal p+r*q representation; not ordinary P2 and not a count of witness triples.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachD19_eventually_lower_of_g11_le_10191 (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (hg : g ≤ 10191 / 100000) (hr : 681633229 / 200000000 < r) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → (r - g - 661251229 / 200000000) / 8 * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(D19 N)

Plug-in endpoint for 0.10191 OR ANY SMALLER proved actual G11 upper coefficient. The quantitative conclusion automatically keeps the gain when g is smaller.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach19_eventually_representation_of_g11_le_10191 (g r : ℝ) (hG11 : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (g + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)) (hRemaining : ∀ (δ : ℝ), 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (Z : ℝ), 1 ≤ Z ∧ Z ≤ √↑N ∧ (r - δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2) ≤ ↑(goldbachWeightG11PaidBase N ε) - ↑(goldbachB9LowPositivePrefixSiftedCount N ε Z)) (hg : g ≤ 10191 / 100000) (hr : 681633229 / 200000000 < r) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ r ^ 10 ≤ q ^ 9

The same author-or-better plug-in endpoint for the original 1.9 representation.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_uniformScalar_fits_finalAssembly (δ : ℝ) : 0 < δ → ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachWeightG11 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ≤ (10385101 / 100000000 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Existing unconditional G11 theorem actually inhabits the generic input interface. It supplies 0.10385101, NOT the pending author value 0.10191.