e_021002

This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to check $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on a block of the $4^6$ index space by kernel decides.

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 contribution term at those six Fin-4 indices. The comparison table $Z_{\mathrm{expl}}$ is an explicit integer pattern-match on the same six indices (sample clauses return $4$, $-2$, etc.).

Both definitions live in the kernel-certificate module imported here. The present lemma fixes one concrete multi-index in chunk 2.

One-line computational proof: decide. Lean reduces both sides at the concrete Fin-4 tuple $(0,2,1,0,0,2)$ to integers (the fold for the numerator versus the pattern clause for the table) and checks equality in the kernel. No lemmas are invoked beyond the two definitions.

Parent theorem is m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in $\mathrm{Fin},4$ by exhaustive fin_cases. Each chunk lemma such as this one discharges one residual case so the assembly stays inside the kernel decide budget (module note: 256 kernel decides per chunk).

In the gravity stack this identity is the algebraic spine of the exact midpoint M2 TT relation in 4D Regge calculus: the folded coupling numerator is forced to match eight times a sparse closed-form table. That match is bookkeeping for the discrete curvature/action side, not a new continuum claim. It does not itself invoke the RS forcing chain (T5–T8) or the J-cost; it is pure finite combinatorial certification supporting the gravity analysis layer.