e_311312
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at index sextuple (3,1,1,3,1,2) equals eight times the explicit kernel table entry there. Gravity analysts cite it as one of 256 concrete Fin-4 cases feeding the assembled m2Num = 8·explicitZ theorem. Proof is a single kernel decide on two closed integer expressions.
Claim. For indices $a{=}3,b{=}1,c{=}1,d{=}3,i{=}1,j{=}2$ in $\mathbb{F}_4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the tabulated explicit kernel value at those same indices.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint Regge mass-squared numerator equals eight times an explicit integer kernel on every sextuple of $\mathbb{F}_4$ indices.
The numerator is defined by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at zero. The explicit kernel is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, several sign-flipped off-diagonal patterns $\mapsto -2$, and so on).
The local goal is only the single sextuple $(3,1,1,3,1,2)$. Upstream definitions supply both sides of the equality as pure integer data, so no analytic estimates enter.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left via the fold definition of the numerator over the coupling list, the right via the case table for the explicit kernel (scaled by 8). Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j:\mathbb{F}_4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a leaf of that case tree.
In the broader Gravity analysis, the identity certifies that the midpoint Regge $M^2$ TT kernel in 4D matches its closed-form table, a computational step toward exact discrete curvature identities. It does not itself touch the RS forcing chain (T0–T8), $\phi$-ladder masses, or $\alpha$; it is pure 4D combinatorial gravity bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.