e_211320
plain-language theorem explainer
Single multi-index instance of the 4D Regge midpoint numerator identity: at indices (2,1,1,3,2,0), the folded coupling numerator equals eight times the explicit kernel integer. Gravity analysts cite it when discharging one cell of the 256-case kernel chunk that builds the global m2Num = 8·explicitZ theorem. The proof is a pure kernel decision (decide).
Claim. For indices $(a,b,c,d,i,j)=(2,1,1,3,2,0)$ in $\mathrm{Fin}\,4$, 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 certified case-split proving that the 4D Regge midpoint M2TT numerator coincides with eight times an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from $0$ and add each term's contribution at the six indices. The explicit kernel $Z$ is a closed-form integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the listed patterns).
The local goal is mechanical: discharge one concrete cell so the assembler can recombine all cells into a single universal equality.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the fixed indices $(2,1,1,3,2,0)$ and accepts the match. No lemmas beyond the definitions of the folded numerator and the explicit kernel table are required.
why it matters
Parent theorem is the universal statement that $m_2^{\mathrm{num}}=8\cdot Z$ for every six-tuple in $(\mathrm{Fin},4)^6$, assembled by exhaustive fin_cases over the six indices and invoking each chunk cell such as this one. That identity is the certified algebraic core of the exact midpoint M2TT relation in the 4D Regge gravity analysis path. Without the per-cell decides, the assembler cannot close the forall. It is pure integer kernel bookkeeping inside the gravity domain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.