e_022223
plain-language theorem explainer
Pointwise identity: the M2 numerator at multi-index (0,2,2,2,2,3) equals eight times the explicit Z kernel at those same Fin-4 slots. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT identity from 256 kernel cells. Proof is a single kernel decide on the concrete integers.
Claim. At indices $(a,b,c,d,i,j)=(0,2,2,2,2,3)$ in $(\mathrm{Fin}\,4)^6$, the folded M2 numerator equals eight times the explicit integer kernel $Z$: $m_2(0,2,2,2,2,3)=8\,Z(0,2,2,2,2,3)$.
background
This module is chunk 2 of the 256-cell kernel certification that the folded M2 numerator equals eight times an explicit integer table $Z$ on $(\mathrm{Fin},4)^6$. The setting is 4D Regge calculus at the exact midpoint: one needs a closed algebraic identity between a coupling-sum numerator and a sparse explicit kernel before continuum or continuum-limit claims.
The numerator $m_2(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six indices. The explicit kernel $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (nonzero only on a short list of index patterns, with values such as $4$ or $-2$).
Chunk theorems pin one concrete six-tuple each so the global $\forall$ statement can be assembled by exhaustive case split on $\mathrm{Fin},4$.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,2,2,2,2,3)$. The left side runs the fold that defines the numerator; the right side multiplies the pattern-matched explicit $Z$ by eight. Both reduce to the same integer, so the equality is discharged by the kernel with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by nested fin_cases. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2–TT identity: without pointwise cells such as this one, the fold-versus-table comparison stays unclosed.
In the Recognition gravity stack this is pure discrete-kernel bookkeeping rather than a forcing-chain landmark (T5–T8). It still matters: continuum or effective-field claims that quote the midpoint M2–TT relation inherit soundness from these 256 decides. The chunk layout (256 kernel cells) is the practical path that keeps each goal inside the decidable fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.