e_311222
plain-language theorem explainer
For the single multi-index (3,1,1,2,2,2) in (Fin 4)^6, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 kernel decides that assemble the global m2Num = 8·explicitZ identity. The proof is a one-line decide on closed integer arithmetic.
Claim. At multi-index $(a,b,c,d,i,j)=(3,1,1,2,2,2)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$, labeling discrete 4D edge/vertex slots in the Regge calculus setup.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a local contribution over every term in couplingZList. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern of integer values (examples include $4$ on diagonal pairs such as $(0,0,1,1,2,2)$ and $-2$ on crossed pairs such as $(0,0,1,2,1,2)$).
The local claim is exactly one sextuple evaluation of the asserted identity $m_2^{\mathrm{num}}=8\cdot Z$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 indices are substituted into the fold definition of the numerator and the pattern-matching definition of the explicit kernel, so the kernel decision procedure closes the equality with no further lemmas.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one concrete cell of that $4^6=4096$-free but kernel-tabulated grid (here the 256 decides of chunk 13).
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge $M^2$ TT analysis in 4D: it replaces a folded coupling sum by a closed integer table, so later curvature and mass-ladder arguments can quote a single explicit kernel rather than re-sum contributions. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure discrete-kernel certification underneath those layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.