e_033012

This module is chunk 3 of a 256-way case split proving that the 4D Regge midpoint M2 numerator equals eight times an explicit integer kernel on every tuple of Fin-4 indices. The local slogan is $m2Num=8\cdot explicitZ$.

The numerator $m2Num(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry. The companion $explicitZ$ is a pattern-matched integer table on the same six Fin-4 arguments (sample values include $4$, $-2$, and so on for the listed index patterns).

The ambient goal is an exact algebraic identity in the Regge/TT gravity analysis, not an asymptotic or numerical fit. Each chunk theorem pins one concrete six-tuple so the assembler can recombine them by exhaustive fin_cases.

One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines the numerator at $(0,3,3,0,1,2)$, the right-hand side multiplies the table value of the explicit kernel by $8$. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.

Feeds the assembler theorem $m2Num_eq_eight_explicitZ$, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ and proves it by nested fin_cases, discharging each leaf with a chunk fact of this form. Without the full set of 256 decides, the global exact midpoint M2 TT identity in 4D cannot be closed in-kernel.

In the Recognition gravity stack this is pure algebraic certification of a discrete curvature/coupling identity, not a continuum GR derivation. It sits downstream of the kernel certificate module and upstream of the assembled equality used by later Regge analysis. No T0–T8 forcing step is at stake here; the landmark is exactness of the 4D midpoint numerator identity.