theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCost_card {N : ℕ} {eps ρ : ℝ} (hρ : 1 < ρ) (hN : 1 ≤ Real.log ↑N) : ↑(fouvryG9GridUsed N eps ρ).card ≤ (1 / Real.log ρ + 1) ^ 3 * Real.log ↑N ^ 3

A real logarithmic bound for the number of actually occupied grid cells.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCost_log_window {n K x : ℝ} (hK : 1 ≤ K) (hn : 0 < n) (hlarge : 2 * Real.log K ≤ Real.log n) (hx : n / K ≤ x) : 0 < x ∧ Real.log n / 2 ≤ Real.log x

The local logarithm comparison is uniform on the full window, including x < N.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCost_one {n K x E : ℝ} (A : ℕ) (hK : 1 ≤ K) (hn : 0 < n) (hlog : 1 ≤ Real.log n) (hlarge : 2 * Real.log K ≤ Real.log n) (hxlo : n / K ≤ x) (hxhi : x ≤ 4 * n) (hE : |E| ≤ x / Real.log x ^ (A + 4)) : |E| ≤ 4 * 2 ^ (A + 4) * n / Real.log n ^ (A + 4)

One C2-sized real error costs a fixed multiple of N / log(N)^(A+4).

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCost_scalar {n D C : ℝ} (A : ℕ) (hn : 0 ≤ n) (hl : 0 < Real.log n) (hDC : D * C ≤ Real.log n) : D * Real.log n ^ 3 * (C * n / Real.log n ^ (A + 4)) ≤ n / Real.log n ^ A

Exact payment of the cubic grid cost with the last spare logarithmic power.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9GridCost_total (ρ K : ℝ) (A : ℕ) (hρ : 1 < ρ) (hK : 1 ≤ K) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → ∀ (eps : ℝ) (x E : ℕ × ℕ × ℕ → ℝ), (∀ k ∈ fouvryG9GridUsed N eps ρ, ↑N / K ≤ x k ∧ x k ≤ 4 * ↑N) → (∀ k ∈ fouvryG9GridUsed N eps ρ, |E k| ≤ x k / Real.log (x k) ^ (A + 4)) → ∑ k ∈ fouvryG9GridUsed N eps ρ, |E k| ≤ ↑N / Real.log ↑N ^ A

The actual occupied grid pays all local C2 envelopes, uniformly in eps and every scale.