e_003301
plain-language theorem explainer
For the concrete index sextuple (0,0,3,3,0,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit kernel integer. Gravity analysts cite it as one cell of the 256-way case split that certifies the 4D midpoint M2TT numerator identity. The proof is a single kernel decide on closed integer arithmetic.
Claim. For indices $a{=}0,b{=}0,c{=}3,d{=}3,i{=}0,j{=}1$ in $\mathbb{F}_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 0 of a 256-cell kernel certificate that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times an explicit sparse integer kernel $Z$ on $(\mathbb{F}_4)^6$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The companion $Z$ is a pattern-matched integer table on the same six Fin-4 arguments (typical nonzero entries are $\pm 2,\pm 4$).
The local claim is the single cell at $(0,0,3,3,0,1)$: equality of those two integers after evaluation.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple and checks integer equality in the kernel. No algebraic lemmas are invoked; the definitions of $m_2^{\mathrm{num}}$ (list fold of contributions) and explicit $Z$ (pattern match) reduce to closed Int values that the decision procedure compares.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on $(\mathbb{F}_4)^6$. Each chunk cell such as this one discharges one concrete sextuple so the assembly has no sorry.
In the Gravity analysis stack this numerator identity is the algebraic backbone of the exact midpoint M2TT certificate for 4D Regge calculus. It is bookkeeping, not a new physical law, but without the 256 decides the global equality cannot be closed in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.