e_211322
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (2,1,1,3,2,2) equals eight times the explicit kernel value at that same index. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ theorem. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,1,3,2,2)$ with each coordinate in $\{0,1,2,3\}$, the folded integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-cell decide grid establishing $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint Regge analysis of the 4D M2 TT identity in the Gravity.Analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The comparison target $Z$ is an explicit integer-valued kernel on the same six indices, given by a finite pattern-match table (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the KernelCert module imported here. The present declaration fixes one concrete cell of that table.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(2,1,1,3,2,2)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit kernel.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six Fin-4 indices, which exhausts the index space by nested fin_cases and consumes the chunk cells (including this one). That global identity is the algebraic backbone of the Regge exact-midpoint M2 TT certification in 4D: it replaces a folded coupling sum by a closed kernel, so later curvature and mass-ladder arguments can quote a single explicit integer table rather than a fold.
Within Recognition Science gravity work this is pure scaffolding discharge, not a new physical law. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder; those enter only once the certified kernel is plugged into continuum or continuum-limit statements downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.