theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Grid_buffered_geometry {N : ℕ} {e ρ : ℝ} (he : 0 < e) (hρ : 1 < ρ) (hρu : ρ ≤ 5 / 4) {k : ℕ × ℕ × ℕ} (hne : (fouvryG9GridCell N e ρ k).Nonempty) : have T := 2 / 3 * ρ ^ k.1; have M := ρ ^ (k.2.1 + k.2.2); 1 ≤ M ∧ ↑N / (2 / e) ≤ 4 * M * T ∧ 4 * M * T ≤ 4 * ↑N ∧ ↑N ^ (4 / 53) / 2 ≤ T ∧ T ≤ ↑N ^ (1 / 10)

Buffer the short scale so integer closed/open endpoints can later be encoded inside the prime interval family. The physical product scale changes with it.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9Grid_exists_buffered_C2_parameters {e ε δ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hε : 0 < ε) (hεa : ε < 4 / 53) (hεδ : ε < δ) (hδ : δ ≤ 1 / 2) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 5 / 4 → ∀ (k : ℕ × ℕ × ℕ), (fouvryG9GridCell N e ρ k).Nonempty → have T := 2 / 3 * ρ ^ k.1; have M := ρ ^ (k.2.1 + k.2.2); have x := 4 * M * T; have ν := Real.log T / Real.log x; 1 ≤ M ∧ 1 < x ∧ 1 ≤ T ∧ T = x ^ ν ∧ ε ≤ ν ∧ ν ≤ 1 / 10 + ε / 10 ∧ ↑N ≤ 2 / e * x ∧ ∀ (j : ℕ) (c : ℕ → ℝ), AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (↑N ^ (5 / 9 - δ) / T ^ (5 / 9)) c → AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c

Every occupied actual G9 cell admits the expanded C2 parameters at a common threshold, and the same global weight transports to the local full level.