e_322011
plain-language theorem explainer
For the six-index slot (3,2,2,0,1,1) 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. For indices $(a,b,c,d,i,j)=(3,2,2,0,1,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis for the 4D M2 TT identity, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given indices. The companion $Z$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
The local module is chunk 14 of a 256-way case split: each theorem pins one concrete six-tuple. The global claim is that $m_2^{\mathrm{num}}=8Z$ holds for every index combination; this file discharges one cell of that grid by pure evaluation.
proof idea
One-line decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted: the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$ become ground arithmetic, which the kernel decides equal after multiplying $Z$ by 8.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j., m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over Fin 4. That identity is the algebraic backbone of the Regge exact-midpoint M2 TT certificate in 4D gravity analysis inside the monolith. Without the per-cell decides, the universal equality cannot close. The factor of 8 is the bookkeeping constant that matches the folded coupling sum to the closed-form kernel table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.