e_230101
plain-language theorem explainer
For the six Fin-4 indices (2,3,0,1,0,1), the midpoint Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 256-case kernel identity that underwrites the 4D midpoint M2TT certificate. The proof is a single decide on concrete integers.
Claim. With indices $a=2$, $b=3$, $c=0$, $d=1$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-cell case split proving that the 4D midpoint Regge numerator equals eight times an explicit integer kernel. The ambient setting is discrete gravity analysis: edge and face couplings on a 4-simplex skeleton, with all free indices ranging over $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison object $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern table (typical nonzero entries are $\pm 2$ or $4$). The identity $m_2^{\mathrm{num}}=8,Z$ is the algebraic content of the kernel certificate imported from the parent KernelCert module.
proof idea
One-line kernel decision: both sides evaluate to concrete integers once the six Fin-4 arguments are fixed, so decide closes the equality. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $\mathrm{explicitZ}$ are required.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8,Z$ for all indices, which runs nested fin_cases and dispatches each cell to a chunk lemma of this form. That global identity is the numerical heart of the Regge exact midpoint M2TT certificate in 4D, tying the folded coupling sum to a sparse explicit kernel. In the broader Recognition gravity stack this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8), but it is required before continuum or continuum-limit claims that quote the midpoint kernel can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.