e_021013
plain-language theorem explainer
For the fixed multi-index $(0,2,1,0,1,3)$ on $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts cite it as one cell of the 4D Regge midpoint $M_2$ identity. The proof is a single kernel `decide` on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the fold of coupling contributions over the fixed coupling list and $Z$ for the explicit integer kernel table, one has $N(0,2,1,0,1,3)=8\,Z(0,2,1,0,1,3)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge-exact midpoint numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. the four spacetime directions.
The numerator $N=\texttt{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\texttt{contrib},t,a,b,c,d,i,j$. The table $Z=\texttt{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for the listed index patterns).
The local claim is one concrete sextuple inside that certification grid.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The proof is the single tactic decide, which asks the kernel to check integer equality after unfolding the fold definition of the numerator and the pattern match of the explicit table. No lemmas beyond those two definitions are invoked.
why it matters
The parent theorem $\texttt{m2Num_eq_eight_explicitZ}$ asserts the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. Each chunk theorem such as this one discharges one branch of that case split, so the assembly can finish without re-deciding the whole grid in one place.
In the Recognition gravity stack this identity is bookkeeping for the Regge midpoint $M_2$ analysis in four dimensions (the $D=3$ spatial forcing of T8 sits upstream of the continuum limit, but this lemma itself is pure finite combinatorics on direction indices). It does not touch the J-cost, $\phi$-ladder, or eight-tick layer directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.