e_021333
plain-language theorem explainer
Single kernel identity: the midpoint Regge mass-squared numerator at index sextuple (0,2,1,3,3,3) equals eight times the explicit integer coupling Z there. Gravity analysts cite it as one concrete cell of the 4^6 case split that builds the global m2Num = 8·Z theorem. Proof is a pure `decide` on fixed integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,3,3,3)$ in $(\mathrm{Fin}\,4)^6$, the midpoint mass-squared numerator equals eight times the explicit integer coupling: $m_2^{\mathrm{num}}(0,2,1,3,3,3)=8\,Z(0,2,1,3,3,3)$.
background
This module is chunk 2 of a 256-way kernel certification that the discrete midpoint Regge mass-squared numerator coincides with eight times an explicit integer table Z on every sextuple of indices in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at those six indices. The companion table $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for the listed patterns).
The local claim is only the single cell $(0,2,1,3,3,3)$. The surrounding analysis lives in the 4D Regge-exact midpoint identity kernel certificate.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six concrete indices are substituted into the fold definition of the numerator and the pattern match for $Z$, so the kernel decision procedure discharges equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is one decided cell of that $4^6$ split.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge mass-squared analysis in 4D: it certifies that the folded coupling numerator collapses to the closed-form integer table used downstream. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; it is a pure discrete algebraic step inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.