e_201111
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,1,1,1,1) equals eight times the explicit integer kernel entry there. Gravity analysts cite it when assembling the global 4D Regge midpoint m2Num = 8·explicitZ certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,1,1,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(2,0,1,1,1,1)=8\,Z_{\mathrm{expl}}(2,0,1,1,1,1)$.
background
This module is chunk 8 of a 256-case kernel for the 4D Regge exact-midpoint M2TT identity: every multi-index in $(\mathbb{F}4)^6$ must satisfy $m_2^{\mathrm{num}}=8,Z{\mathrm{expl}}$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at those six indices. The explicit kernel $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (typical nonzero entries are $\pm 2,,4$).
Both definitions live in the KernelCert module; this chunk only discharges one concrete sextuple.
proof idea
One-line computational proof: decide evaluates both sides at the closed indices $(2,0,1,1,1,1)$ and checks integer equality. No lemmas are invoked; the fold that defines the numerator and the match that defines the explicit kernel reduce to numerals in the kernel.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the numerator half of the Regge exact-midpoint M2TT certificate in 4D gravity analysis.
Within Recognition Science gravity work, these kernel chunks turn a symbolic coupling fold into a fully checked integer table, so later curvature or deficit identities can quote a closed-form factor of 8 rather than an opaque sum. The present case is one of 256 parallel decides; alone it is bookkeeping, together they close the numerator side of the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.