e_121002
plain-language theorem explainer
For the single multi-index (1,2,1,0,0,2) in (Fin 4)^6, the folded coupling numerator m2Num equals eight times the explicit integer table entry explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT kernel identity cite this as one of 256 kernel decides. The proof is a pure `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,1,0,0,2)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices in the 4D Regge exact-midpoint M2–TT kernel certificate.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a local contribution contrib over couplingZList at the six indices. The companion table explicitZ is a closed-form integer pattern match on those same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and zero off the matched patterns).
The local setting is pure integer arithmetic on a finite discrete index set; no continuum limit or metric signature is invoked at this layer.
proof idea
One-line computational discharge: by decide. Both sides reduce to concrete Int values (the fold of m2Num at the fixed indices versus 8 * explicitZ at those indices), and Lean’s kernel decision procedure checks equality. No lemmas are applied beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 index sextuples via nested fin_cases, and this chunk supplies the case $(1,2,1,0,0,2)$. That universal identity is the algebraic core of the 4D Regge exact-midpoint M2–TT kernel certificate in the Gravity analysis stack: it certifies that the folded coupling numerator is exactly eight times the explicit $Z$ table, so downstream curvature/defect identities can quote a closed form rather than a fold.
Within Recognition Science this sits in the discrete gravity layer that supports continuum limits and effective $G$; it does not itself touch the T0–T8 forcing chain, $\varphi$-ladder masses, or $\alpha$ band, but it hardens the combinatorial backbone those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.