m2TransportedAllOrbitMomentDistinctHinge
plain-language theorem explainer
Defines the distinct-hinge all-orbit m² moment: a sum over the six hinge orbit types of each transported orbit moment, weighted by the reciprocal star size 1/r_τ. Gravity analysts cite it as the continuum-facing multi-orbit fold that matches mean-local incidence and feeds the frozen EH value −1/4 on axisTTPlus. The body is a one-line weighted Finset sum over HingeOrbitType.
Claim. For a $4\times 4$ real matrix $H$ and a direction $d:\{0,1,2,3\}\to\mathbb{R}$, the distinct-hinge all-orbit $m^2$ moment is $\sum_{\tau} r_\tau^{-1}\, m^2_\tau(H,d)$, where the sum runs over the six hinge orbit types $\tau$, $r_\tau$ is the geometric star size of type $\tau$, and $m^2_\tau$ is the transported orbit moment of that type.
background
The module builds a continuum-facing multi-orbit Bloch fold in 4D Regge analysis. Each slot transports its orbit seed area covector and star deficit kernel by the orbit covering permutation (first $S_4$ cover of the orbit representative). The six lattice orbit types under coordinate permutation are $t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}$.
Geometric star size $r_\tau$ is fixed by the star modules and paper table: $(1,1)\mapsto 6$, $(1,2)\mapsto 4$, $(2,1)\mapsto 4$, $(1,3)\mapsto 6$, $(3,1)\mapsto 6$, $(2,2)\mapsto 4$. The per-orbit moment $m^2_\tau(H,d)$ sums transported slot coefficients over the 24 covering slots and 10 dual indices. The matrix type is ordinary $4\times 4$ real matrices.
Module status stresses that transport must use the covering permutation, not the factorized $(1,1)$-only transport: measured all-orbit $m^2$ along the symbol direction on axisTTPlus is $-5/2$ raw, not the factorized $0$.
proof idea
Pure definition: expand as the sum over all six hinge orbit types of the reciprocal star size times the already-defined transported orbit moment for that type, matrix, and direction. No tactics or lemmas; the body is the weighted aggregate itself.
why it matters
This is the distinct-hinge fold weight $1/r_\tau$ named in the module status block. Downstream, distinctHingeMomentForm packages it as a quadratic form in the polarization; local-incidence theorems prove the mean-local all-orbit moment equals this quantity, so Path B cannot repair $e_0$ anisotropy. Homogeneity under $H\mapsto cH$ is quadratic. The open evaluation target on axisTTPlus/symbolDir is the frozen Einstein–Hilbert value $-1/4$ (closed in the sibling M2Eval module). It sits inside the 4D Regge–Bloch gravity stack feeding continuum EH isotropy work; residual $2/N^4$ cell-sum dictionary and all-orbit $m^2$ Tendsto remain open. Does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.