theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11RoughPairs_cofactor_window {N p m : ℕ} {ε z b : ℝ} {v : GoldbachG11Label} (hv : v ∈ goldbachG11Labels N z b) (hpm : (p, m) ∈ goldbachG11RoughPairs N ε v) : ε * ↑N / ↑(goldbachG11LabelProd v) < ↑m ∧ ↑m < ↑N / ↑(goldbachG11LabelProd v)

Both strict cofactor endpoints come from the actual prime-output pair, not from a zero-prefix enlargement. This finite statement even allows an arbitrary real epsilon.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_positivePrefix_logQuotient_bounds (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), Real.log (ε * ↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd ∈ Set.Icc 4 (37 / 4)

A fixed positive prefix has a uniform Buchstab parameter window. The threshold precedes all four varying prime labels; this does not assert a rough-number asymptotic.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_actualRoughCofactor_log_bounds (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ v ∈ goldbachG11Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)), ∀ pm ∈ goldbachG11RoughPairs N ε v, Real.log ↑pm.2 / Real.log ↑v.snd.snd.snd ∈ Set.Ioo 4 (37 / 4)

Every actual cofactor lies strictly inside the common parameter window, after a threshold depending only on epsilon and not on its prime label or output prime.