e_323203
plain-language theorem explainer
Finite-case check that the Regge midpoint mass-squared numerator at multi-index (3,2,3,2,0,3) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,2,3,2,0,3)\in(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-case kernel certification that the midpoint Regge mass-squared numerator equals eight times an explicit integer table on four-valued indices. The ambient setting is 4D discrete gravity analysis: each index runs in $\mathbb{F}_4\cong{0,1,2,3}$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The comparison target $Z$ is an explicit piecewise integer function on $(\mathbb{F}_4)^6$ (sample values include $4$, $-2$, and other small integers on listed patterns).
The global claim is that these two agree up to the constant factor $8$ at every multi-index. That universal statement is proved by exhaustive fin_cases on the six arguments, each leaf discharging one concrete equality of this form.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted (left via the fold definition of the numerator, right via the piecewise table for $Z$). Lean’s decision procedure checks the resulting integer equality; no lemmas beyond the two definitions are invoked.
why it matters
This is one leaf of the 256-case tree that builds m2Num_eq_eight_explicitZ, the assembled identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$. Downstream, that universal equality is the certified algebraic core of the Regge exact midpoint $M_2$/$TT$ identity in 4D. In the Recognition gravity stack it supplies a fully computational bridge from the coupling-list definition of the numerator to a closed-form integer kernel, so later curvature and continuum-limit arguments can quote a single clean factor-of-eight relation rather than an opaque fold. It does not itself touch the T0–T8 forcing chain; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.