e_012200
plain-language theorem explainer
For the concrete multi-index (0,1,2,2,0,0), the folded Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of 256 kernel cases that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on fully evaluated integers.
Claim. At multi-index $(a,b,c,d,i,j)=(0,1,2,2,0,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-case kernel certification that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. the four discrete directions of a 4D simplicial edge labeling.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on those same six indices (typical values $\pm 2,,4$, and zero off the matched patterns).
The local claim is one sextuple in that table. Upstream, both sides are pure definitions in the kernel-cert module; no analytic hypothesis is left open at this index.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list on the left, the pattern match on the right), and the kernel decides equality of those integers. No lemmas are invoked beyond the evaluators of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhausting indices. That global equality is the algebraic content of the 4D midpoint Regge $M^2$ TT-identity kernel: the folded numerator is exactly eight copies of the explicit Z table.
In the Recognition gravity stack this is bookkeeping, not a new dynamical law. It certifies that the discrete curvature/mass-squared combinatorics used downstream match the closed-form integer kernel, so later continuum or continuum-limit arguments can quote a single clean identity rather than a fold. It does not itself touch T0–T8, RCL, or the phi ladder; it is infrastructure inside the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.