DiscreteReggeCompletionLimit
plain-language theorem explainer
Defines the ε–N completion limit for a discrete Regge lattice refinement: spacing at level N converges to a real target ℓ. Gravity and continuum-bridge arguments cite it to state that the mesh goes to a continuum spacing (classically zero). The body is the standard metric limit predicate on the refinement’s spacing sequence.
Claim. For a lattice refinement $R$ and a real number $\ell$, the discrete Regge completion limit holds when $\mathrm{spacing}_R(N)\to\ell$ as $N\to\infty$: for every $\varepsilon>0$ there exists $N_0\ge 1$ such that for all $N\ge N_0$, $|\mathrm{spacing}_R(N)-\ell|<\varepsilon$.
background
The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law, normalization, and calibration. Mid-chain, T5 forces the unique J-cost $J(x)=(x+x^{-1})/2-1$; continuum gravity is reached by completing discrete Regge-type actions built from that cost.
A lattice refinement packages a nested discrete geometry whose mesh size is the real sequence $\mathrm{spacing}(N)$. The continuum stage needs a precise notion that this mesh settles to a fixed length $\ell$. That is ordinary sequential convergence in $\mathbb{R}$, written in $\varepsilon$–$N$ form so uniqueness and identification of the limit are elementary analysis.
Upstream lattice–manifold correspondence supplies the refinement type and the spacing field (including eventual smallness for the canonical family). Related continuum bridges identify discrete ledger/Laplacian actions with continuum surface terms; this definition only records the metric completion of the mesh, not the action identity itself.
proof idea
Definitional, not a proved theorem. The predicate is the standard $\varepsilon$–$N$ limit of the real sequence $N\mapsto R.\mathrm{spacing},N$ toward $\ell$, with the minor side condition $N_0>0$. No lemmas are invoked in the body; downstream theorems discharge instances by quoting eventual smallness of spacing (for $\ell=0$) or by uniqueness of limits in $\mathbb{R}$.
why it matters
Pins the continuum-completion language used after T5’s unique J-cost is transported into nonlinear Regge form. Downstream, zero is shown to be a completion limit for any such refinement, limits are unique, and therefore every completion limit is zero. Those facts feed the Regge/J-cost → continuum completion bridge certificate, which packages the discrete action surface as the object being completed.
In the forcing chain this is scaffolding for the discrete-to-continuum step between unique $J$ (T5) and the geometric side of the later T7–T8 octave and dimension story: continuum spacing must be forced, not assumed. It does not itself force $D=3$ or $\varphi$; it only makes the mesh limit a first-class proposition the bridge can name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.