e_002111

This module is one of the chunk files that discharge the pointwise identity between two integer-valued kernels on $(\mathrm{Fin},4)^6$. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing local contributions at a six-tuple of indices. The comparison target $Z=\mathrm{explicitZ}$ is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults) on the same index domain.

The local setting is the exact midpoint analysis of the 4D Regge M2 TT identity: one must check $N=8Z$ at every index combination. Because the domain is finite and tiny, the check splits into many concrete equalities (this file is chunk 0 of the 256 kernel decides). Upstream, both $N$ and $Z$ are pure definitions in the kernel certificate module; no analytic hypotheses remain once the indices are fixed.

One-line proof by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel evaluates the equality and closes the goal with no lemmas or rewriting.

Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by exhaustive fin_cases over all six indices and dispatch to these chunk equalities. That global identity is the algebraic backbone of the exact midpoint Regge M2 TT certificate in 4D gravity analysis inside the monolith. It is bookkeeping rather than a new physical law: once every slot matches, the folded coupling numerator is interchangeable with the explicit kernel scaled by eight, clearing a finite combinatorial obligation on the way to the continuum/Regge comparison.