e_311032
plain-language theorem explainer
For the Fin-4 index sextuple (3,1,1,0,3,2), the folded Regge coupling numerator equals eight times the explicit kernel table entry. Gravity analysts assembling the 4D midpoint M2TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decide on two closed integer expressions.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}1,\,d{=}0,\,i{=}3,\,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-case kernel certification that the Regge midpoint numerator equals eight times an explicit integer table on $(\mathrm{Fin},4)^6$. The local slogan is $m_2^{\mathrm{num}}=8\cdot Z$ by exhaustive decide.
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 term's contribution at those six indices. The table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical nonzero values are $\pm 2,,4$ on sparse support).
Both definitions live in the KernelCert module imported here. The present declaration fixes one concrete sextuple and asserts the scalar identity at that point.
proof idea
One-line proof: by decide. Both sides reduce to closed Int expressions (a finite fold versus a pattern match), so the kernel decides equality with no lemmas or case splits in this file.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all $a,b,c,d,i,j:\mathrm{Fin},4$ and discharges the universal claim by nested fin_cases, consuming this chunk equality as one of the 256 pointwise facts.
In the Recognition gravity stack this certifies the exact midpoint M2TT numerator identity in 4D Regge calculus: the folded coupling matches the sparse explicit kernel after the universal factor of eight. That identity is bookkeeping infrastructure for discrete curvature and mass-ladder gravity analyses, not a forcing-chain (T0–T8) step itself. Closing all chunks removes scaffolding from the assemble theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.