discreteReggeCompletionLimit_zero
plain-language theorem explainer
Any cubic lattice refinement sequence has lattice spacing tending to zero in the epsilon sense: the completion limit of spacing is exactly 0. Gravity and continuum-bridge arguments cite this to pin the discrete-to-manifold limit. The proof is a short term argument: eventual smallness of spacing plus positivity rewrites the absolute deviation from zero.
Claim. For every lattice refinement $R$ (fixed box side $L>0$, spacing $a_N=L/N$), the sequence $a_N$ has completion limit $0$: for every $\varepsilon>0$ there exists $N_0>0$ such that $N\ge N_0$ implies $|a_N-0|<\varepsilon$.
background
The Unified Forcing Chain module aims to force T0–T8 from the Recognition Composition Law and cost normalization. In the gravity layer, continuum emergence is packaged via a cubic lattice refinement: a structure with fixed physical side $L>0$ and spacing $a_N=L/N$ at level $N$.
DiscreteReggeCompletionLimit R ℓ is the standard epsilon form of $\lim_{N\to\infty} a_N=\ell$: for every $\varepsilon>0$ there is $N_0>0$ so that $N\ge N_0$ forces $|a_N-\ell|<\varepsilon$. Upstream, spacing_eventually_small already gives $a_N\to 0$ without the absolute-value packaging, and spacing_pos records $a_N>0$ for $N>0$.
The completion interface from PrimitiveRecognitionCalculus is the broader display/certificate pattern; here the “display” quantity is simply the real spacing sequence of the Regge refinement.
proof idea
Fix $\varepsilon>0$. Apply spacing_eventually_small to obtain $N_0>0$ with $a_N<\varepsilon$ for all $N\ge N_0$. For such $N$, positivity of $N$ follows from $N_0\le N$, so spacing_pos gives $a_N>0$. Rewrite $|a_N-0|$ as $a_N$ via sub_zero and abs_of_pos, then discharge with the eventual-smallness bound. Purely algebraic packaging of an existing limit lemma.
why it matters
This pins the canonical Regge refinement’s continuum limit at zero spacing, the geometric content needed before uniqueness and bridge theorems. Downstream, discreteReggeCompletionLimit_unique_zero uses uniqueness of completion limits to conclude any limit $\ell$ equals $0$. The same fact feeds t5regge_to_continuum_limit_bridge_holds, which packages the T5-to-continuum bridge: weak-field/refinement correspondence is theorem-backed once the discrete Regge side has a zero-spacing completion.
In the forcing chain, T5 forces unique $J(x)=(x+x^{-1})/2-1$. The Regge-to-continuum bridge is how that cost structure is meant to reach continuum gravity. Zero spacing is the elementary geometric half of that bridge; nonlinear Einstein–Hilbert correspondence remains the conditional layer noted in the bridge theorem’s doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.