e_130101

This module is chunk 7 of a 256-cell kernel certification that the Regge midpoint mass-squared numerator equals eight times an explicit integer table on $(\mathrm{Fin},4)^6$. The setting is 4D discrete gravity analysis: edge and face couplings are summed into a numerator that should match a closed-form kernel.

The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and adding each contribution at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and zero off the listed patterns).

The local claim is one concrete cell of that table identity, not the universal quantification.

One-line proof by decide. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at $(1,3,0,1,0,1)$, the right by looking up $8\cdot Z$ at the same indices. The kernel checks integer equality; no lemmas are invoked beyond the definitions of the numerator and the explicit table.

Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices, dispatching each cell to a chunk theorem of this form. Without the cell identities, the universal midpoint M2–TT numerator identity in 4D does not close.

In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/mass-squared side of the Regge analysis, not a forcing-chain landmark (T5–T8) by itself. It removes one of 256 kernel obligations so the assembled equality can be cited downstream without sorry.