e_113201
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (1,1,3,2,0,1) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full Regge midpoint M2TT numerator identity over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(1,1,3,2,0,1)\in(\mathbb{F}_4)^6$, the summed coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(1,1,3,2,0,1)=8\,Z_{\mathrm{expl}}(1,1,3,2,0,1)$.
background
This module is chunk 5 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at every sextuple of indices in $\mathbb{F}_4$. The setting is the exact midpoint analysis of a 4D Regge/M2TT identity in the Gravity.Analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six indices. The comparison object $Z_{\mathrm{expl}}$ is an explicit integer-valued table on $(\mathbb{F}_4)^6$, given by pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The present declaration fixes one concrete sextuple, $(1,1,3,2,0,1)$, and asserts the scalar equality of the fold against eight times the table entry.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel decision procedure discharges the equality with no lemmas or case splits in this file.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathbb{F}_4$ and proves it by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies one (or a block of) decided cells so the assembly stays inside kernel-checkable fragments rather than a single giant decide.
In the Recognition gravity stack this closes the algebraic numerator side of the exact midpoint M2TT/Regge identity in 4D: once every cell matches $8,Z_{\mathrm{expl}}$, the folded coupling form is interchangeable with the closed table. That supports downstream curvature and continuum-limit arguments that need a fully explicit, machine-checked numerator. It is bookkeeping inside the gravity analysis layer, not a T0–T8 forcing step, but it is load-bearing for any claim that the 4D midpoint identity holds exactly on the discrete index set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.