discreteReggeCompletionLimit_unique
plain-language theorem explainer
If a single discrete Regge lattice refinement has two completion limits for its spacing sequence, those limits coincide. Continuum-recovery and zero-mode arguments that treat the refined spacing as converging cite this uniqueness. The proof is a standard ε/3 triangle-inequality contradiction on the absolute difference of the two candidate limits.
Claim. Let $R$ be a lattice refinement with spacing map $N\mapsto s_R(N)\in\mathbb{R}$. Say $\ell\in\mathbb{R}$ is a completion limit of $R$ when for every $\varepsilon>0$ there is $N_0\ge 1$ such that $|s_R(N)-\ell|<\varepsilon$ whenever $N\ge N_0$. If $\ell_1$ and $\ell_2$ are both completion limits of the same $R$, then $\ell_1=\ell_2$.
background
The ambient module is the Unified Forcing Chain: T-1 through T8 are derived as inevitabilities from the Recognition Composition Law plus normalization and calibration. Gravity enters via the lattice-to-manifold correspondence: a lattice refinement $R$ supplies a spacing sequence $s_R(N)$ that is meant to approach a continuum edge length under successive refinement.
The predicate at issue is the ε-form completion limit: $\ell$ is a completion limit of $R$ when $s_R(N)\to\ell$ in the usual real sense (for every $\varepsilon>0$ an $N_0>0$ eventually keeps $|s_R(N)-\ell|<\varepsilon$). That is exactly the discrete Regge analogue of ordinary sequential convergence of mesh size.
Uniqueness of such limits is the elementary real-analysis fact needed before one can identify "the" continuum spacing attached to a given refinement sequence. Downstream, the same module pins that unique value to zero for the canonical refinement.
proof idea
Argue by contradiction. Assume $\ell_1\ne\ell_2$ and set $d:=|\ell_1-\ell_2|>0$, $\varepsilon:=d/3>0$. Apply each completion-limit hypothesis at this $\varepsilon$ to obtain thresholds $N_1,N_2$. At $N:=\max(N_1,N_2)$ both $|s_R(N)-\ell_1|<\varepsilon$ and $|s_R(N)-\ell_2|<\varepsilon$. Rewrite $\ell_1-\ell_2=-(s_R(N)-\ell_1)+(s_R(N)-\ell_2)$ and use the triangle inequality (with $|{-}a|=|a|$) to get $d\le|s_R(N)-\ell_1|+|s_R(N)-\ell_2|$. The right-hand side is strictly less than $2\varepsilon=2d/3$, hence less than $d$, a contradiction. No external lemmas beyond basic absolute-value and order facts are required.
why it matters
This lemma is the uniqueness half of continuum recovery for discrete Regge refinements inside the forcing chain. Its sole recorded consumer is discreteReggeCompletionLimit_unique_zero, whose doc-comment states: any completion limit of the canonical Regge refinement is the zero-spacing completion. That zero identification is the bridge from a discrete lattice with positive mesh to a continuum geometry with vanishing spacing, which is the gravity-side counterpart of T2 (discreteness forced by cost) meeting the lattice-manifold correspondence.
In the broader T0-T8 narrative, continuum limits must be single-valued before one can speak of a forced continuum geometry, eight-tick octave structure on the continuum side, or $D=3$ spatial dimensions recovered from discrete data. Without uniqueness, "the" completion length would be ambiguous and zero-mode / hinge-aware continuum statements would not be well-posed. The result itself is pure real analysis; its place in the framework is as the gate that lets the canonical refinement's spacing be named and set to zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.