e_211112
plain-language theorem explainer
For the six-index slot (2,1,1,1,1,2) in (Fin 4)^6, the folded Regge numerator m2Num equals eight times the tabulated kernel value explicitZ. The assembly theorem that exhausts all 4^6 index tuples cites this as one decide cell. Proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}1,\,d{=}1,\,i{=}1,\,j{=}2$ 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 9 of a 256-cell decide grid proving the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on every six-tuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint analysis of the 4D Regge $M_2$ TT 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 term at those indices. The comparison value $Z$ is an explicit integer table on $(\mathrm{Fin},4)^6$, with nonzero entries such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The present cell fixes the single multi-index $(2,1,1,1,1,2)$. Sibling theorems cover the other tuples in the same chunk; together they feed the universal quantifier over all indices.
proof idea
One-line kernel proof: by decide. Lean reduces both sides on the concrete Fin-4 indices to closed integers (the fold of m2Num versus 8 * explicitZ) and checks equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the quantifier by six nested fin_cases, each leaf a chunk decide such as this one. Without the full 256-cell cover, the exact midpoint $M_2$ TT identity in 4D Regge analysis cannot be certified at the numerator level.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the discrete curvature/coupling kernel, not a forcing-chain landmark (T5–T8). It closes a pure computational obligation so higher geometric claims can treat $m_2^{\mathrm{num}}=8Z$ as an unconditional fact on $\mathrm{Fin},4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.