e_331122
plain-language theorem explainer
For the six-index slot (3,3,1,1,2,2) on Fin 4, the folded M2 numerator equals eight times the explicit integer kernel entry. Gravity analysts cite it when discharging one concrete cell of the 4D Regge midpoint M2–TT identity. The proof is a single `decide` on two closed integer expressions.
Claim. With indices in $\mathrm{Fin}\,4$, the folded M2 numerator at $(3,3,1,1,2,2)$ equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(3,3,1,1,2,2)=8\,Z_{\mathrm{expl}}(3,3,1,1,2,2)$.
background
This module is one chunk of the exact midpoint M2–TT identity in 4D Regge analysis. The local claim pattern is $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on every six-tuple of $\mathrm{Fin},4$ indices; chunk 15 packages 256 such kernel decisions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a contribution functional over a fixed coupling list couplingZList, starting from 0. The explicit kernel $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal sign patterns $\mapsto -2$, and so on).
Both objects live in the kernel certificate module imported here; the present file only evaluates named index cells.
proof idea
One-line kernel decision. After unfolding the fold that defines the numerator and the matching clause of the explicit table at $(3,3,1,1,2,2)$, both sides reduce to concrete integers; decide checks the equality $n=8z$ in $\mathbb{Z}$. No lemmas beyond the two definitions are invoked.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every $a,b,c,d,i,j:\mathrm{Fin},4$ and proves it by exhaustive fin_cases. Each chunk theorem such as this one supplies one (or a block of) closed cells so the case split does not re-decide the arithmetic inline.
In the broader Recognition gravity stack, the M2–TT midpoint identity is part of the discrete curvature/bookkeeping layer that feeds continuum limits and coupling normalizations. It does not itself touch the T5–T8 forcing chain, $\phi$-ladder masses, or the $\alpha$ band; it is infrastructure for the Regge-side exact identities those continuum statements rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.