e_022232
plain-language theorem explainer
For the six-index slot (0,2,2,2,3,2) on Fin 4, the folded Regge coupling numerator equals eight times the tabulated explicit integer Z. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one atomic kernel cell. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,2,3,2)$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit integer table entry: $N(0,2,2,2,3,2)=8\,Z(0,2,2,2,3,2)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2 TT identity. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six Fin-4 indices. The comparison object $Z$ is an explicit integer table on the same six indices (sample clauses return $4$, $-2$, and similar small integers on matching patterns).
The local goal of the chunk is the pointwise identity $N=8Z$ on a block of the $4^6$ index space, discharged by kernel decisions rather than algebraic rewriting. Upstream, both $N$ and $Z$ are pure definitions in the kernel-cert module; no analytic lemma is required beyond evaluating those definitions at a concrete tuple.
proof idea
One-line proof by decide. Lean reduces both sides at the closed indices $(0,2,2,2,3,2)$: the fold that defines the numerator becomes a finite integer sum, the explicit table returns a constant, and the kernel checks $N=8Z$ by computation. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, N=8Z$ by exhausting Fin-4 cases; this declaration is one concrete cell in that cover (chunk 2 of the 256-decide split). In the Recognition gravity stack, the identity certifies that the midpoint M2 TT coupling numerator is exactly eight times a sparse explicit integer kernel, which is the algebraic backbone for the Regge-side exactness claim in 4D. It does not itself touch the forcing chain (T0–T8) or the J-cost RCL; it is infrastructure under the discrete gravity identities those continuum limits rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.