M2DistinctHingeAxisSymbolDirEvalOpen_holds
plain-language theorem explainer
The distinct-hinge transported all-orbit second moment of the Regge–Bloch curvature probe, on the TT-plus axis against the symbol direction, equals the frozen Einstein–Hilbert value −1/4. 4D discrete-gravity analysts cite this when matching orbit sums to continuum EH. Proof is a one-line wrapper that discharges the open Prop by the already-proved six-orbit evaluation.
Claim. The distinct-hinge weighted transported all-orbit moment $m^2$, evaluated on the TT-plus axis polarization in the symbol direction, equals $-1/4$ (equivalently $-3/6 + 2/4 + (-3/2)/6$).
background
This module closes transported all-orbit $m^2$ certificates for Regge–Bloch 4D analysis. The distinct-hinge variant folds each orbit contribution by the reciprocal hinge radius $1/r_\tau$, rather than the raw unweighted sum. On the TT-plus axis against the symbol direction the target value is the frozen Einstein–Hilbert number $-1/4$.
Orbit slices on plus are already certified: $t_{11}=-3$, $t_{12}=+2$, $t_{13}=-3/2$, and $t_{21}=t_{31}=t_{22}=0$. The open Prop M2DistinctHingeAxisSymbolDirEvalOpen simply asserts that the distinct-hinge moment equals $-1/4$; the computational theorem that sums the six orbits lives in the same module and is the sole nontrivial dependency.
Decoy-gauge vanishing remains zero under the same weighting. Plus and cross axes agree on the symbol direction after the $1/r_\tau$ fold, while they disagree on the bare $e_0$ ray.
proof idea
One-line wrapper that applies the computational theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir. That theorem unfolds the distinct-hinge moment definition, rewrites via the six-orbit sum identity, and simplifies the orbit star-size factors to obtain the rational $-1/4$. No further arithmetic is performed at this site.
why it matters
Closes the distinct-hinge certificate named in the module header for axisTTPlus / symbolDir, matching the frozen EH value quoted as $-3/6+2/4+(-3/2)/6$. Together with the parallel cross-axis certificate it shows that the $1/r_\tau$ fold restores plus/cross agreement on the symbol direction (both give $-1/4$; normalized raw both give $-1/8$).
Downstream continuum-isotropy work still faces the open blockage on the bare axis-aligned $e_0$ mode, and the full cosine two-jet does not repair $e_0$ anisotropy or plus vanishing. The module explicitly does not flip gap_action_recovery. No further used-by edges are recorded yet; the declaration is a status latch for the evaluation suite and external probe receipts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.