e_113010
plain-language theorem explainer
For the six-index tuple (1,1,3,0,1,0) on Fin 4, the Regge midpoint mass-squared numerator equals eight times the explicit Z-coupling at those indices. Gravity analysts cite it as one of the 256 kernel cases that assemble the global m2Num = 8·explicitZ identity. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $a{=}1,b{=}1,c{=}3,d{=}0,i{=}1,j{=}0$ in $\mathbb{F}_4$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel certifying that the Regge-exact midpoint mass-squared numerator equals eight times an explicit integer coupling table on $(\mathbb{F}_4)^6$. The setting is 4D discrete gravity analysis: each index runs over the four coordinate directions.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at the six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on those same indices (typical nonzero entries are $\pm 2,\pm 4$). The identity $m_2^{\mathrm{num}}=8,Z$ is the algebraic content being certified case by case.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(1,1,3,0,1,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $\mathrm{explicitZ}$ (pattern table).
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathbb{F}_4$ by exhaustive fin_cases and dispatches each leaf to a chunk theorem of this form. Without the 256 kernel decides, the global midpoint TT identity for the 4D Regge mass-squared numerator does not close. In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/mass ladder, not a new physical law; it locks the algebraic factor of eight between the folded numerator and the explicit Z table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.