e_312103
plain-language theorem explainer
For the single multi-index (3,1,2,1,0,3) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel point checks. The proof is a pure decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded sum of coupling contributions at those indices and $Z$ for the explicit integer kernel table, one has $N(3,1,2,1,0,3)=8\,Z(3,1,2,1,0,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2–TT identity certification. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices, and the fold starts from 0. The comparison target $Z=\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
The local goal, stated in the module header, is to discharge $N=8Z$ on a 256-point block of the $4^6$ index space by kernel decides. Upstream, both $N$ and $Z$ live in the KernelCert module; neither carries a universal proof there, only the raw definitions used pointwise here.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete indices $(3,1,2,1,0,3)$ to closed integers (the fold for $N$, the match for $Z$) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $N=8Z$ for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof is a complete fin_cases tree that bottoms out at pointwise facts such as this one. Chunk 13 supplies one block of those leaves, so the universal identity (and whatever continuum or discrete gravity identity consumes it) depends on this decide succeeding.
In the broader Recognition gravity stack this is bookkeeping infrastructure for the Regge midpoint analysis, not a forcing-chain step (T0–T8) or an RCL identity. It closes a finite combinatorial obligation so later analytic claims can quote a single clean equality rather than a case table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.