e_200230
plain-language theorem explainer
At multi-index (2,0,0,2,3,0) on (Fin 4)^6, the folded midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 kernel point checks in the Regge exact-midpoint M2TT identity. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,2,3,0)$ 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 kernel value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2TT identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ on one chunk of the $4^6=4096$ index space by discharging 256 kernel decisions.
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 Fin-4 indices. The comparison target explicitZ is a closed-form integer table on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel-certificate module imported here; this file only specializes them to concrete points.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the fixed indices $(2,0,0,2,3,0)$ and confirms they match. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit kernel table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases. Each chunk lemma such as this one is a named kernel point in that cover.
In the broader gravity stack, the factor-of-eight match between the folded coupling numerator and the explicit Z table is the algebraic content of the Regge exact-midpoint M2TT identity in 4D. Closing all chunks removes a computational gap in that identity; it does not by itself force continuum GR or the RS forcing chain (T0–T8), but it is a necessary discrete certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.