e_312121
plain-language theorem explainer
For the six-index slot (3,1,2,1,2,1) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}2,\,d{=}1,\,i{=}2,\,j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(3,1,2,1,2,1)=8\,Z_{\mathrm{ex}}(3,1,2,1,2,1)$.
background
This module is chunk 13 of a 256-cell case split proving $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ for the exact midpoint M2 TT identity in 4D Regge analysis. Indices run over $\mathrm{Fin},4$ (four spacetime directions).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib at those indices. The comparison value $Z_{\mathrm{ex}}$ is an explicit integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete cell of that table identity, not the universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left via the fold definition of m2Num, the right via the pattern-match table explicitZ scaled by 8. Lean’s kernel decision procedure discharges the integer equality with no lemmas or case splits in this file.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by nested fin_cases on $(a,b,c,d,i,j)$ and invokes each chunk equality such as this one. Closing every cell yields the exact algebraic identity between the folded coupling numerator and eight times the explicit kernel, which is the computational heart of the 4D Regge midpoint M2 TT certification in the Gravity analysis stack.
In the broader Recognition framework this sits inside the discrete gravity / Regge side of the forcing chain (spatial $D=3$ plus time), supplying a machine-checked numerator identity rather than a continuum curvature argument. It does not itself touch $\phi$-ladder masses or $\alpha$; it is pure index algebra supporting the geometric certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.