e_022333
plain-language theorem explainer
For the six-index slot (0,2,2,3,3,3) on Fin 4, the folded Regge M2 numerator equals eight times the explicit kernel integer Z. Gravity analysts cite it when discharging one cell of the 4D midpoint TT identity. The proof is a single kernel decide on two closed integer expressions.
Claim. With indices in $\mathrm{Fin}\,4$, the M2 numerator at $(0,2,2,3,3,3)$ satisfies $m_2^{\mathrm{num}}(0,2,2,3,3,3)=8\,Z(0,2,2,3,3,3)$, where $Z$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of coupling contributions.
background
In the 4D Regge midpoint analysis, the TT-sector M2 identity is checked by comparing a folded numerator against an explicit integer table. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib terms over a fixed coupling list. The comparison target explicitZ 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$, mixed pairs $\mapsto -2$).
This module is chunk 2 of that comparison: it proves $m_2^{\mathrm{num}}=8\cdot Z$ on a block of index tuples by kernel decision, rather than by a single global algebraic rewrite. The local setting is pure integer arithmetic on a $4^6$ grid; no continuum limit is taken here.
proof idea
One-line proof: decide. Lean reduces both sides at the concrete indices $(0,2,2,3,3,3)$ to integers (fold of contrib versus the explicitZ case) and checks equality in the kernel. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full $\forall a,b,c,d,i,j$ statement by fin_cases on all six indices; each chunk theorem such as this one supplies one concrete cell so the case split closes. That global identity is the algebraic certificate that the midpoint M2 TT numerator is exactly eight times the explicit kernel on the whole $4^6$ grid, a required step in the Regge-exact 4D gravity analysis inside the monolith. It does not itself touch the RS forcing chain (T5–T8) or the $\phi$-ladder mass formula; it is infrastructure for the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.