e_011301
plain-language theorem explainer
For the single multi-index (0,1,1,3,0,1) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit integer kernel. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cases. The proof is a one-shot kernel decision (`decide`) with no algebraic rewriting.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $N(a,b,c,d,i,j)$ for the integer obtained by folding the coupling contribution list at those indices, and $Z(a,b,c,d,i,j)$ for the tabulated explicit kernel integer. Then $N(0,1,1,3,0,1)=8\,Z(0,1,1,3,0,1)$.
background
This module sits in the 4D Regge-exact midpoint analysis for the M2TT identity. The local goal, stated in the module header, is to certify $N=8Z$ on one 256-case chunk of the Fin-4 sextuple space by kernel decides.
The numerator $N=\mathrm{m2Num}$ is the fold of a fixed coupling contribution list over six Fin-4 indices: start at 0 and add each term's contribution at $(a,b,c,d,i,j)$. The comparison value $Z=\mathrm{explicitZ}$ is a closed integer table on the same six indices (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Upstream, both $N$ and $Z$ are defined in the kernel-certificate module; this chunk only evaluates the equality at concrete points.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(0,1,1,3,0,1)$ and checks integer equality. No lemmas are invoked; the kernel reduces the fold defining the numerator and the matching table clause of the explicit kernel to numerals and compares them.
why it matters
Parent theorem is the full assembly m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4,,N=8Z$ and discharges the quantifiers by nested fin_cases, landing on pointwise certificates such as this one. The module labels the work as chunk 1 of the 256 kernel decides needed for that identity.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint form of the 4D Regge M2TT relation, not a forcing-chain step (T0–T8) or an RCL identity. It closes one concrete cell so the universal equality can be assembled without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.