e_013200
plain-language theorem explainer
For the six-index slot (0,1,3,2,0,0) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one atomic kernel cell. The proof is a single kernel decide on two concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,1,3,2,0,0)=8\,Z_{\mathrm{expl}}(0,1,3,2,0,0)$, where $Z_{\mathrm{expl}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of all coupling contributions at that multi-index.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple in $(\mathrm{Fin},4)^6$. The module doc states the local goal as "$m2Num = 8\cdot explicitZ$, chunk 1 (256 kernel decides)."
Upstream, $m2Num(a,b,c,d,i,j)$ is defined by folding couplingZList and summing each contribution at the given indices. explicitZ is the matching closed-form table of integers on those same six indices (sample cells include $4$, $-2$, and so on). Both live in the kernel-certificate module imported here.
The full identity is $\forall$ six indices, $m2Num=8\cdot explicitZ$. Exhaustive casework on $4^6$ cells is split across chunk files; this declaration is the cell at $(0,1,3,2,0,0)$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin-4 indices are fixed, so the decision procedure checks integer equality and closes the goal. No lemmas beyond the definitions of m2Num and explicitZ are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every cell into the universal statement $\forall a,b,c,d,i,j,, m2Num,a,b,c,d,i,j = 8\cdot explicitZ,a,b,c,d,i,j$, via exhaustive fin_cases on the six indices. This chunk supplies the $(0,1,3,2,0,0)$ branch of that case tree.
In the gravity stack the identity is part of the exact midpoint analysis for the 4D Regge M2TT kernel: a discrete curvature/mass-squared numerator must match a simple multiple of an explicit coupling table. Closing all 256-decide chunks removes scaffolding from that certificate and supports downstream continuum or continuum-limit comparisons in the RS gravity layer (spatial $D=3$ forced at T8, eight-tick structure at T7 as ambient discrete timing).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.