theorem G12FineGrid.occupied_long_lower {ρ : ℝ} (hρ : 1 < ρ) (hu : ρ ≤ 3 / 2) {N : ℕ} {ε : ℝ} {k p : ℕ × ℕ} (hp : p ∈ motherCell ρ N ε k) (hsize : 6 ≤ ↑N ^ (4 / 53)) : 3 ≤ longLower ρ k

A large occupied long coordinate forces the actual rounded lower endpoint up.

structure G12FineGrid.SourceGeometry (ρ : ℝ) (N : ℕ) (ε : ℝ) (k : ℕ × ℕ) : Prop

Geometry of the actual clipped endpoints; this is not a safety assertion.

• long_three : 3 ≤ longLower ρ k
• short_three : 3 ≤ shortLower ρ N k
• long_order : longLower ρ k ≤ longUpper ρ N k
• long_twice : longUpper ρ N k ≤ 2 * longLower ρ k
• short_order : shortLower ρ N k ≤ shortUpper ρ N k
• short_twice : shortUpper ρ N k ≤ 2 * shortLower ρ N k
• source_lower : ↑N ^ (4 / 53) ≤ ↑(shortLower ρ N k)
• source_upper : ↑(shortUpper ρ N k) < ↑N ^ (1 / 10)
• scale_lower : ε * ↑N ≤ 4 * ↑(longLower ρ k) * ↑(shortLower ρ N k)
• scale_upper : 4 * ↑(longLower ρ k) * ↑(shortLower ρ N k) ≤ 4 * ↑N

theorem G12FineGrid.uniform_occupied_geometry : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ N ≥ N₀, ∀ (ρ ε : ℝ), 1 < ρ → ρ ≤ 3 / 2 → ∀ (k : ℕ × ℕ), (motherCell ρ N ε k).Nonempty → SourceGeometry ρ N ε k

One cutoff precedes every mesh, prefix and occupied mother cell.

theorem G12FineGrid.occupied_atom_coordinates {ρ ε : ℝ} {N : ℕ} {k p : ℕ × ℕ} (hp : p ∈ motherCell ρ N ε k) : shortLower ρ N k < p.2 ∧ p.2 ≤ shortUpper ρ N k ∧ ↑N ^ (4 / 53) ≤ ↑p.2 ∧ ↑N ^ (4 / 53) ≤ ↑p.1

The actual atom supplies the source prime, not an artificial endpoint.