e_132010
plain-language theorem explainer
For the multi-index (1,3,2,0,1,0) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts certifying the 4D Regge midpoint M2 TT identity cite this as one atomic kernel instance. The proof is a single `decide` on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(1,3,2,0,1,0)$ in $\mathrm{Fin}\,4$, the numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2 TT identity is certified by matching a folded numerator against a closed-form kernel. The numerator m2Num is the fold of contrib over couplingZList at a six-tuple of Fin 4 indices, returning an Int. The companion explicitZ is a pattern-matched integer table on the same six-tuple (sample clauses: $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
This module is chunk 7 of the 256-kernel decide suite that discharges one multi-index at a time. The local claim is the scalar identity $m_2^{\mathrm{num}}=8Z$ at the fixed tuple $(1,3,2,0,1,0)$.
proof idea
One-line computational discharge: by decide. Lean evaluates both sides of the integer equality (the fold defining the numerator versus eight times the pattern-matched kernel entry) and closes the goal by kernel decision procedure. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies one concrete case in that case-split tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge M2 TT kernel in 4D: once every multi-index matches, the folded coupling is interchangeable with the explicit table, clearing a certification obligation in the discrete curvature analysis. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is pure integer kernel hygiene inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.