e_313123
plain-language theorem explainer
For the fixed index sextuple (3,1,3,1,2,3) in (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one of 256 kernel cases that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $N$ for the folded coupling numerator obtained by summing all elementary contributions over the fixed coupling list, and $Z$ for the explicit integer lookup table on the same six indices. Then $N(3,1,3,1,2,3)=8\,Z(3,1,3,1,2,3)$.
background
This module is chunk 13 of a 256-way case split proving that the folded Regge midpoint numerator equals eight times a closed integer table on every sextuple of indices in $\mathrm{Fin},4$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start from $0$ and add each elementary contribution at the six indices. The table $Z=\mathrm{explicitZ}$ is a pattern-matched $\mathrm{Fin},4^6\to\mathbb{Z}$ map whose nonzero entries are small integers such as $\pm 2,\pm 4$.
The local claim is only the single point $(3,1,3,1,2,3)$. Sibling theorems cover the other points in the same chunk; the assembly theorem quantifies over all six indices by nested fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the kernel decision procedure discharges the equality with no lemmas and no manual algebra.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhausting all $4^6$ index tuples via fin_cases; each leaf is one of these chunk theorems. Establishing $N=8Z$ is the algebraic core of the exact midpoint M2TT identity in 4D Regge gravity analysis inside the Recognition Science gravity stack. It does not itself invoke the forcing chain (T0–T8) or the J-cost, but it is infrastructure for the discrete curvature side of that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.