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

The sharper actual quadratic grid bound fits the existing cubic-log budget. Only this finite-cardinality bridge is new; the scalar error payments are reused.