e_123231
plain-language theorem explainer
Pointwise check that the Regge midpoint numerator m2Num at Fin-4 indices (1,2,3,2,3,1) equals eight times the closed-form kernel explicitZ at those indices. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ identity. The proof is a single kernel decide.
Claim. For the index sextuple $(a,b,c,d,i,j)=(1,2,3,2,3,1)$ with each index in $\mathbb{F}_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 6 of a 256-cell case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all sextuples of $\mathrm{Fin},4$ indices in the 4D Regge exact-midpoint M2TT identity.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The closed form $\mathrm{explicitZ}$ is an integer-valued pattern match on the six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local claim is only the single cell with indices $(1,2,3,2,3,1)$; neighbouring cells live in sibling theorems of the same shape.
proof idea
One-line computational discharge: by decide. Both sides are closed integer terms once the six concrete $\mathrm{Fin},4$ indices are substituted into $m_2^{\mathrm{num}}$ (a finite fold) and into $\mathrm{explicitZ}$ (a pattern match), so the kernel evaluates the equality directly. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all $a,b,c,d,i,j:\mathrm{Fin},4$, which exhausts the six indices by fin_cases and lands on cells such as this one. That global identity is the algebraic backbone of the 4D Regge exact-midpoint M2TT kernel certificate in the Gravity analysis stack.
Within Recognition Science this sits on the gravity side of the forcing chain: once the discrete midpoint kernel is pinned, continuum and continuum-limit arguments can treat the factor-of-eight relation as settled data rather than a symbolic obligation. It does not itself touch T5–T8 or the RCL; it is pure discrete bookkeeping that those later gravity claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.