e_302010
plain-language theorem explainer
For the six-index slot (3,0,2,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite it when assembling the full Regge midpoint M2TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the coupling-fold numerator at $(a,b,c,d,i,j)=(3,0,2,0,1,0)$ satisfies $N(3,0,2,0,1,0)=8\,Z(3,0,2,0,1,0)$, where $N$ is the fold of local contributions and $Z$ is the explicit integer table.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity: the claim that the folded numerator m2Num equals eight times a sparse integer table explicitZ on every six-tuple of Fin-4 indices. The module header states the local goal as "m2Num = 8·explicitZ, chunk 12 (256 kernel decides)."
m2Num a b c d i j is defined by folding contrib over a fixed coupling list, starting from 0. explicitZ is a pattern-matched Int-valued table on six Fin-4 arguments (typical nonzero entries are $\pm 2,\pm 4$). The present declaration fixes one concrete six-tuple in that 4^6 grid.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 indices are substituted: the left via the fold definition of the numerator, the right via the pattern table. The kernel checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by exhaustive fin_cases and dispatches each cell to a chunk equality of this form. That global identity is part of the certified algebraic core of the 4D Regge midpoint M2TT analysis in the Gravity domain. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete tensor bookkeeping supporting the continuum gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.