e_210230
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (2,1,0,2,3,0). Gravity analysts cite it as one cell of the 256-point kernel table that assembles into the full m2Num = 8·Z identity. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. At indices $(a,b,c,d,i,j)=(2,1,0,2,3,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six indices in $\mathrm{Fin},4$ are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from $0$ and add each term's contribution at $(a,b,c,d,i,j)$. The comparison target is an explicit piecewise integer map $Z$ on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
This module is chunk 9 of the 256 kernel decides that discharge $m_2^{\mathrm{num}}=8\cdot Z$ one multi-index at a time. The local setting is pure finite enumeration: every argument is a concrete residue in ${0,1,2,3}$, so equality of integers is decidable.
proof idea
One-line computational proof: decide evaluates both sides at the fixed tuple $(2,1,0,2,3,0)$. The left side runs the fold that defines the numerator; the right side looks up the matching clause of the explicit kernel and multiplies by $8$. No lemmas are invoked beyond the kernel definitions and integer arithmetic decidability.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk such as this one is a named cell of that $4^6=4096$-free, 256-pattern kernel table (the module doc: "m2Num = 8·explicitZ, chunk 9 (256 kernel decides)").
In the broader gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared coupling in 4D: once numerator and explicit kernel agree up to the universal factor $8$, later curvature and continuum-limit arguments can quote a single closed form rather than a fold. It does not itself touch the T0–T8 forcing chain or the J-cost; it is infrastructure inside the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.