e_221102
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,2,1,1,0,2) equals eight times the explicit kernel value there. Gravity analysts cite it as one cell of the 256-entry kernel table that assembles into the universal m2Num = 8·explicitZ identity. Proof is a single native decide on concrete Fin-4 indices and integer arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,2,1,1,0,2)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit kernel entry: $m_2^{\mathrm{num}}(2,2,1,1,0,2)=8\,Z_{\mathrm{expl}}(2,2,1,1,0,2)$.
background
This module is chunk 10 of a 256-cell kernel certification for the 4D Regge exact-midpoint M2TT identity. The claim under audit is the pointwise relation $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on one fixed multi-index in $(\mathbb{F}_4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it accumulates integer contributions contrib t a b c d i j over every term $t$ in couplingZList. The explicit kernel $Z_{\mathrm{expl}}$ is a closed-form integer table on the same six Fin-4 indices (sample entries include $4$ on diagonal-type slots such as $(0,0,1,1,2,2)$ and $-2$ on off-diagonal slots such as $(0,0,1,2,1,2)$).
Both definitions live in the KernelCert module imported here. The present theorem fixes the concrete slot $(2,2,1,1,0,2)$ and checks the factor-of-eight match at that slot alone.
proof idea
One-line computational proof: by decide. After the six Fin-4 arguments are substituted, both sides reduce to concrete integers (the fold that defines the numerator, and the pattern match that defines the explicit kernel). Lean’s native decision procedure discharges the resulting integer equality with no lemmas and no case splits in the source.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhausting all $4^6=4096$ index tuples via fin_cases. This declaration is one certified cell in that table (chunk 10 of the 256 kernel decides), so the assembly step can treat the factor-of-eight match as already checked at $(2,2,1,1,0,2)$.
In the broader gravity stack the identity is the algebraic core of the Regge exact-midpoint M2TT analysis in 4D: it converts a folded coupling sum into an explicit sparse kernel, which is the form needed for later continuum and continuum-limit arguments. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; those enter only upstream of the Regge discretization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.