e_311033

This module is one certified chunk of the identity $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ on all six-tuples of $\mathrm{Fin},4$, used in the 4D Regge exact-midpoint M2 TT analysis. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $Z_{\mathrm{explicit}}$ is an explicit integer-valued kernel on the same six indices, given by a finite pattern-match table (entries such as $4$, $-2$, and so on).

Chunk 13 isolates one block of those kernel decisions so the full $4^6$ case split can be assembled without a single monolithic proof term. Upstream, both $m_2^{\mathrm{num}}$ and $Z_{\mathrm{explicit}}$ live in the KernelCert module that supplies the raw definitions this equality instantiates.

One-line computational proof: decide evaluates both sides at the concrete Fin-4 six-tuple $(3,1,1,0,3,3)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of $m_2^{\mathrm{num}}$ (list fold of contrib) and $Z_{\mathrm{explicit}}$ (pattern match).

Parent theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ (forall on $(\mathrm{Fin},4)^6$) is assembled by exhaustive fin-cases; this chunk discharges the single cell $(3,1,1,0,3,3)$. That global identity is infrastructure for the exact midpoint M2 TT relation in 4D Regge gravity inside the Recognition Science gravity stack. It does not itself invoke the forcing chain (T5 J-uniqueness, T8 $D=3$), but it sits in the discrete-geometry layer that must match continuum limits once the eight-tick and dimension constraints are in force. Closing every chunk removes scaffolding from the M2 numerator certification.