e_011012

This module is chunk 1 of a 256-case kernel certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a sparse explicit integer table $Z_{\mathrm{explicit}}$. Both maps take six arguments in $\mathrm{Fin},4$ and return an Int.

Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The table $Z_{\mathrm{explicit}}$ is a pattern-matched closed form (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on). The local claim is one concrete six-tuple equality inside that certification.

One-line computational proof: decide evaluates both sides on the fixed indices $(0,1,1,0,1,2)$ and checks integer equality. No lemmas are invoked; the kernel reduces the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z_{\mathrm{explicit}}$ to concrete Int values and compares them.

Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple into the global identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhaustive fin_cases. This declaration discharges the single cell $(0,1,1,0,1,2)$ inside that case split (chunk 1 of the 256 kernel decides).

In the Recognition gravity stack the identity is the exact algebraic midpoint form of the 4D Regge M2 TT relation: once numerator and explicit kernel match everywhere, downstream curvature and mass-ladder arguments can quote a closed integer formula instead of a fold. It is pure discrete GR bookkeeping, not a forcing-chain (T0–T8) step, but it hardens the gravity side of the monolith.