e_212012
plain-language theorem explainer
For the concrete multi-index (2,1,2,0,1,2) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two closed integer expressions.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer kernel table, one has $N(2,1,2,0,1,2)=8\,Z(2,1,2,0,1,2)$.
background
This module is chunk 9 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator equals eight times an explicit integer table. Indices run over Fin 4 (four spacetime directions).
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The table $Z=\mathrm{explicitZ}$ is a pattern-matched Int-valued function on six Fin 4 arguments, with nonzero entries such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The local claim is only the single sextuple $(2,1,2,0,1,2)$. Sibling chunks cover the other concrete cells; the assembly theorem quantifies over all of Fin 4.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left by evaluating the fold of contrib over couplingZList at the fixed indices, the right by unfolding the pattern match of explicitZ and multiplying by 8. The kernel checks integer equality; no lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N=8Z$ by exhaustive fin_cases on the six indices. Each chunk such as this one discharges one generated goal, so the universal midpoint identity is only as strong as the full set of 256 decides.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint form of the 4D Regge/M2TT coupling, not a derivation of $G$ or the forcing chain (T0–T8). It closes a computational certificate rather than an open physical hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.