e_201312

In the 4D Regge midpoint analysis, the mass-squared numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices $(a,b,c,d,i,j)$. The companion object $Z$ is an explicit piecewise integer function on the same index space (values such as $4$, $-2$, and so on on named patterns).

The local module is chunk 8 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8Z$ holds at every multi-index. The module imports only Mathlib and the kernel certificate that defines both $m_2^{\mathrm{num}}$ and $Z$. No continuum limit or variational principle is invoked here; the claim is purely discrete and arithmetic.

One-line computational proof: decide evaluates both sides on the concrete six-tuple $(2,0,1,3,1,2)$ and checks integer equality. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $Z$ (pattern match) are required; the kernel is small enough for Lean’s decision procedure.

This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall(a,b,c,d,i,j),, m_2^{\mathrm{num}}=8Z$ and discharges the universal claim by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete equality the assembler relies on.

In the broader Recognition gravity stack, the midpoint M2–TT identity is part of the discrete curvature and mass-squared bookkeeping on the Regge side. The factor of eight is the structural bridge between the folded coupling sum and the closed-form kernel $Z$. The result does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure inside the gravity analysis layer.