e_020130

The ambient module is a chunk of the 4D Regge-exact midpoint M2–TT identity certification: one must check that a folded numerator built from coupling contributions equals eight times a sparse explicit integer table, for every six-tuple in $(\mathrm{Fin},4)^6$.

Here $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing the local contribution of each term at those indices. The comparison table $Z_{\mathrm{explicit}}$ is a pattern-matched integer function on the same six indices (nonzero only on a short list of pairings such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).

This file is chunk 2 of the 256 kernel decides that cover the finite case split.

One-line computational proof: by decide. Both sides reduce to concrete Int values for the fixed indices $(0,2,0,1,3,0)$, and the kernel checks equality. No lemmas beyond the definitions of m2Num and explicitZ are required.

Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge-exact midpoint M2–TT identity in 4D gravity analysis inside the monolith.

In the Recognition framework this sits in the gravity sector that must match continuum curvature identities on the discrete ladder; it is bookkeeping, not a new forcing step (T0–T8), but it closes a finite certification cell needed before continuum limits or effective $G$ comparisons can be trusted.