e_212121
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index sextuple (2,1,2,1,2,1) equals eight times the closed-form explicit-Z table entry. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. Proof is a single decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(2,1,2,1,2,1)$ with each index in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(2,1,2,1,2,1)=8\,Z_{\mathrm{expl}}(2,1,2,1,2,1)$.
background
This module is chunk 9 of a 256-case kernel certifying that the folded numerator of the 4D Regge exact-midpoint M2TT identity agrees with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$.
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 term's contribution at those six indices. The table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on).
The local claim is only the single sextuple $(2,1,2,1,2,1)$. Sibling theorems cover the other cells; the assembly theorem quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold for the numerator versus the pattern match for the table, scaled by 8), and the kernel decides equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhaustive fin_cases on all six indices. Each chunk cell such as this one discharges one branch of that case split.
In the gravity analysis stack, the identity is the algebraic backbone of the 4D Regge exact-midpoint M2TT kernel certificate: it replaces a folded coupling sum by a sparse explicit table, which is what downstream curvature and continuum-limit arguments actually consume. It is pure discrete linear algebra on $\mathrm{Fin},4$, not a continuum GR statement, and does not by itself touch the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.