theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.pairLayer_ideal_coordinate_bounds (N m : ℕ) (hN : 4 ≤ N) (hm : 0 < m) (hml : ↑N ^ (8 / 53) ≤ ↑m) (hmu : ↑m ≤ ↑N ^ (13 / 33)) : 0 < (1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53) ∧ (1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53) ≤ 37 / 8

The ideal coordinate lies in a fixed positive interval for the pair range.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_pairLayer_coordinate_lt_six (B : ℝ) (hB : 0 ≤ B) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (m : ℕ), 0 < m → ↑N ^ (8 / 53) ≤ ↑m → ↑m ≤ ↑N ^ (13 / 33) → ↑N ^ (7 / 132) ≤ ↑(LiuWeight.panModulusCutoff N B / m + 1) ∧ Real.log ↑(LiuWeight.panModulusCutoff N B / m + 1) / (4 / 53 * Real.log ↑N) < 6

Uniform fixed compact-range consumer; no prime or coprimality assumptions.