distinctHingeMomentForm_axisTTPlus_e0Dir
plain-language theorem explainer
On the unnormalized plus TT polarization diag(0,0,1,−1), the distinct-hinge transported m² moment vanishes when the Bloch direction is the time axis e₀. Gravity analysts cite it when tabulating closed ray evaluations of the 4D Regge quadratic form. The proof is a one-line wrapper renaming the already-proved M2Eval identity.
Claim. For the unnormalized plus transverse-traceless polarization $E_+=\mathrm{diag}(0,0,1,-1)$ and the coordinate direction $e_0=(1,0,0,0)$, the distinct-hinge transported $m^2$ moment equals zero: $Q_{\mathrm{dh}}(E_+,e_0)=0$.
background
This module is the 4D counterpart of the 3D Regge TT algebraic closer. It banks the transported distinct-hinge $m^2$ as a quadratic form $Q_{\mathrm{dh}}(E,\mathrm{dir})$ on the TT variety, with every closed ray evaluation available today, while a universal adjugate-style tensor contraction remains open.
distinctHingeMomentForm is exactly that quadratic form: it aliases m2TransportedAllOrbitMomentDistinctHinge. The plus axis mode axisTTPlus is the unnormalized matrix $\mathrm{diag}(0,0,1,-1)$. The direction e0Dir is the pure time unit vector $(1,0,0,0)$ in $\mathbb{R}^4$.
Upstream, the M2Eval layer already evaluates the six-orbit sum for this pair and proves the moment is zero by reducing each orbit contribution. The module doc records the banked table: on $e_0$, plus gives $0$ and cross gives $-1/8$ (normalized $-1/16$).
proof idea
One-line wrapper. The definition of the quadratic form is definitional equality with m2TransportedAllOrbitMomentDistinctHinge, so the claim is identical to the upstream theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir, which is applied directly. That upstream proof unfolds the all-orbit moment, splits the six orbits, and simplifies each transported orbit contribution along $e_0$ for the plus polarization.
why it matters
Fills one cell of the banked ray table in the Regge 4D tensor algebraic closer: plus polarization on $e_0$ is the vanishing entry. The module theorem list explicitly records "$e_0$Dir plus $0$, cross $-1/8$"; this declaration is the plus half under the quadratic-form alias.
No used_by edges are recorded yet; siblings cover the cross/$e_0$ and symbolDir rays and the continuum-face normalizations. The open items it supports by tabulation are Regge4DDistinctHingeTensorClosedFormOpen (universal bilinear form matching all TT/nonzero-dir rays) and the residual factor-4 comparison to Einstein–Hilbert continuum faces. It does not address gap_action_recovery or install any magic-4 multiplier.
In the broader RS gravity stack this is pure continuum/Regge analysis scaffolding, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.