ReggeTTContinuumSymbolIs
plain-language theorem explainer
Packages the continuum TT Bloch symbol as a predicate: Λ is that coefficient for polarization E and integer mode m when discrete TT symbols H_j on tori of side N=j+3, normalized by |k_N|², converge to Λ as N→∞. Anyone citing the ReggeTT continuum program or the open isotropy target uses this object. Pure definition: existence and the value Λ=−1/4 are not asserted here.
Claim. For a real $3\times 3$ matrix $E$ (polarization), an integer wave vector $m\in\mathbb{Z}^3$, and $\Lambda\in\mathbb{R}$, the continuum TT-symbol predicate holds iff there exists a sequence $H:\mathbb{N}\to\mathbb{R}$ such that each $H(j)$ is a TT Bloch symbol of the true nonlinear Regge action on the periodic Freudenthal torus of side $N=j+3$ for $(E,m)$, and $H(j)/|k_{j+3}(m)|^2\to\Lambda$ as $j\to\infty$ (equivalently $k_N=2\pi m/N\to 0$ at fixed direction).
background
This module is Stage 1 of the QG full-theory ReggeTTContinuumSymbol campaign. It defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field: $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum_{\mathrm{tets}}\theta)$, with dihedral angles from Cayley–Menger cofactors. At conformal fields the action recovers the existing linearized Regge action.
The TT Bloch symbol is the second-difference response of that action to a plane-wave edge field at commensurate momentum $k=2\pi m/N$. The continuum object asks what happens when $N\to\infty$ at fixed integer direction $m$, so $|k|\to 0$. Normalization is by the squared lattice momentum (the preflight's momentumNormSq), matching the continuum Fourier convention in which the linearized Einstein–Hilbert TT coefficient is $-1/4$.
C10 numerics (critic-signed) report isotropy with that value on 14 preregistered directions; that evidence is explicitly not a proof. The named open target later in the file quantifies the full claim.
proof idea
Definition only: the body is a Prop built from an existential quantifier over a sequence $H:\mathbb{N}\to\mathbb{R}$. The first conjunct requires each $H(j)$ to satisfy the finite-torus TT Bloch symbol predicate at side $N=j+3$ for the given polarization and mode. The second conjunct is a Filter.Tendsto statement: the $|k|^2$-normalized sequence converges in the usual topology of $\mathbb{R}$ to the candidate continuum coefficient $\Lambda$. No lemmas are applied; no existence or uniqueness is shown.
why it matters
This is the program's target object for the continuum TT symbol. Downstream, the open isotropy target states that for every nonzero integer mode and every TT polarization the predicate holds at $\Lambda=-1/4$ (the linearized Einstein–Hilbert TT coefficient). Closing that target is the kernel goal of the campaign.
A concrete non-vacuity receipt instantiates the closed form at the axis wave vector and the $+$ polarization, asserting the continuum symbol equals $-1/4$ once the open target is discharged. The definition therefore sits between the finite-torus symbol machinery (true Regge action, plane-wave edge fields, TT second differences) and the continuum identification with GR's TT kinetic term. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; its role is gravity-side continuum recovery of the Einstein–Hilbert TT sector on the Freudenthal lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.