e_310302

This module is chunk 13 of a 256-cell kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times an explicit integer table on every sextuple of indices in $\mathbb{F}_4$.

The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at the six indices, and the fold accumulates their sum. The comparison target explicitZ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite case table (typical nonzero entries are $\pm 2,\pm 4$).

The local claim is only the single cell $(3,1,0,3,0,2)$. Sibling theorems cover the other cells in the same chunk; the assembly theorem later quantifies over all of $\mathbb{F}_4^6$.

One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple and checks integer equality. No algebraic lemmas are invoked; the kernel definitions reduce to closed integer arithmetic that Lean’s decision procedure discharges.

Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on each coordinate and dispatch to the matching cell theorem. That global identity is the algebraic backbone of the 4D midpoint Regge TT mass-squared certification in the Gravity analysis stack. Within Recognition Science it supports the discrete geometric side of the gravity sector (Regge calculus on the eight-tick / $D=3$ scaffold), not the T0–T8 forcing chain itself. Closing all 256 cells removes a scaffolding gap between the folded coupling definition and the explicit kernel table.