theorem G12FineGrid.uniform_occupied_source (δ : ℝ) (hδ : 0 < δ) : ∃ (ζ : ℝ), 0 < ζ ∧ ζ ≤ 1 / 100 ∧ ∀ (e η : ℝ), 0 < e → 0 < η → η < 1 / 8 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ρ : ℝ), 1 < ρ → ρ ≤ 3 / 2 → ∀ (k p : ℕ × ℕ), p ∈ motherCell ρ N e k → have x := 4 * ↑(longLower ρ k) * ↑(shortLower ρ N k); have T := ↑(shortLower ρ N k); SourceGeometry ρ N e k ∧ 1 < x ∧ 0 < T ∧ x ^ G12LocalScale.nu x T = T ∧ ζ ≤ G12LocalScale.nu x T ∧ G12LocalScale.nu x T ≤ 1 / 10 + ζ / 10 ∧ ↑N ^ (1 / 3) ≤ G12LocalScale.level x T ζ ∧ G12LocalScale.level x T ζ ≤ ↑N ∧ 2 ≤ MathlibNt.SieveTheory.LiLiuPrereqWF.externalInternalLevel (G12LocalScale.level x T ζ) η ∧ 4 / 53 ≤ Real.log ↑p.2 / Real.log ↑N ∧ Real.log ↑p.2 / Real.log ↑N ≤ 1 / 10 ∧ 4 * Real.log ↑N / Real.log (G12LocalScale.level x T ζ) ≤ 36 / (5 * (1 - Real.log ↑p.2 / Real.log ↑N)) + δ

The source package is consumed at x=4MT for every atom in an occupied cell. The single threshold precedes all meshes, cell indices and actual prime labels.