e_121302
plain-language theorem explainer
For the six Fin-4 indices (1,2,1,3,0,2), the folded Regge midpoint numerator equals eight times the explicit Z-kernel entry. Gravity analysts cite these atomic equalities when assembling the full 4D M2TT identity over all index tuples. The proof is a single kernel decide on concrete integers.
Claim. For $a=1$, $b=2$, $c=1$, $d=3$, $i=0$, $j=2$ 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
This module is one chunk of a finite case split proving that the 4D Regge midpoint mass-squared numerator agrees with eight times an explicit integer kernel on every 6-tuple of indices in $\mathrm{Fin},4$. The local setting is pure computational certification: 256 kernel decides, no analytic expansion.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing the contribution of each term at those indices. The comparison object $Z(a,b,c,d,i,j)$ is a piecewise integer table on the same six indices (typical nonzero values $\pm 2,,4$). Both live in the kernel-cert module imported here.
The identity $m_2^{\mathrm{num}}=8Z$ is the algebraic content needed to close the midpoint M2TT bookkeeping in four dimensions; each chunk theorem pins one concrete tuple.
proof idea
One-line proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel evaluates the fold defining the numerator and the piecewise clause defining $Z$, then checks equality with the factor eight. No lemmas beyond the two definitions are invoked.
why it matters
This atom is consumed by the assembler m2Num_eq_eight_explicitZ, which states the universal claim
$\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$
and discharges it by nested fin_cases over all six indices. The chunk theorems supply (or match) the residual goals after case split.
In the Recognition gravity stack, the midpoint M2TT identity is part of the discrete curvature and mass-squared bookkeeping that must hold exactly on the eight-tick, $D=3$ lattice before continuum limits or phenomenological fits are discussed. Closing every index tuple removes a scaffolding gap in that certification path; it does not itself derive $G$, $\phi$-ladder masses, or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.