theorem G12FineGrid.exists_small_raw_boundary_mesh (τ : ℝ) (hτ : 0 < τ) : ∃ (ρ : ℝ), 1 < ρ ∧ ρ ≤ 3 / 2 ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 2 / 15 → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Real.log ↑N / ↑N * (400 * ∑ k ∈ indices ρ N, ∑ p ∈ boundaryCell ρ N ε k, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1) ≤ τ

Fix a genuinely small geometric mesh before the truncation and ambient threshold. This is only the raw-mother normalization, not a prime-output bound.