e_110012
plain-language theorem explainer
At multi-index (1,1,0,0,1,2) the folded Regge coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts cite this as one cell of the 256-case certification that m2Num = 8·explicitZ on Fin 4. The proof is a single kernel decide on concrete integers.
Claim. For $a=1$, $b=1$, $c=0$, $d=0$, $i=1$, $j=2$ 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 value $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel certification that the folded Regge midpoint numerator equals eight times an explicit integer table on all sextuples in $\mathrm{Fin},4$.
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 kernel $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The local goal is pointwise equality $m_2^{\mathrm{num}}=8Z$ at every multi-index; each chunk theorem discharges one concrete sextuple so the assembler can recombine them.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin 4 literals $(1,1,0,0,1,2)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the fold numerator and the pattern-matched kernel.
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. That identity is the algebraic core of the Regge exact-midpoint M2TT 4D kernel certificate in the Gravity analysis stack: it replaces a symbolic fold by a closed integer table, enabling exact (non-approximate) checks of the midpoint discrete gravity identities. Within Recognition Science this sits in the gravity/Regge side of the forcing chain rather than T5–T8 proper, but it is the concrete computational step that makes the 4D midpoint identity machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.