e_121013
plain-language theorem explainer
For the single index sextuple (1,2,1,0,1,3) on Fin 4, the folded Regge numerator m2Num equals eight times the explicit Z-table value. Gravity analysts cite it as one cell of the 4D midpoint M2–TT kernel identity. The proof is a pure kernel decision (`decide`) on a closed integer equality.
Claim. For indices $(a,b,c,d,i,j)=(1,2,1,0,1,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(1,2,1,0,1,3)=8\,Z_{\mathrm{explicit}}(1,2,1,0,1,3)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times a closed-form integer table. The ambient setting is the exact midpoint M2–TT identity in discrete gravity: one checks, index by index, that a folded sum of coupling contributions matches an explicit sparse table.
m2Num a b c d i j is defined by folding couplingZList and accumulating contrib t a b c d i j into an Int. explicitZ is the matching lookup table on six Fin 4 arguments, returning small integers such as $4$, $-2$, and (by default) $0$ off the listed patterns.
The local claim is only the one sextuple $(1,2,1,0,1,3)$. Sibling theorems cover the other cells in the same chunk; the assembly theorem quantifies over all of $(\mathrm{Fin},4)^6$.
proof idea
One-line kernel proof: by decide. Both sides are closed integer terms once the six concrete Fin 4 indices are substituted, so the decidable equality procedure discharges $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ with no lemmas and no case split inside this declaration.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by exhaustive fin_cases on the six indices. Each chunk cell such as this one is a certified ground instance the assembly (or the kernel) relies on.
In the Recognition gravity stack this is bookkeeping for the exact 4D Regge midpoint identity, not a new physical law: it locks the discrete numerator to the explicit Z table so later curvature or continuum-limit arguments can quote a single closed form. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi ladder; those enter only if a downstream gravity theorem imports the assembled identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.