theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_buchstabParameter_bounds {u v w x : ℝ} (hu : u ∈ Set.Icc (4 / 53) (4 / 33)) (hv : v ∈ Set.Icc (4 / 53) (4 / 33)) (hw : w ∈ Set.Icc (4 / 53) (4 / 33)) (hx : x ∈ Set.Icc (4 / 33) (3 / 11)) : (1 - u - v - w - x) / v ∈ Set.Icc 3 (1141 / 132)

A domain estimate for the literal Buchstab argument; no estimate for the Buchstab function.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_logPrimeExponent_mem {N p : ℕ} {a b : ℝ} (hN : 2 ≤ N) (hp : Nat.Prime p) (hlo : ↑N ^ a ≤ ↑p) (hhi : ↑p ≤ ↑N ^ b) : Real.log ↑p / Real.log ↑N ∈ Set.Icc a b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_canonical_logQuotient_bounds {N r q s t : ℕ} (hN : 2 ≤ N) (ht : t ∈ goldbachClosedPrimes N (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) (hs : s ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hr : r ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) ↑s) (hq : q ∈ goldbachClosedPrimes N ↑r ↑s) : Real.log (↑N / ↑(r * q * s * t)) / Real.log ↑q ∈ Set.Icc 3 (1141 / 132)

Actual closed cross G12 labels give the same compact Buchstab window, including repeated primes.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12_low_buchstabParameter_lower {u v w x : ℝ} (hu : u ≤ 1 / 10) (hv : v ∈ Set.Icc (4 / 53) (4 / 33)) (hw : w ≤ 4 / 33) (hx : x ≤ 3 / 11) : 127 / 40 ≤ (1 - u - v - w - x) / v

The low-first-prime domain gives 127/40, without relaxing to 79/25.