theorem G12FineGrid.exists_occupied_C2_sieve : ∃ (K : ℝ) (C : ℝ), 1 < K ∧ 0 < C ∧ ∀ (δ : ℝ), 0 < δ → ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∀ (e η : ℝ), 0 < e → e ≤ 1 → 0 < η → η < 1 / 8 → ∀ (A : ℕ), ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, Even N → ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 3 / 2 → ∀ (k p : ℕ × ℕ), p ∈ motherCell ρ N e k → have x := 4 * ↑(longLower ρ k) * ↑(shortLower ρ N k); have Q := G12LocalScale.level x (↑(shortLower ρ N k)) ζ; (↑N ^ (1 / 3) ≤ Q ∧ Q ≤ ↑N ∧ 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η) ∧ (4 / 53 ≤ Real.log ↑p.2 / Real.log ↑N ∧ Real.log ↑p.2 / Real.log ↑N ≤ 1 / 10) ∧ 4 * Real.log ↑N / Real.log Q ≤ 36 / (5 * (1 - Real.log ↑p.2 / Real.log ↑N)) + δ ∧ ∀ (Z : ℝ), 2 ≤ Z → Z ≤ √Q → have P := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftingPrimes N Z; have D := MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel Q η; have S := MathlibNt.SieveTheory.LiLiuPrereqWF.externalTags true P D η Z; have B := safe ρ N e k; have Euler := ∏ q ∈ P, (1 - AnalyticNumberTheory.Sieve.goldbachNu q); have E := C * (η + (η ^ 8)⁻¹ * Real.exp (6 * K + 2) * Real.log Q ^ (-(1 / 3))); (400 * ∑ q ∈ B, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N q.1 * if Nat.Prime (N - q.2 * q.1) then 1 else 0) ≤ 400 * G12FlexibleWF.mass N B * Euler * (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965F (Real.log Q / Real.log Z) + E) + 400 * ↑S.card * (x / Real.log x ^ A) + 400 * ↑S.card * G12FlexibleWF.correctionBudget N Q η + 8000 * ↑⌈Z⌉₊

Actual occupied grid atoms supply every geometric hypothesis of the full same-family C2 sieve. No per-cell source-size premise is carried by the caller.