e_213232
plain-language theorem explainer
For the single multi-index (2,1,3,2,3,2) in (Fin 4)^6, the folded Regge mass-squared numerator equals eight times the explicit integer Z coupling. Gravity analysts cite it as one of 256 kernel certificates that assemble the full midpoint identity. The proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,2,3,2)$ with each entry 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 9 of a 256-way kernel split that certifies the 4D Regge exact-midpoint identity $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The local setting is discrete gravity: a mass-squared numerator built by folding a fixed coupling list, matched against a sparse explicit integer table.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding couplingZList and summing a contribution at each multi-index. The comparison target $Z$ is an explicit pattern-matched table $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$ on selected diagonal and off-diagonal patterns). Both live in the kernel certificate module imported here.
The full quantified statement is assembled downstream by exhausting all six $\mathrm{Fin},4$ coordinates; each chunk theorem discharges one concrete cell.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six indices are fixed literals, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ by six nested fin_cases sweeps. That global identity is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT certificate in the Gravity analysis stack.
In the Recognition framework this sits on the gravity side of the discrete geometry pipeline (eight-tick / $D=3$ structure upstream in the forcing chain). It does not itself touch $\phi$-ladder masses or $\alpha$; it only locks the integer kernel that later continuum or continuum-limit arguments rely on. Closing all 256 chunks removes a scaffolding surface under the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.