theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Thin_buchstab_modulus (η : ℝ) (hη : 0 < η) : ∃ δ > 0, δ ≤ 1 ∧ ∀ u ∈ Set.Icc 2 10, ∀ v ∈ Set.Icc 2 10, |u - v| < δ → |LiLiuPrereqBuchstab.buchstab u - LiLiuPrereqBuchstab.buchstab v| < η

Compact continuity gives one modulus for every endpoint, not a derivative estimate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Thin_uniform_endpoint (e₀ : ℝ) (he₀ : 0 < e₀) (he₁ : e₀ ≤ 1) (η : ℝ) (hη : 0 < η) : ∃ (X : ℝ) (L : ℝ), 1 < X ∧ 0 < L ∧ ∀ (y q : ℝ), X ≤ e₀ * y → L ≤ Real.log q → 1 < q → Real.log y / Real.log q ∈ Set.Icc 3 (1141 / 132) → ∀ l ∈ Set.Icc e₀ 1, |↑(LiLiuPrereqBuchstab.roughCount (l * y) q) - l * goldbachG11BuchstabMass y q| ≤ η * y / Real.log q

Real endpoints retain the literal integer rough counts, including both floors. The threshold is chosen before the scaling parameter.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Thin_canonical_endpoints (e₀ : ℝ) (he₀ : 0 < e₀) (he₁ : e₀ ≤ 1) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), ∀ l ∈ Set.Icc e₀ 1, |↑(LiLiuPrereqBuchstab.roughCount (l * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd) - l * goldbachG11BuchstabMass (↑N / ↑(goldbachG11LabelProd v)) ↑v.snd.snd.snd| ≤ η * (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd

Uniform raw-mother endpoint approximation on the original closed cross.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12Thin_cofactor_budget (e₀ : ℝ) (he₀ : 0 < e₀) (he₁ : e₀ ≤ 1) (η : ℝ) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)), ∀ (l₁ l₂ : ℝ), e₀ ≤ l₁ → l₁ ≤ l₂ → l₂ ≤ 1 → ↑(LiLiuPrereqBuchstab.roughCount (l₂ * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd) - ↑(LiLiuPrereqBuchstab.roughCount (l₁ * (↑N / ↑(goldbachG11LabelProd v))) ↑v.snd.snd.snd) ≤ (564383 / 1000000 * (l₂ - l₁) + η) * (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd

The coefficient is the certified broad Buchstab majorant. This does not assert an output-prime sieve, a second logarithm, or a full boundary payment.