e_313031
plain-language theorem explainer
For the six-index tuple (3,1,3,0,3,1) on Fin 4, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-coupling. Gravity analysts building the 4D exact midpoint M2TT identity cite this as one kernel cell among the 256. The proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,0,3,1)$ in $\{0,1,2,3\}^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer table of midpoint couplings.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list and summing each term's contribution at the given multi-index. The comparison target is an explicit piecewise table $Z$ that records the closed-form midpoint coupling (values such as $4$, $-2$, and so on on the listed patterns).
The local module is chunk 13 of a 256-cell kernel: each cell fixes one concrete six-tuple and asserts $m_2^{\mathrm{num}}=8Z$ there. The factor eight is the global normalization relating the folded sum to the explicit table across the whole kernel.
proof idea
One-line computational proof: both sides reduce to concrete integers once the six Fin-4 arguments are literals, so decide discharges the equality. No algebraic lemmas are invoked beyond the definitions of the folded numerator and the explicit $Z$ table.
why it matters
This cell is one brick in the exhaustive case split that yields the assembled identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. That parent theorem is the certified algebraic core of the 4D Regge exact-midpoint M2TT identity used on the gravity side of the monolith. Without the full 256-cell cover, the global equality remains a kernel gap rather than a proved normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.