m2Symbol
plain-language theorem explainer
Closed-form small-momentum ($m^2$) coefficient for the single (1,1) orbit of the 4D Regge Bloch fold, obtained by summing per-slot quadratic coefficients over all 24 slots and 10 triangle types. Gravity analysts cite it when comparing one-orbit TT and gauge rays to the continuum Einstein–Hilbert target. The body is a pure double sum of the slot-level coefficients; no analytic limit is taken here.
Claim. For a $4\times 4$ real mode matrix $H$, the one-orbit $m^2$ symbol is $\sum_{s=0}^{23}\sum_{t=0}^{9} c_{s,t}(H)$, where $c_{s,t}(H)$ is the quadratic slot coefficient built from area-covariant and deficit-kernel pairings of the class coefficients of $H$ (nonzero only on the $(1,1)$ triangle class).
background
This module isolates the $(1,1)$-orbit contribution to the small-momentum symbol of the 4D Regge Bloch fold blochFold11. It never redefines Hessians, kernels, or stencils; those live upstream in the fold module. Along the fixed ray symbolDir = (1,1,0,0), one studies foldAlong H μ := blochFold11 H (μ · symbolDir) and extracts the quadratic coefficient in $μ$.
The building block is the slot coefficient: for each of 24 slots and 10 triangle indices it multiplies an area-covariant class pairing by a deficit-kernel class pairing (with a factor $-1/2$), gated by the $(1,1)$ triangle predicate. Summing those slot values yields the closed-form $m^2$ symbol of this definition.
Module scope is deliberately one orbit only. Landed facts include evenness of the fold along the ray, vanishing at zero on TT-plus and decoy-gauge axes, and the numerical values $-3$ (TT) and $0$ (gauge). The punctured limit foldAlong H μ / μ² → m2Symbol H remains an OPEN Prop.
proof idea
Definitional, not a theorem. The value is the double finite sum $\sum_{s:\mathrm{Fin},24}\sum_{t:\mathrm{Fin},10}$ of the already-defined slot coefficient of $H$. No tactics, no lemmas, no analytic remainder: the symbol is exactly that algebraic aggregate of area and deficit pairings.
why it matters
This coefficient is the banked algebraic witness that the one-orbit $(1,1)$ ray is not the continuum Einstein–Hilbert $m^2$ target. Downstream decoys record m2Symbol(axisTTPlus) = -3 while the frozen EH TT coefficient is $-1/4$, hence inequality; the same symbol vanishes on the decoy gauge mode and is nonzero on the TT-plus axis (nonvacuity).
Algebraic-closer honesty theorems use it to keep ledger flags false: banked one-orbit identities do not flip gap-action recovery or full TT isotropy. Transported-closer and continuum-preflight modules reuse it when separating finite transported symbols from continuum claims. In the Recognition gravity stack it is a local Regge-analysis primitive, not a forcing-chain (T0–T8) step; it supports the open continuum glue without claiming $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.