e_313102
plain-language theorem explainer
Exact integer identity for one sextuple of Fin-4 indices: the folded Regge coupling numerator at (3,1,3,1,0,2) equals eight times the explicit kernel table entry there. Gravity analysts assembling the 4D midpoint M2 TT identity cite it as one of the 256 kernel cases. The proof is a single kernel decide on concrete Int arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,1,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel value: $N(3,1,3,1,0,2)=8\,Z(3,1,3,1,0,2)$.
background
This module is chunk 13 of a 256-case kernel certification that the 4D Regge midpoint M2 TT numerator matches eight times an explicit integer table. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex lattice with values in $\mathrm{Fin},4$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index $(a,b,c,d,i,j)$. The comparison table $Z=\mathrm{explicitZ}$ is a closed-form $\mathrm{Int}$-valued function on the same six $\mathrm{Fin},4$ arguments, with sparse nonzero entries such as $4$ on diagonal-type patterns and $-2$ on selected off-diagonal patterns.
Upstream, both $N$ and $Z$ live in the kernel certificate module; the present file only discharges one concrete sextuple equality needed for the global assembly.
proof idea
One-line kernel proof: decide evaluates both sides as concrete integers (the fold defining the numerator versus eight times the table lookup) and closes the propositional equality. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
Feeds the universal assembly theorem $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$, which exhausts all $(\mathrm{Fin},4)^6$ sextuples by case split and consumes the chunk equalities. That identity is the algebraic core of the Regge exact midpoint M2 TT certification in four dimensions: it replaces a folded coupling sum by a sparse explicit kernel, making subsequent gravity identities pure table arithmetic.
Within Recognition Science gravity work, this is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8). It closes one of 256 decide obligations so the assembled numerator–kernel match can be cited without residual case debt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.