e_013101
plain-language theorem explainer
For the six Fin-4 indices (0,1,3,1,0,1), the folded M2 numerator equals eight times the explicit kernel table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint M2TT identity. The proof is a single kernel `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,1,0,1)$ in $\mathrm{Fin}\,4$, the folded 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 one chunk of the 4D Regge exact-midpoint certification that the folded M2 numerator equals eight times an explicit integer kernel on every six-tuple of Fin-4 indices. The ambient setting is discrete gravity: edge couplings are summed into a numerator that must match a closed-form table.
Upstream, m2Num is defined by folding contrib over couplingZList from zero. explicitZ is the sparse case table of that kernel (values such as $4$, $-2$, and so on on selected index patterns). The module doc states the local goal bluntly: "$m_2^{\mathrm{num}}=8\cdot\mathrm{explicit}Z$, chunk 1 (256 kernel decides)."
Each sibling e_* theorem pins one concrete six-tuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,1,3,1,0,1)$: the left via the fold definition of the numerator, the right via the pattern-match table for the explicit kernel. Lean’s decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all $a,b,c,d,i,j:\mathrm{Fin},4$ and discharges the identity by nested fin_cases, each leaf landing on a chunk fact such as this one. Without the per-tuple certificates the universal statement does not close.
In the Recognition gravity stack this is bookkeeping for the exact midpoint M2TT identity in 4D Regge analysis, not a new dynamical law. It supports the discrete curvature/coupling side of the framework once the kernel table is trusted. No T0–T8 forcing step is proved here; the result is pure finite verification that the numerator fold matches $8Z$ on this cell of the $4^6$ grid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.