ReggeTTContinuumIsotropyTarget
plain-language theorem explainer
Named open target packaging continuum isotropy of the true Regge TT Bloch symbol: every nonzero integer wave vector and every TT polarization yields continuum symbol value exactly -1/4 (linearized Einstein-Hilbert TT coefficient). Cited by the continuum closer and the preflight status record. Pure Prop definition of the ReggeTTContinuumSymbol program's kernel goal; no proof content here.
Claim. The proposition that for every nonzero integer wave vector $m\in\mathbb{Z}^3$ and every TT polarization $E$ (symmetric, traceless, transverse to $m$, Frobenius-normalized to $1$), the continuum TT Bloch symbol of the true nonlinear Regge action at $(E,m)$ exists and equals the constant $-\frac{1}{4}$.
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 matches the existing frozen Regge action.
A TT polarization for integer wave vector $m$ is a real $3\times 3$ matrix that is symmetric, traceless, transverse to $m$, and Frobenius-normalized. The continuum symbol object ReggeTTContinuumSymbolIs asserts existence of a sequence of finite-$N$ TT Bloch symbols converging to a prescribed coefficient. The constant reggeTTContinuumCoefficient is fixed at $-1/4$, the linearized Einstein-Hilbert TT value in these conventions.
Supporting evidence for isotropy is numerical only (C10 probe): isotropic $K(0)=-(1/4)I_{\mathrm{TT}}$ on 14 preregistered directions. This Prop is the named open target; its status flag in the preflight record is false until closed elsewhere.
proof idea
Definitional packaging only: the body is the universal quantification over nonzero $m:\mathrm{Fin},3\to\mathbb{Z}$ and matrices $E$, with hypotheses $m\neq 0$ and TT polarization, concluding that the continuum symbol predicate holds at coefficient $-1/4$. No tactics, no lemmas applied, no existence construction. Downstream closers discharge the Prop by exhibiting a concrete finite-$N$ family (canonical reduced second-variation symbols) and taking the continuum limit.
why it matters
Kernel goal of the ReggeTTContinuumSymbol program: continuum recovery of linearized Einstein-Hilbert TT dynamics from the true nonlinear 3D Regge action on the Freudenthal lattice. Downstream, reggeTTContinuumIsotropyTarget_closed asserts the Prop holds, superseding C10/C8 numerics by kernel proof at 3D action strength; canonicalFiniteH_TTBlochSymbolIs supplies the finite-$N$ witnesses used in that closer. The preflight status structure records this target as the remaining OPEN item after flat-point, conformal identification, and symbol well-formedness theorems. In the broader RS gravity stack this is the continuum-isotropy gate for lattice gravity matching GR's TT sector in $D=3$ spatial dimensions (forcing chain T8), not a mass or alpha claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.