e_313210

This module is one chunk of the 4D Regge midpoint M2–TT identity certification: the claim that the folded numerator m2Num equals eight times a sparse explicit integer kernel explicitZ on every six-tuple of Fin-4 indices.

m2Num a b c d i j is defined by folding a coupling list and summing local contributions at those indices. explicitZ is the closed-form integer table (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). The module doc frames chunk 13 as part of the 256 kernel decides that discharge the identity casewise.

Upstream, both definitions live in the kernel-cert module; downstream assembly will quantify over all index sextuples.

One-line computational proof: by decide. Lean evaluates both sides at the concrete Fin-4 sextuple $(3,1,3,2,1,0)$ (the fold for the numerator and the matching clause or default of the explicit kernel) and checks integer equality. No lemmas are invoked beyond the decidable equality instance on Int.

Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; N_{M_2}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one leaf of that case tree.

In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2–TT relation in 4D Regge analysis: it converts a summed coupling expression into a sparse explicit kernel, so later curvature and continuum-limit arguments can quote a closed integer table rather than a fold. It does not itself touch T0–T8 or the J-cost forcing chain; it is infrastructure inside the gravity analysis layer.