e_313100
plain-language theorem explainer
Pointwise identity: the folded numerator m2Num at multi-index (3,1,3,1,0,0) equals eight times the explicit kernel value explicitZ there. Gravity analysts cite it as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ statement. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(3,1,3,1,0,0)\in(\mathbb{F}_4)^6$, the integer numerator $m_2^{\mathrm{num}}(3,1,3,1,0,0)$ equals $8$ times the explicit kernel entry $Z(3,1,3,1,0,0)$.
background
In the 4D Regge exact-midpoint analysis, the TT-sector mass-squared numerator is realized as an integer-valued six-index array on $\mathbb{F}_4$. The definition m2Num folds a fixed coupling list, summing a local contribution at each multi-index $(a,b,c,d,i,j)$. The companion array explicitZ is a closed-form integer table on the same index set (sample values include $4$, $-2$, and so on for the listed patterns).
The module is chunk 13 of a 256-cell kernel certification: each cell asserts m2Num = 8·explicitZ at one concrete multi-index. The local setting is pure integer arithmetic on Fin 4 coordinates; no continuum limit or metric signature is reopened here.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (m2Num by folding the coupling list at the fixed indices; explicitZ by its pattern-match table), and the equality $n = 8\cdot z$ is discharged by the decidable integer equality procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six Fin-4 indices. Each chunk cell such as this one is a leaf of that case tree. In the broader gravity stack, the factor-of-eight match certifies that the folded Regge midpoint numerator agrees with the explicit kernel used downstream in the 4D TT identity; without the pointwise cells the assembly cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.