theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.pairLayer_floor_div (X : ℝ) (m : ℕ) : ⌊X⌋₊ / m = ⌊X / ↑m⌋₊

The genuine natural quotient has the same floor as the real quotient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.pairLayer_rounding (X : ℝ) (m : ℕ) (hY : 0 ≤ X / ↑m) : X / ↑m < ↑(⌊X⌋₊ / m + 1) ∧ ↑(⌊X⌋₊ / m + 1) ≤ X / ↑m + 1

Exact rounding bounds for the natural layer, including its final +1.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.pairLayer_log_rounding (Y D : ℝ) (hY : 1 ≤ Y) (hlo : Y ≤ D) (hhi : D ≤ Y + 1) : 0 ≤ Real.log D - Real.log Y ∧ Real.log D - Real.log Y ≤ 1

The floor perturbation contributes at most one to the logarithm.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.pairLayer_coordinate_eventually (B η : ℝ) (hB : 0 ≤ B) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, 4 ≤ N ∧ ∀ (m : ℕ), 0 < 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) - (1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53)| < η

Uniform power lower bound and absolute logarithmic coordinate control for Q / m + 1, where the quotient and the addition are both in ℕ.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_pairLayer_coordinate_threshold (B η : ℝ) (hB : 0 ≤ B) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (m : ℕ), 0 < 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) - (1 / 2 - Real.log ↑m / Real.log ↑N) / (4 / 53)| < η

One threshold is chosen before the whole varying modulus range.