e_112012

This module is chunk 5 of a 256-point kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, labeling discrete directions in the 4D simplex/edge data of the Regge calculus setup.

The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term for the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).

The local claim is the pointwise identity $N=8Z$ at one concrete sextuple. Upstream, only the definitions of $N$ and $Z$ are needed; no analytic lemma is invoked beyond evaluation.

One-line proof by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals: the fold that defines the numerator runs over a concrete list, and the explicit kernel is a match on those literals. Lean’s kernel decision procedure compares the two evaluated Int values and closes the goal.

Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one concrete cell so the global identity is a pure case split rather than a symbolic fold argument.

In the Recognition gravity stack this identity is part of the exact midpoint M2 TT certification in 4D Regge analysis: it locks the discrete curvature/coupling numerator to an explicit sparse integer kernel, which is the computational backbone for later continuum or continuum-limit comparisons. It does not itself invoke the T0–T8 forcing chain, but it sits in the gravity analysis layer that consumes the forced $D=3$ spatial plus time structure as 4D combinatorial data.