e_013230
plain-language theorem explainer
Pointwise check that the folded M2 numerator equals eight times the explicit Z table at multi-index (0,1,3,2,3,0) in (Fin 4)^6. Gravity analysts cite it as one of 256 kernel cells feeding the assembled identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,3,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 table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint M2/TT identity kernel, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given multi-index. The comparison target is an explicit sparse table $Z$ on the same six indices, with nonzero entries such as $4$ on diagonal-type patterns and $-2$ on selected off-diagonal patterns.
This module is chunk 1 of the 256-cell decide grid that certifies $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is pure finite enumeration over $(\mathrm{Fin},4)^6$; no continuum limit or variational argument is invoked here.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(0,1,3,2,3,0)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the matching explicitZ clause by 8. Equality of the resulting integers is decided by the kernel.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple and is proved by exhaustive fin_cases on the six Fin-4 indices. Each cell such as this one discharges one branch of that case split, so the chunked decide grid is the computational spine of the exact midpoint M2 numerator identity in 4D Regge analysis.
Within Recognition gravity work, closing $m_2^{\mathrm{num}}=8Z$ removes a kernel-level obstruction before continuum or phenomenological claims. It does not itself touch the forcing chain (T0–T8), RCL, or the $\phi$-ladder; it is infrastructure under the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.