e_313110
plain-language theorem explainer
For multi-index (3,1,3,1,1,0), the midpoint Regge numerator equals eight times the explicit kernel entry. Gravity analysts cite it as one of 256 finite kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single computational decide on concrete integers.
Claim. The integer midpoint numerator $m_2^{\mathrm{num}}(3,1,3,1,1,0)$ equals $8$ times the explicit kernel value $Z(3,1,3,1,1,0)$, where both sides are evaluated at indices in $\mathrm{Fin}\,4$.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint Regge numerator equals eight times an explicit integer table. The ambient setting is 4D discrete gravity analysis: six indices in $\mathrm{Fin},4$ label the tensor slots of a midpoint contribution.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those indices. The comparison table $Z$ is an explicit piecewise integer function on the same 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 the single-point instance of $m_2^{\mathrm{num}}=8Z$ at $(3,1,3,1,1,0)$.
proof idea
One-line computational proof: decide evaluates both sides at the concrete $\mathrm{Fin},4$ sextuple $(3,1,3,1,1,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold-sum numerator and the piecewise table $Z$.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles the universal identity
$\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$
by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one concrete cell so the case split can close.
In the Recognition gravity stack this identity is the certified algebraic core of the 4D midpoint Regge $M_2$/$TT$ comparison: once every kernel cell matches, the continuum-facing curvature bookkeeping inherits an exact discrete factor of eight rather than a numerical fit. It does not itself touch the forcing chain (T0–T8) or the $\varphi$-ladder mass formula; it is pure discrete-gravity algebra supporting those later geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.