theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_reciprocal_level_loss {b δ : ℝ} (hb : 1 / 2 ≤ b) (hδ : 0 ≤ δ) (hδu : δ < 1 / 4) : 4 / (b - δ) ≤ 4 / b + 32 * δ

Reciprocal-level stability with a fixed explicit loss, uniformly in the short-prime coordinate.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel_log_lower {N : ℕ} {ε ρ δ : ℝ} (hN : 4 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) {p : ℕ} (hp : p ∈ goldbachG11GridShort N ρ k) : (5 / 9 * (1 - min (Real.log ↑p / Real.log ↑N) (1 / 10)) - δ) * Real.log ↑N ≤ Real.log (goldbachG11MixedLevel N δ ρ k)

The actual buffered low level and ordinary high level both dominate the level encoded by the author's clamped weight at EVERY prime in the cell.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11MixedLevel_author_weight {N : ℕ} {ε ρ δ : ℝ} (hN : 4 ≤ N) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) (hbig : 4 ≤ ↑N ^ (4 / 53)) (hδ : 0 ≤ δ) (hδu : δ < 1 / 4) {k : ℕ × ℕ} (hk : k ∈ goldbachG11GridUsed N ε ρ) {p : ℕ} (hp : p ∈ goldbachG11GridShort N ρ k) : 4 * Real.log ↑N / Real.log (goldbachG11MixedLevel N δ ρ k) ≤ goldbachG11AuthorWeight (Real.log ↑p / Real.log ↑N) + 32 * δ

The author weight is derived from the literal two-route level, rather than substituted for the old uniform coefficient 8.