e_320310
plain-language theorem explainer
For the Fin-4 index sextuple (3,2,0,3,1,0), the midpoint Regge mass-squared numerator equals eight times the explicit coupling kernel Z. Gravity analysts cite it as one atomic kernel decision among the 256 that assemble the global identity m2Num = 8·explicitZ. The proof is a single computational decide on concrete integers.
Claim. At indices $(3,2,0,3,1,0)\in(\mathrm{Fin}\,4)^6$, the midpoint mass-squared numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(3,2,0,3,1,0)=8\,Z(3,2,0,3,1,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ by 256 concrete kernel decisions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: it sums a contribution functional over that list and returns an integer. The explicit kernel $Z$ is a piecewise integer table on $(\mathrm{Fin},4)^6$, with values such as $4$, $-2$, and so on on the listed index patterns.
Both maps are defined in the kernel-certificate module imported here. The present declaration fixes one sextuple and asserts numerical equality of the two sides.
proof idea
One-line computational proof: decide evaluates both the folded numerator and the explicit table entry at the concrete Fin-4 indices $(3,2,0,3,1,0)$, reduces each side to a closed integer, and checks equality in $\mathbb{Z}$. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$ are required.
why it matters
The parent theorem is the assembled identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$, proved by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one case of that cover.
In the broader Gravity analysis stack, the identity certifies that the midpoint Regge mass-squared numerator is exactly eight times the explicit 4D coupling kernel, a numerical checkpoint inside the TT-sector exactness argument. It does not itself touch the Recognition forcing chain (T0–T8), but it is infrastructure for the discrete gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.