e_302103

This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local claim is the pointwise relation $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the six-index kernel (Fin 4 arguments), discharged by kernel decides.

The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from 0 and add each contribution term at the six indices. The companion $Z$ is an explicit integer-valued table on $(\mathrm{Fin},4)^6$, with sparse nonzero patterns (e.g. value 4 or $-2$ on selected index tuples, and 0 elsewhere by the match default).

Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel certificate module. The present lemma fixes one concrete multi-index and asserts numerical equality of the two sides.

One-line computational proof: decide. Both sides are closed integer expressions once the six Fin-4 indices are concrete literals, so the kernel evaluates the fold that defines the numerator and the match that defines the explicit table, then checks Int equality. No algebraic rewriting or named lemmas beyond the two definitions.

Parent theorem is the assembled universal statement: for all six Fin-4 indices, the folded numerator equals eight times the explicit table. That assembler introduces the six variables and runs exhaustive fin_cases on each; the present lemma is the decide discharge for the cell $(3,0,2,1,0,3)$ inside chunk 12 of the kernel.

In the Recognition gravity stack this cell-level identity is bookkeeping for the exact midpoint M2 TT identity in 4D Regge analysis. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi ladder; it is pure integer kernel support for the continuum/discrete gravity side. Closing all chunks yields the global $m_2^{\mathrm{num}}=8Z$ identity used downstream in the midpoint certification.