e_313201
plain-language theorem explainer
For the single index sextuple (3,1,3,2,0,1) in (Fin 4)^6, the folded Regge midpoint coupling numerator equals eight times the explicit kernel integer. Gravity analysts cite it as one cell of the 4D M2TT midpoint identity. The proof is a pure kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,2,0,1)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of the exhaustive 4D kernel certification that the Regge exact-midpoint M2 numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
Local goal, per the module header: discharge $m_2^{\mathrm{num}}=8\cdot Z$ on one concrete sextuple so the global assembler can cover all $4^6$ cells.
proof idea
One-line computational proof: decide. Both sides reduce to closed integer expressions once the six concrete Fin 4 arguments are substituted into the fold definition of the numerator and the pattern match for the explicit kernel, so the kernel equality checker finishes the goal with no lemmas or case splits in this file.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ and proves it by nested fin_cases on all six indices. Each chunk theorem such as this one is a single cell of that $4^6$-fold case tree (256 kernel decides organized across chunk modules).
In the Recognition gravity stack this is bookkeeping for the exact midpoint M2TT identity in 4D Regge analysis: the folded coupling numerator is forced to match eight copies of the explicit kernel, a discrete algebraic step toward the continuum gravity side rather than a new physical postulate. It does not itself invoke the T0–T8 forcing chain, $\phi$-ladder masses, or the RCL; it is pure index algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.