e_233103
plain-language theorem explainer
For the six-index tuple (2,3,3,1,0,3) on Fin 4, the folded midpoint M2 numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one atomic case in the 256-way case split that certifies the Regge midpoint identity. The proof is a single kernel decide on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $m_2^{\mathrm{num}}$ for the fold of coupling contributions and $Z$ for the explicit integer kernel, one has $m_2^{\mathrm{num}}(2,3,3,1,0,3)=8\,Z(2,3,3,1,0,3)$.
background
This module is chunk 11 of a 256-case kernel certification that the midpoint M2 numerator equals eight times an explicit integer table in 4D Regge analysis. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those six indices. The comparison object $Z(a,b,c,d,i,j)$ is an explicit pattern-matched integer (values such as $4$, $-2$, and so on on the listed patterns).
The local goal is purely discrete: check the scalar identity $m_2^{\mathrm{num}}=8Z$ at one concrete multi-index, as part of exhausting all $4^6$ combinations.
proof idea
Both sides evaluate to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed. The proof is the single tactic decide, which asks the kernel to confirm equality of those two computed Int values. No algebraic rewriting or named lemmas are invoked beyond the definitions of the numerator fold and the explicit $Z$ table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every index tuple by nested fin_cases and needs each atomic equality such as this one. That universal identity is the certified bridge between the folded coupling numerator and the closed-form $Z$ table in the Regge exact-midpoint M2/TT analysis.
In the broader Recognition gravity stack this is bookkeeping infrastructure, not a new physical law: it underwrites exact discrete identities used when matching continuum limits and coupling normalizations. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; it only clears one cell of the 256-cell decide grid named in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.