e_001021
plain-language theorem explainer
For multi-index (0,0,1,0,2,1) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer kernel value. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one finite kernel cell. Proof is a single decide on the concrete integer equality.
Claim. For indices $a=0$, $b=0$, $c=1$, $d=0$, $i=2$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $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
This module is chunk 0 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The setting is the exact midpoint analysis of the 4D Regge M2TT identity in the Gravity.Analysis stack.
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 contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The explicit kernel $Z$ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite case table (e.g. $Z(0,0,1,2,2,1)=-2$, and many other tuples).
The parent assembly theorem states the identity for every index sextuple by exhaustive fin_cases. Each chunk theorem such as this one discharges one concrete cell of that case tree.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality for the fixed indices $(0,0,1,0,2,1)$ and checks they match. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (the fold over couplingZList) and $Z$ (the case table).
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by six nested fin_cases over $\mathrm{Fin},4$. That assembly is the certified algebraic identity behind the exact midpoint form of the 4D Regge M2TT kernel used in the gravity analysis stack.
In the Recognition Science gravity line this is bookkeeping infrastructure, not a forcing-chain step (T0–T8). It closes one of the 256 decide cells so the midpoint mass/curvature identity can be cited without residual case obligations. Downstream work that quotes the assembled equality inherits this cell automatically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.