theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11GridCost_card {N : ℕ} {ε ρ : ℝ} (hρ : 1 < ρ) (hlog : 1 ≤ Real.log ↑N) : ↑(goldbachG11GridUsed N ε ρ).card ≤ (1 / Real.log ρ + 1) ^ 3 * Real.log ↑N ^ 3

The full occupied G11 grid, not just its low subfamily.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11Grid_subpower_sum (A : ℕ) {B μ ρ : ℝ} (hB : 0 ≤ B) (hμ : 0 < μ) (hρ : 1 < ρ) : ∃ (N₀ : ℝ), ∀ (N : ℕ), N₀ ≤ ↑N → 1 ≤ ↑N ∧ 1 ≤ Real.log ↑N ∧ ∀ (ε : ℝ) (E : ℕ × ℕ → ℝ), (∀ k ∈ goldbachG11GridUsed N ε ρ, E k ≤ B * ↑N ^ (1 - μ) * Real.log ↑N ^ 2) → ∑ k ∈ goldbachG11GridUsed N ε ρ, E k ≤ ↑N / Real.log ↑N ^ A

Reuse the existing fixed-power/log payment on the literal two-dimensional G11 grid. This generic finite envelope is instantiated with actual errors.