M2TransportedAllOrbitAxisSymbolDirEvalOpen
plain-language theorem explainer
Names the proposition that the raw transported all-orbit m² moment, on the plus TT axis diag(0,0,1,−1) along symbol direction (1,1,0,0), equals −5/2. Gravity analysts cite it when matching discrete Regge–Bloch folds to continuum Einstein–Hilbert curvature. The equality itself is proved in the sibling M2Eval module; this declaration only packages the claim as a Prop.
Claim. The raw transported all-orbit second moment of the 4D Bloch fold, evaluated on the plus TT polarization $\mathrm{diag}(0,0,1,-1)$ along the symbol direction $(1,1,0,0)$, equals $-5/2$.
background
This module builds a continuum-facing multi-orbit fold: each hinge-orbit slot transports its seed area covector and star deficit kernel by the orbit covering permutation (first $S_4$ cover of orbit representatives). The raw all-orbit m² moment is the sum over hinge-orbit types of the transported orbit moments.
The plus TT axis is the unnormalized polarization matrix with only the $(2,2)$ and $(3,3)$ entries nonzero ($+1$ and $-1$). The symbol direction is the covector $(1,1,0,0)$ on $\mathrm{Fin},4$. Module status records that the measured all-orbit m² along this pair is $-5/2$ raw (orbit slices $t_{11}=-3$, $t_{12}=+2$, $t_{13}=-3/2$), not the factorized value $0$; one must not use the non-transported permutation for non-$(1,1)$ orbits.
After division by $|\mathrm{symbolDir}|^2$ the raw value becomes $-5/4$. A distinct-hinge weight $1/r_\tau$ further upgrades the axis value to $-1/4$ (path A toward Einstein–Hilbert).
proof idea
Definitional packaging only: the body is the equality of the summed transported orbit moment on the plus TT axis and symbol direction with the constant $-5/2$. No tactics run here. Discharge is one-line in the sibling eval module, which applies the already-proved evaluation lemma for that axis/direction pair.
why it matters
Pins the numerical target that the transported all-orbit fold must hit before continuum matching. Downstream, M2TransportedAllOrbitAxisSymbolDirEvalOpen_holds proves the Prop by invoking the axis/symbolDir evaluation. That closes the raw m² eval listed under module THEOREM status and feeds the distinct-hinge upgrade to frozen EH $-1/4$ ($-3/6+2/4+(-3/2)/6$).
The residual open work is all-orbit m² Tendsto and continuum EH isotropy: a 3D-style $2/N^4$ cell-sum dictionary is still required. The declaration does not flip gap-action recovery. In the broader RS gravity stack it is a discrete curvature checkpoint on the path from Regge hinges to continuum Einstein–Hilbert, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.