e_021110
plain-language theorem explainer
Pointwise check that the folded mass-squared numerator equals eight times the explicit Z-table entry at multi-index (0,2,1,1,1,0). Gravity analysts cite it as one of the 256 kernel cells feeding the global m2Num = 8·explicitZ identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, the mass-squared numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and the fold starts from zero. The companion table $Z$ is an explicit case-split function on the same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero patterns.
This module is chunk 2 of a 256-cell kernel that asserts $m_2^{\mathrm{num}}=8\cdot Z$ at every multi-index. The local setting is pure integer arithmetic on a finite discrete index set; no continuum limit or metric signature is invoked here.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The tactic decide runs the kernel decision procedure on that equality and closes the goal. No lemmas beyond the definitions of the fold and the table are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by nested fin_cases on $(a,b,c,d,i,j)$ and dispatches each cell to a chunk lemma of this form. Without the pointwise identities, the global numerator-to-table factor of eight would remain unproved. In the broader gravity stack this factor is the algebraic bridge between the summed Regge coupling expansion and the closed-form midpoint kernel used downstream in the 4D TT-sector identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.