e_211312
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (2,1,1,3,1,2) equals eight times the explicit Z kernel there. Gravity analysts cite it as one cell of the 256-decide kernel that assembles the global m2Num = 8·explicitZ theorem. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,1,3,1,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2(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 finite case-split proving $m_2=8Z$ on the 4D Regge midpoint kernel. Indices run over $\mathrm{Fin},4$ (four discrete directions on the simplex/edge labeling).
Upstream, $m_2$ 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 comparison target $\mathrm{explicitZ}$ is a closed-form integer table on six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local claim is only the single sextuple $(2,1,1,3,1,2)$; siblings cover the other concrete cells in the same chunk.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (left via the fold definition of $m_2$, right via the pattern-match table for $Z$ and multiplication by 8), so the equality is a decidable integer identity with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8Z$ and discharges the universal quantifier by fin_cases on all six indices, invoking one decide cell per sextuple.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT kernel in 4D: once every cell matches, the numerator is interchangeable with the closed $Z$ table, simplifying later curvature/mass-side identities. It is pure discrete algebra, not a continuum GR theorem, and sits downstream of the kernel certificate module rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.