e_201202

This module is one chunk of a 256-case kernel certification that the Regge midpoint M2TT numerator in 4D is exactly eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching four spacetime directions.

The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The table $Z$ is a hand-written piecewise integer function on the same six $\mathrm{Fin},4$ arguments (typical nonzero values $\pm 2,,4$).

The local claim is the instance of $N=8Z$ at the single tuple $(2,0,1,2,0,2)$. Sibling chunk theorems cover the other tuples; the assemble theorem glues them by exhaustive fin_cases.

One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at fixed indices, the right by looking up explicitZ 2 0 1 2 0 2 and multiplying by 8. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.

Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by casing all six $\mathrm{Fin},4$ arguments and dispatching to chunk equalities such as this one.

In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint M2TT certificate for 4D Regge calculus: once every index tuple matches, the continuum-facing mass/curvature bookkeeping can treat the folded numerator as a pure multiple of the sparse kernel. It is pure discrete linear algebra on the coupling list, not a continuum GR derivation, but it closes a necessary computational step in the RS gravity pipeline.