resolution_achievable
plain-language theorem explainer
For fixed box side L > 0 and any target resolution ε > 0, lattice spacing a = L/N eventually drops below ε. Gravity and continuum-limit arguments cite it to justify N → ∞ refinement. The proof is a short real-analysis argument: pick N larger than L/ε via exists_nat_gt and rearrange the inequality.
Claim. For every box length $L > 0$ and every target resolution $\varepsilon > 0$, there exists a positive integer $N_0$ such that for all $N \ge N_0$, the lattice spacing satisfies $L/N < \varepsilon$.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice → quadratic cost → Laplacian → Minkowski interval → curved metric from defect → Einstein equations. Architecture step 5 is a finite N-site lattice in a box of side L with spacing a = L/N; continuum statements require a → 0 as N → ∞.
RS-native units fix the microscopic quanta: one tick τ₀ = 1 and one voxel ℓ₀ = 1, so c = ℓ₀/τ₀ = 1 voxel per tick. The continuum limit does not change those quanta; it only refines how many sites pack into a macroscopic box of side L.
This lemma is the elementary Archimedean fact that makes refinement well-defined: spacing is eventually smaller than any prescribed ε. Downstream lattice-refinement wrappers restate it as "spacing N < ε eventually."
proof idea
Term-mode proof. Apply exists_nat_gt (L/ε) to obtain some natural N₀ with N₀ > L/ε. Return witness N₀+1 (strictly positive). For any N ≥ N₀+1, cast positivity of N, rewrite L/N < ε as L < ε·N via div_lt_iff₀, and close by nlinarith from the comparison N ≥ N₀ > L/ε (equivalently L/ε < N₀ ≤ N). No RS-specific lemmas are needed; only Mathlib real/nat casting and linear arithmetic.
why it matters
Without arbitrary resolution, the N → ∞ continuum bridge cannot be stated: Laplacian convergence, flat Minkowski limit, and weak-field curvature all presuppose that lattice spacing can be driven below any ε. The module lists this under the proved continuum architecture (finite N-site lattice, spacing a = L/N).
Direct consumer: spacing_eventually_small in UnifiedLatticeManifoldCorrespondence, which is literally this theorem applied to a LatticeRefinement record ("For any target resolution ε > 0, eventually spacing N < ε"). It also feeds the module's master continuum_limit_certificate, which packages signature, causal trichotomy, and related continuum fields.
Framework role: supports the foundational (not phenomenological) continuum limit after DimensionForcing (D = 3) and ZeroParameterGravity, enabling the path from discrete ledger sites to Lorentzian manifold structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.