e_200330
plain-language theorem explainer
For the six-index slot (2,0,0,3,3,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}0,\,d{=}3,\,i{=}3,\,j{=}0$ in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit integer kernel entry: $N(2,0,0,3,3,0)=8\,Z(2,0,0,3,3,0)$.
background
This module sits in the Regge exact-midpoint analysis for the 4D M2 TT identity. 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 comparison object $Z=\mathrm{explicitZ}$ is a sparse integer table on six Fin-4 indices (typical nonzero values $\pm2,,4$).
The local claim is one cell of the identity $N=8Z$. The module is chunk 8 of a 256-way partition of the Fin-4^6 kernel; each chunk discharges a block of concrete index tuples by decision procedure rather than by symbolic algebra.
Upstream, only the two definitions matter: the fold that builds $N$ and the pattern-matched table $Z$. No analytic lemma is invoked at this leaf.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed indices $(2,0,0,3,3,0)$. The left side runs the fold over couplingZList; the right side looks up explicitZ and multiplies by 8. Equality of the resulting integers is certified by the decision procedure. No lemmas, rewrites, or case splits appear in the body.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j:,N=8Z$ and proves it by exhaustive fin_cases on all six indices, each leaf pointing at a chunk identity such as this one. Without the 256 concrete equalities, the assemble step has nothing to quote.
In the gravity stack this identity is bookkeeping for the Regge midpoint M2 TT kernel in 4D: it certifies that the folded coupling numerator is exactly eight copies of the sparse explicit table, so later curvature or mass-gap arguments can substitute the closed form. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel hygiene supporting the continuum gravity claims that sit above it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.