discreteReggeCompletionLimit_unique_zero
plain-language theorem explainer
Any epsilon-limit of the spacing sequence of a canonical discrete Regge lattice refinement must be zero. Continuum-bridge and T5-to-Regge arguments cite this to pin the refinement endpoint. The proof is a two-premise uniqueness application: the given limit equals the already-established zero limit.
Claim. Let $R$ be a lattice refinement and $\ell\in\mathbb{R}$. If $\ell$ is a completion limit of $R$ in the epsilon sense (for every $\varepsilon>0$ there is $N_0>0$ such that $N\ge N_0$ implies $|R.\mathrm{spacing}(N)-\ell|<\varepsilon$), then $\ell=0$.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T5 forces the unique J-cost $J(x)=(x+x^{-1})/2-1$; continuum gravity is reached by a discrete Regge refinement whose mesh spacing is driven to a completion limit.
A lattice refinement $R$ carries a spacing sequence $R.\mathrm{spacing}:\mathbb{N}\to\mathbb{R}$. The predicate DiscreteReggeCompletionLimit states the standard epsilon-form limit: $\ell$ is a completion limit when spacings eventually stay within every positive $\varepsilon$ of $\ell$. Upstream, uniqueness of such limits for a fixed $R$ is already proved, and zero is exhibited as one completion limit of the canonical refinement.
Several cost notions (observer J-cost, multiplicative-recognizer cost, PRC quotient cost) sit in the dependency cone but are not invoked in the body; they only locate the result inside the cost-founded continuum bridge.
proof idea
Term-mode one-liner. Apply the uniqueness theorem for completion limits of a single refinement $R$ to the two witnesses: the hypothesis that $\ell$ is a completion limit, and the theorem that zero is a completion limit of $R$. Uniqueness forces $\ell=0$. No epsilon chasing is redone here.
why it matters
This pins the continuum endpoint of the canonical Regge mesh: the only admissible spacing limit is the zero-spacing completion. Downstream it is consumed by the T5 Regge-to-continuum bridge certificate, whose doc-comment records that the continuum bridge is theorem-backed in the weak-field/refinement layer (and remains conditional in the full nonlinear Einstein–Hilbert layer).
In the forcing chain this sits under T5 (unique J) as the discrete-to-continuum handoff: once J is forced, Regge actions built from that cost refine to a unique continuum limit at vanishing spacing. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those are T6–T8. It closes the uniqueness half of the refinement story so the bridge can quote a single endpoint rather than a set of candidate limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.