e_332001
plain-language theorem explainer
For the single multi-index (3,3,2,0,0,1) on Fin 4, the folded Regge midpoint M2 numerator equals eight times the explicit integer Z kernel. Gravity analysts cite it as one atomic cell in the 4D TT-identity certification. The proof is a pure kernel decide on that integer equality.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $m_2^{\mathrm{num}}$ for the fold of coupling contributions and $Z$ for the explicit integer kernel, one has $m_2^{\mathrm{num}}(3,3,2,0,0,1)=8\,Z(3,3,2,0,0,1)$.
background
This module is chunk 15 of a 256-cell kernel certification that the midpoint M2 numerator in 4D Regge calculus equals eight times an explicit integer table. Indices run over Fin 4 (four spacetime directions).
Upstream, m2Num is defined by folding a coupling list: it sums contrib t a b c d i j over every coupling term t. The companion table explicitZ is a closed-form integer function on six Fin-4 arguments, with sparse nonzero cases such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$.
The local claim is only the equality at one fixed sextuple. The surrounding analysis aims at an exact algebraic identity for the transverse-traceless midpoint mass-squared numerator, not a continuum limit or numerical fit.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality at the concrete indices $(3,3,2,0,0,1)$ and checks they match. No lemmas are invoked beyond the definitions of the fold m2Num and the table explicitZ; the kernel decision procedure discharges the ground term.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases and needs each cell equality such as this one. That global identity is the certified algebraic core of the 4D Regge midpoint M2 TT analysis in the Gravity domain.
Within Recognition Science this sits in the discrete geometric layer that supports continuum gravity limits, not in the T0–T8 forcing chain itself. It closes one of 256 decide cells so the assembled statement can be cited without residual case obligations. No open scaffold remains on this cell once decide succeeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.