e_210203
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,1,0,2,0,3) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D midpoint M2 TT numerator identity over (F_4)^6. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,2,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer at that multi-index: $N(2,1,0,2,0,3)=8\,Z(2,1,0,2,0,3)$.
background
This module is chunk 9 of a 256-case kernel certification that the 4D Regge midpoint M2 TT numerator agrees with an explicit integer table, up to the universal factor 8. The ambient setting is discrete gravity analysis: edge/face multi-indices live in $\mathbb{F}_4$, and both sides of the identity are pure integers.
The folded numerator $N(a,b,c,d,i,j)$ is defined by left-folding a fixed coupling list, accumulating each term's contribution at the six indices. The comparison object $Z$ is an explicit pattern-matched table $\mathbb{F}_4^6\to\mathbb{Z}$ (sample clauses send $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). The claim is the pointwise equality $N=8Z$ at one concrete tuple.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions (the fold over the fixed coupling list versus the table lookup, scaled by 8), so the equality is a decidable proposition on Int and discharges without lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhaustive fin_cases on all six $\mathbb{F}_4$ arguments. That universal identity is the certified numerator half of the Regge exact midpoint M2 TT relation in 4D; this chunk is one of the 256 kernel atoms the assembly glues together. In the broader Recognition gravity stack it supports exact discrete curvature bookkeeping (no floating approximation) on the eight-tick, $D=3$ spatial backbone, keeping the continuum limit honest at the level of integer combinatorics rather than numeric fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.