e_010223
plain-language theorem explainer
Pointwise identity: the folded Regge M2 numerator at multi-index (0,1,0,2,2,3) equals eight times the explicit integer kernel value at those same indices. Gravity analysts cite it as one cell of the 256-case kernel table that builds the global numerator identity. Proof is a single kernel decision on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,2,2,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel integer: $m_2^{\mathrm{num}}(0,1,0,2,2,3)=8\,Z_{\mathrm{expl}}(0,1,0,2,2,3)$.
background
This module is chunk 1 of a 256-cell kernel certification that the 4D Regge midpoint M2 TT numerator matches an explicit closed form: $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on every multi-index in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at those six indices. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local setting is pure finite enumeration: no continuum limit, no floating arithmetic. Upstream definitions supply only the fold and the table; each chunk theorem pins one concrete six-tuple.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed indices $(0,1,0,2,2,3)$ and checks integer equality. The left side reduces by unfolding the fold over the coupling list; the right side reduces by unfolding the explicit table and multiplying by eight. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all six indices, which exhausts $(\mathrm{Fin},4)^6$ by case split and consumes the chunk cells. That global identity is the algebraic core of the Regge exact midpoint M2 TT certification in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, such kernel equalities underwrite discrete curvature bookkeeping before continuum or phenomenological layers. This cell is scaffolding for the assembled identity, not a standalone physical law; its value is coverage of one multi-index in the complete table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.