e_010313
plain-language theorem explainer
For the single index tuple (0,1,0,3,1,3), the Regge midpoint mass-squared numerator equals eight times the explicit Z coupling. Gravity analysts cite it as one of 256 kernel cases that assemble into the universal m2Num = 8·explicitZ identity. The proof is a pure kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,3,1,3)\in(\mathrm{Fin}\,4)^6$, the midpoint mass-squared numerator equals eight times the explicit integer coupling: $m_2^{\mathrm{num}}(0,1,0,3,1,3)=8\,Z(0,1,0,3,1,3)$.
background
This module is chunk 1 of a 256-case kernel certification that the 4D Regge midpoint $M_2$ numerator agrees with eight times a closed-form coupling table. The ambient setting is discrete gravity analysis: edge and face indices run over $\mathrm{Fin},4$, and both sides of the identity are integers.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at those six indices. The right-hand side is the lookup table $\mathrm{explicitZ}$, a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ with finitely many nonzero pattern entries (for example $4$ on matched pairs such as $(0,0,1,1,2,2)$ and $-2$ on crossed patterns such as $(0,0,1,3,1,3)$).
The present declaration fixes one concrete sextuple and asserts numerical equality at that point only.
proof idea
One-line computational proof: decide evaluates both integer sides at the fixed indices $(0,1,0,3,1,3)$ and discharges the equality in the kernel. No algebraic lemmas are invoked; the fold defining the numerator and the pattern-match defining explicit Z are reduced to concrete Int values and compared.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):\mathrm{Fin},4$ by exhaustive fin_cases. Each chunk theorem such as this one supplies one case of that cover (module doc: "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)").
In the broader Recognition gravity stack, the certified numerator–coupling match is infrastructure for the exact midpoint Regge $M_2$ TT identity in 4D. It does not itself touch the forcing chain (T0–T8), the J-cost, or the $\varphi$-ladder; it is a discrete-geometry bookkeeping step that keeps the 4D kernel exact rather than approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.