e_232000
plain-language theorem explainer
At multi-index (2,3,2,0,0,0) the folded Regge midpoint numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one concrete cell in the 256-point kernel that certifies m2Num = 8·explicitZ. The proof is a single native decide on the two integer sides.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,0,0,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis the numerator mass-squared coupling is assembled by folding a fixed list of elementary contributions over six $\mathbb{F}_4$ indices:
$$m_2^{\mathrm{num}}(a,b,c,d,i,j)=\sum_{t\in\mathrm{couplingZList}}\mathrm{contrib}(t;a,b,c,d,i,j)\in\mathbb{Z}.$$
An independent closed-form table $Z:\mathbb{F}_4^6\to\mathbb{Z}$ records the expected values (e.g. $4$, $-2$, and sparse zeros). The module goal is the pointwise identity $m_2^{\mathrm{num}}=8Z$ on the full $4^6=4096$ grid, discharged by 256 kernel decides in chunks. This declaration is chunk 11's cell at $(2,3,2,0,0,0)$.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The tactic decide reduces the equality in the integer decision procedure: it unfolds m2Num (the fold over couplingZList) and explicitZ (the pattern-match table), computes each side, and checks equality. No lemmas beyond the two definitions are required.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ proves the universal statement by exhaustive fin_cases on all six indices and invokes each cell theorem such as this one. Closing the 256 kernel cells is the computational certificate that the folded Regge midpoint numerator is exactly eight times the explicit Z-table, a structural identity used downstream in the 4D gravity analysis. It is pure discrete algebra on $\mathbb{F}_4$ indices; it does not itself invoke the T0–T8 forcing chain, but it sits inside the gravity layer that consumes those geometric constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.