candidate_m2_axisTTPlus_symbolDir
plain-language theorem explainer
On the plus TT polarization diag(0,0,1,−1) and Bloch symbol direction (1,1,0,0), the distinct-hinge transported second-moment form equals −1/4. Analysts of the 4D Regge continuum face cite this as the raw m² evaluation before Frobenius pin and |k|² scaling (which yields −1/16). Proof is a one-line re-export of the algebraic closer identity.
Claim. The distinct-hinge transported moment form of the unnormalized plus transverse-traceless polarization $E=\mathrm{diag}(0,0,1,-1)$ along the symbol direction $k=(1,1,0,0)$ equals $-1/4$.
background
This module treats the flat second variation of 4D Regge calculus under Schläfli reduction. Gate A2 aims to elevate the nonlinear Regge action to a candidate edge Hessian; the flat Freudenthal closed form and directional Schläfli kill are already theorems, but full off-flat pathwise Schläfli elevation remains open.
The plus TT axis is the unnormalized polarization matrix with sole nonzero entries $E_{22}=1$ and $E_{33}=-1$. The symbol direction is the discrete wavevector $k=(1,1,0,0)$ used for the Bloch symbol of the $m^2$ operator. The distinct-hinge moment form is the quadratic form in the polarization obtained by restricting the all-orbit transported second moment to distinct hinges.
Upstream, the same numerical identity is already proved in the tensor algebraic closer as the evaluation of that quadratic form on this polarization and direction; the present declaration re-exports it into the second-variation module.
proof idea
One-line term-mode wrapper: the goal is definitionally the statement of distinctHingeMomentForm_axisTTPlus_symbolDir from the tensor algebraic closer, which itself reduces to the underlying all-orbit transported distinct-hinge moment evaluation on axis TT plus at the symbol direction. No additional algebra is performed here.
why it matters
Module tier tags list as THEOREM that the Bloch continuum face of the candidate on Frobenius-normalized axis TT at the symbol direction equals $-1/16$, and that this face differs from frozen Einstein-Hilbert $-1/4$. The present identity supplies the raw numerator: distinct-hinge $m^2=-1/4$; after Frobenius pin and division by $|k|^2$ one obtains the continuum-facing coefficient $-1/16$.
That mismatch is intentional diagnostic content. Prior repair paths (distinct-hinge fold isotropy, full two-jet $A_0\cdot K_2$, path-B mean-local, density dictionary) do not close the gap. The residual is Schläfli elevation of the nonlinear action, not another incidence rescale. The result does not flip gap_action_recovery and does not inhabit the 4D EH convergence statement; it pins one concrete face of the candidate Hessian against which those open elevations will be judged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.