FactorizedMomentEqualsEH
plain-language theorem explainer
Records the Prop that the factorized all-orbit torus moment polynomial equals the frozen Option-C Einstein–Hilbert face on every nonzero TT mode. Anyone tracking the factorized-versus-transported fold in the 4D continuum closure would cite it. Pure definition of an equality shape; no proof content, and it does not by itself discharge the iterated continuum Tendsto target.
Claim. For every nonzero integer mode $m\in\mathbb{Z}^4$ and every $4\times 4$ real matrix $E$ that is symmetric, Euclidean-traceless, and transverse to $m$, the factorized all-orbit moment polynomial of $E$ along the real direction of $m$ equals the scale-explicit Option-C Einstein–Hilbert continuum face of $E$.
background
The ambient module builds the canonical Recognition mesh on the periodic Freudenthal 4-torus and attaches a value-level exact-$J$ action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol. Preferred limit shape is amplitude Hessian at fixed mesh, then mesh side $N\to\infty$.
Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$ on the side-$N$ torus; intModeDir views $m$ as an unnormalized real covector. Algebraic TT means $E$ is symmetric, traceless, and transverse to that covector. The right-hand side continuumEHScaleExplicitFace is the frozen Option-C EH coefficient (Frobenius-norm gate of the exact flat Hessian). The left-hand side is the factorized all-orbit moment polynomial from the Bloch symbol assembly.
The genuine continuum target is the separate Prop that amplitude Hessians on the canonical mesh family, after $|k|^2$ normalization, Tendsto that same EH face. The present definition is only a parallel equality shape on the factorized scaffold.
proof idea
No proof: the declaration is a bare Prop abbreviation. It packages the universal quantifiers (nonzero integer mode, TT matrix) and the single equality between the factorized all-orbit moment polynomial and the scale-explicit EH face. Downstream work is expected to either assume this Prop as a named hypothesis or replace it by a transported-moment equality of the same shape.
why it matters
In the QG full-theory campaign this module is the Recognition gate of the 4D continuum closure. The real theorem-shaped target is iterated continuum convergence of exact-$J$ amplitude Hessians to the Option-C EH face. The factorized moment polynomial is a convenient scaffold, not the transported continuum object, so this Prop deliberately does not discharge that Tendsto statement (open fold: factorized versus transported).
It is recorded so a future transported-moment equality can be swapped in with the same interface, matching the shape of the older dictionary-constant theorem. It sits beside the mesh true-Regge Hessian identification and the exact midpoint $m^2$ TT/gauge faces, without flipping gap-action recovery or inhabiting the full $S_{RS}\to\mathrm{EH}$ 4d statement. No downstream consumers are wired yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.