Regge4DContinuumEHTarget
plain-language theorem explainer
Names the open continuum target for 4D Regge gravity: on every nonzero lattice mode and every transverse-traceless polarization, the continuum symbol must equal the independently frozen Einstein-Hilbert face (−1/8) times the Frobenius norm squared of the polarization. Continuum-limit and algebraic-closer authors cite it as the TT half of weak-field EH recovery. It is a pure Prop definition (Restatement C), not a proof.
Claim. For every nonzero integer 4-mode $m$ and every $4\times 4$ matrix $E$, if $E$ is transverse-traceless with respect to the real momentum of $m$, then the continuum Regge symbol of $(m,E)$ equals the scale-explicit Einstein-Hilbert face $(-1/8)\,\|E\|_F^2$.
background
The module freezes the weak-field continuum contracts for 4D Regge calculus before any recovery proof: a canonical periodic Freudenthal 4-torus of side $N\ge 3$, Frobenius-normalized Euclidean TT polarizations, and an independently defined linearized Einstein-Hilbert quadratic (via kappa_einstein, not a free lattice scale). Continuum recovery is deliberately left open.
The continuum symbol is the $|k|^2$-normalized exact flat cross-term fold (not the legacy distinct-hinge or bare Bloch folds). The target face is the explicit EH coefficient on TT data: $(-1/8)$ times the Frobenius norm squared of the polarization matrix. Pure-gauge vanishing is a separate conjunct.
IsTT encodes the transverse-traceless gate on the real momentum of the integer mode. The definition packages Restatement C of the preflight: symbol equals that frozen face on every nonzero mode and every TT polarization.
proof idea
Definition only: the body is the universal Prop quantifying over nonzero integer modes and Mat4 polarizations, requiring TT, and asserting continuum-symbol equality to the scale-explicit EH face. No tactics, no lemmas discharged.
why it matters
This is the named OPEN TT half of 4D continuum EH recovery in the QG full-theory campaign. Downstream, S_RS_converges_EH_4d packages it with the pure-gauge zero target as the ledger closer for weak-field quadratic action convergence (not nonlinear GR, not sourced EFE). Algebraic closers alias it as full TT isotropy and prove that full isotropy implies the frozen coefficient $-1/4$ (via the bookkeeping $2\cdot(-1/8)=-1/4$).
It also anchors status flags and decoy discriminators: Schläfli-elevation and distinct-hinge factor-4 Props are defined relative to this target so that wrong faces (e.g. $-1/16$) are falsifiable against the independently frozen EH quadratic. The module insists the EH face is never reverse-engineered from lattice weights; later closers must observe equality.
In the broader RS gravity stack this is the continuum binding increment after edge/TT decomposition and exact flat Hessian symbols, still short of inhabiting the Tendsto Props.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.