e_103020
plain-language theorem explainer
Single kernel identity: the Regge midpoint mass-squared numerator at multi-index (1,0,3,0,2,0) equals eight times the explicit Z coupling there. Gravity analysts cite it as one of 256 concrete cases feeding the global m2Num = 8·explicitZ assembly. The proof is a pure decide on closed integer arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,0,3,0,2,0)$ with each entry in $\mathbb{F}_4$, the midpoint Regge mass-squared numerator equals eight times the explicit integer coupling $Z$ at that multi-index: $m_2^{\mathrm{num}}(1,0,3,0,2,0)=8\,Z(1,0,3,0,2,0)$.
background
This module is chunk 4 of a 256-case kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint Regge identity in 4D. Indices run over $\mathrm{Fin},4$ (discrete spacetime/edge labels).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: sum of local contributions at those six indices. The comparison target $Z$ is an explicit piecewise integer table on $(\mathrm{Fin},4)^6$ (sample values $\pm 2,4,\ldots$), not derived in this chunk.
The local setting is pure integer equality after both sides evaluate; no continuum limit or curvature hypothesis is in play here.
proof idea
One-line computational proof: decide. Both sides are closed Int expressions once the six concrete Fin 4 arguments are substituted into the fold definition of the numerator and the pattern-match table for $Z$. Lean’s decision procedure discharges the resulting numeral equality with no lemmas or rewriting.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall(a,b,c,d,i,j),,m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six indices; each leaf is one of these e_* kernel facts. That global identity is the algebraic core of the 4D Regge exact-midpoint $M_2$–TT certification in the Gravity analysis stack. It does not itself touch the RS forcing chain (T5–T8) or the $\varphi$-ladder mass formula; it is infrastructure for discrete curvature/mass-squared bookkeeping inside the Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.