theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_low_log_budget (L R Q S T : ℝ) (hL : 0 ≤ L) (hR : R ≤ L / 10) (hQ : Q ≤ 4 / 33 * L) (hS : S ≤ 4 / 33 * L) (hT : T ≤ 3 / 11 * L) : 79 / 25 * Q ≤ L - (R + Q + S + T)

The original low first-prime box leaves at least 3.16 q-logarithms.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_canonical_low_logQuotient {N r q s t : ℕ} (hN : 4 ≤ 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) (hcut : ↑r < ↑N ^ (1 / 10)) : 79 / 25 ≤ Real.log (↑N / ↑(r * q * s * t)) / Real.log ↑q

Low first-prime geometry for the literal original closed cross.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_low_cut_of_log {N r : ℕ} (hN : 4 ≤ N) (hr : Nat.Prime r) (h : Real.log ↑r / Real.log ↑N < 1 / 10) : ↑r < ↑N ^ (1 / 10)

The logarithmic step cutoff is exactly the physical low cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_buchstab_le_factor {N : ℕ} (hN : 4 ≤ N) {v : GoldbachG11Label} (hv : v ∈ goldbachG12Labels N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) : LiLiuPrereqBuchstab.buchstab (Real.log (↑N / ↑(goldbachG11LabelProd v)) / Real.log ↑v.snd.snd.snd) ≤ G12SharpWeight.factor (Real.log ↑v.snd.snd.fst / Real.log ↑N)

The actual Buchstab value is bounded by the step factor, not a uniform constant.