e_320311
plain-language theorem explainer
For the six-index tuple (3,2,0,3,1,1) in (Fin 4)^6, the folded coupling numerator m2Num equals eight times the closed-form integer kernel explicitZ. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,3,1,1)$ with each entry in $\{0,1,2,3\}$, the summed 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 chunk 14 of a 256-way case split proving that the numerical second-moment numerator built from Regge midpoint couplings agrees with eight times a closed-form integer table, in four dimensions.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by an exhaustive pattern table (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal sign patterns $\mapsto -2$, and so on).
The local goal is purely arithmetic: evaluate both sides at one fixed multi-index and check equality in $\mathbb{Z}$.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted: the fold that defines $m_2^{\mathrm{num}}$ becomes a finite sum of known contributions, and explicitZ hits a single table clause (or the default). Lean’s kernel decision procedure discharges the resulting integer equality.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 4^6 index tuples into the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$. That assembly runs fin_cases on each coordinate and lands on chunk lemmas such as this one.
In the Recognition gravity stack, the identity certifies that the discrete Regge midpoint second-moment kernel matches its explicit closed form, a prerequisite for exact 4D curvature bookkeeping. It is infrastructure for the gravity analysis path, not a forcing-chain (T0–T8) step; it does not itself touch $\phi$, the eight-tick octave, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.