Regge4DFullTTIsotropyTarget
plain-language theorem explainer
Names the open full TT-isotropy goal for 4D Regge continuum recovery: every nonzero mode and Frobenius-normalized TT polarization must give continuum symbol equal to the Einstein–Hilbert TT coefficient −1/4. Gravity auditors cite it as the first conjunct of the algebraic closer package. The body is a one-line alias of the preflight continuum EH target.
Claim. Define the full TT-isotropy target as the proposition that for every nonzero integer 4-mode $m$ and every matrix $E$ that is transverse-traceless with respect to the real direction of $m$, the continuum Regge symbol of $(m,E)$ equals the scale-explicit Einstein–Hilbert face $\bigl(-\tfrac18\bigr)\|E\|_F^2$ (equivalently the frozen coefficient $-1/4$ after $|k|^2$-normalization on unit TT polarizations).
background
This module is the 4D algebraic closer for the quantum-gravity full-theory campaign: it banks available algebraic witnesses (decoy orbit symbols, plus/cross TT witnesses, gauge vanishing, zero-momentum full-moment identities) and packages the remaining continuum goals as named open propositions with status flags false.
The continuum EH target from preflight asserts: for every nonzero integer mode $m$ and every TT matrix $E$ relative to the real wavevector of $m$, the continuum symbol equals the scale-explicit face $(-1/8)\cdot|E|F^2$. Pure-gauge vanishing is kept as a separate conjunct. The module disclosures stress that the continuum object is the concrete transported sequence, not a factorized all-orbit Bloch symbol, and that this layer does not prove $S{\mathrm{RS}}$ converges to EH in 4D.
TT means transverse-traceless polarization in the 4D edge/hinge Regge setting; the frozen coefficient $\mathrm{einsteinHilbertTTCoefficient4D}=-1/4$ is the numerical face those symbols must hit after $|k|^2$ normalization.
proof idea
Definitional alias, not a proved theorem. The right-hand side is exactly Regge4DContinuumEHTarget from the continuum preflight module, so the Prop is definitionally that universal quantification over nonzero modes and TT matrices. No tactics, no lemmas applied beyond unfolding the name.
why it matters
First conjunct of Regge4DAlgebraicCloserTarget, which packages full TT isotropy, pure-gauge vanishing, and plus–cross agreement as the open algebraic closer. Downstream, fullTTIsotropyTarget_mentions_eh_coefficient records that the frozen coefficient is $-1/4$ and that this name is definitionally the preflight EH target, so status tracking stays tied to the numerical face auditors expect.
In the Recognition gravity stack this is the 4D counterpart of the TT algebraic closer: it sits between banked orbit/Hessian witnesses and the still-open finite-momentum transported continuum limit. Closing it is necessary (with the other two conjuncts) before any claim that the Regge discrete action recovers continuum Einstein–Hilbert TT kinetics; the module explicitly does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.