e_203330
plain-language theorem explainer
For the six-index slot (2,0,3,3,3,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel decides. The proof is a single decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(2,0,3,3,3,0)$ equals eight times the explicit kernel integer at the same indices: $N(2,0,3,3,3,0)=8\,Z(2,0,3,3,3,0)$.
background
This module is chunk 8 of a 256-case kernel certification that the folded numerator m2Num equals eight times a sparse closed form explicitZ on all six-tuples in $(\mathrm{Fin},4)^6$. The setting is the exact midpoint analysis of the 4D Regge M2 TT identity in the Gravity.Analysis stack.
m2Num a b c d i j is defined by folding a fixed coupling list and summing a local contribution at each term. explicitZ is an integer-valued pattern match on the six indices; only a sparse set of index patterns is nonzero (e.g. $(0,0,1,1,2,2)\mapsto 4$, several permutations $\mapsto -2$).
The present declaration fixes one concrete six-tuple, $(2,0,3,3,3,0)$, so both sides reduce to plain integers and can be checked by computation.
proof idea
One-line decide. Both sides are closed integer expressions once the six Fin 4 arguments are concrete: the left unfolds the fold over couplingZList, the right evaluates the pattern match in explicitZ. Lean’s kernel decision procedure discharges the equality with no lemmas beyond definitional reduction.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhaustive fin_cases and routes each case to a chunk decide such as this one. That global equality is the certified bridge between the folded coupling numerator and the sparse explicit kernel used in the 4D Regge exact-midpoint M2 TT analysis.
In the broader Recognition gravity stack, these kernel identities underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ lattice side of the forcing chain. The chunk exists only to keep the 256 decides modular; it does not itself introduce new physics constants or mass-ladder claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.