e_211110
plain-language theorem explainer
At multi-index (2,1,1,1,1,0) the folded Regge midpoint numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on fixed Fin-4 arguments.
Claim. For indices $(a,b,c,d,i,j)=(2,1,1,1,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-point kernel certification that the midpoint Regge $m_2$ numerator equals eight times an explicit integer table $Z$ on $(\mathrm{Fin},4)^6$. The setting is 4D discrete gravity analysis: index sextuples label edge/face couplings in a Regge triangulation at the midpoint configuration.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The companion $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (nonzero only on a sparse set of index patterns, with values such as $\pm 2,\pm 4$).
The local claim is the equality at one concrete sextuple. Sibling theorems cover the other index combinations; together they feed the assembled universal statement.
proof idea
One-line computational proof: decide evaluates both sides at the closed Fin-4 literals $2,1,1,1,1,0$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the pattern-matched $Z$ value by eight. No lemmas beyond the two definitions are invoked; the kernel is small enough for kernel decision.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one case of that case-split, so the assemble step is pure bookkeeping once the 256 decides succeed.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint $M_2$ TT analysis in 4D Regge calculus: it replaces a symbolic fold by a closed integer kernel, enabling later exact identities without residual summation. It does not itself touch the forcing chain (T0–T8), $\phi$, or the eight-tick octave; those enter only if the midpoint kernel is later tied to continuum limits or RS mass/gravity constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.