continuumSymbolIs_unique
plain-language theorem explainer
If the |k|²-normalized exact-action Regge mesh sequence on the side-(j+3) 4-torus tends to two real values for a fixed integer mode and polarization matrix, those values coincide. Anyone arguing continuum recovery or excluding decoy faces cites this uniqueness. The proof is a one-line application of uniqueness of limits in a Hausdorff space.
Claim. Let $m\in\mathbb{Z}^4$ be an integer wave mode and $E$ a $4\times 4$ real matrix. If the $|k|^2$-normalized exact-action continuum sequence (along torus side $N=j+3$) tends to both $\Lambda_1$ and $\Lambda_2$ in $\mathbb{R}$, then $\Lambda_1=\Lambda_2$.
background
This module is the first binding increment of the 4D continuum closure plan for Regge gravity. It freezes the independent continuum target, the canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, Frobenius-normalized TT data, and honesty decoys before any recovery claim. Nothing in the module proves continuum recovery of Einstein–Hilbert.
An integer mode $m$ is a map $\mathrm{Fin},4\to\mathbb{Z}$ (commensurate Bloch wavevector on the torus). The real covector is $k=2\pi m/N$. The continuum-symbol predicate asserts that $$j\mapsto \frac{\mathrm{finiteExactMidpointBlochSymbol}(j,m,E)}{|k(N=j+3,m)|^2}$$ tends to a real $\Lambda$ as $j\to\infty$. The sequence is definitionally the concrete exact-action Hessian fold, not a constant face and not the legacy transported hinge fold.
Uniqueness of that limit is elementary analysis once the predicate is a Tendsto into nhds, but it is banked here so later exclusion and closer lemmas can name a single continuum value.
proof idea
One-line term proof: apply Mathlib's tendsto_nhds_unique to the two Tendsto hypotheses. Neighborhood filters in $\mathbb{R}$ are Hausdorff, so a net (here the exact-action mesh sequence indexed by $j$) has at most one limit. No Regge-specific algebra is used.
why it matters
In the QG continuum preflight, symbol uniqueness is listed among the THEOREM-tier pins (with Frobenius pin lemmas and decoy discriminators). Downstream, continuumSymbolIs_unique_limit re-exports it into the transported algebraic closer, and mesh_sequence_does_not_converge_to_eh_face uses it to exclude the Einstein–Hilbert face: the limit exists, is unique, and equals the Regge face rather than the frozen EH coefficient on any nonzero TT mode with positive Frobenius mass.
That exclusion is the honesty gate for the still-OPEN continuum Tendsto props (Regge4DContinuumEHTarget, gauge-zero) and the uninhabited S_RS_converges_EH_4d. The module insists the EH quadratic is frozen independently of the lattice symbol; uniqueness prevents fitting a scale or double-booking two continuum values. Framework context is 4D Regge weak-field analysis toward continuum recovery, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.