e_223301
plain-language theorem explainer
At multi-index (2,2,3,3,0,1) the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of 256 concrete kernel checks that assemble the full 4D identity. The proof is a pure `decide` on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(2,2,3,3,0,1)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel table.
background
This module is chunk 10 of a 256-way case split proving that the midpoint Regge $m_2$ numerator coincides with eight times an explicit integer kernel on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings are summed over a fixed list, and the resulting integer is compared to a hand-written table.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over couplingZList, starting from zero. The comparison target $Z$ is a pattern-matched table on six Fin 4 arguments (snippet shows values such as $4$, $-2$ on selected index patterns). Both live in the kernel-certificate module imported here.
The local claim is only the single tuple $(2,2,3,3,0,1)$; siblings cover the rest of the chunk.
proof idea
One-line computational proof: by decide. After the six indices are substituted, both sides reduce to concrete integers (the fold over the coupling list versus eight times the table entry), and Lean’s decision procedure checks equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every index by nested fin_cases and consumes this chunk fact (and its siblings) to obtain the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. That identity is the algebraic core of the 4D Regge exact-midpoint $m_2$–TT certificate in the gravity analysis stack.
Within Recognition Science this sits in the discrete-gravity / Regge sector that supports continuum limits and curvature bookkeeping; it does not itself touch the T0–T8 forcing chain, $\varphi$-ladder masses, or $\alpha$, but it hardens the geometric side those constants later couple to. Closing all 256 decides removes scaffolding from the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.