e_213010
plain-language theorem explainer
At the multi-index (2,1,3,0,1,0) on Fin 4, the folded Regge coupling numerator equals eight times the explicit closed-form kernel entry. Gravity analysts cite it as one cell of the 4D midpoint M2 TT identity. The proof is a single kernel decision on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,0,1,0)$ with each entry in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit 4D midpoint kernel table.
background
This module is chunk 9 of a 256-case kernel certification that the folded numerator of the 4D Regge midpoint M2 TT identity coincides with eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$ on a 4-simplex edge/face pattern.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from 0 and add each contribution evaluated at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for the listed patterns).
The local claim is one concrete sextuple inside that certification grid.
proof idea
One-line kernel proof: decide evaluates both sides as concrete integers (the fold for the numerator at $(2,1,3,0,1,0)$ and eight times the table lookup) and discharges equality by computation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the universal assembly theorem stating that for every sextuple in $(\mathrm{Fin},4)^6$ the folded numerator equals eight times the explicit kernel. That assembly exhausts all indices by nested finite case splits and invokes each chunk cell such as this one. In the Recognition gravity stack this is bookkeeping for the exact midpoint M2 TT identity in 4D Regge analysis, not a new dynamical law; it closes a finite computational obligation so the closed-form kernel can be used downstream without residual folds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.