e_213312

This module is chunk 9 of a case-split certification that the midpoint Regge numerator equals eight times an explicit kernel on all of $(\mathrm{Fin},4)^6$. The local slogan is "$\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$, chunk 9 (256 kernel decides)."

The numerator is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The explicit kernel is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).

Both definitions live in the kernel-certificate module imported here. The present declaration fixes one concrete six-tuple and asserts the scalar identity at that point.

One-line kernel proof: by decide. After unfolding the fold that defines the numerator and the pattern match that defines the explicit kernel at $(2,1,3,3,1,2)$, both sides reduce to concrete integers; decide discharges the equality in the integer decidable instance. No lemmas beyond the two definitions are invoked.

Parent theorem is the assembled identity: for all $a,b,c,d,i,j:\mathrm{Fin},4$, the numerator equals eight times the explicit kernel. That proof introduces the six indices and runs fin_cases on each, so every leaf is one of these chunk theorems (including this one).

In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2/TT analysis in 4D Regge calculus: it replaces a folded coupling sum by a closed integer kernel, which is what later curvature and continuum-limit arguments consume. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure inside the gravity analysis layer.