e_012201

This module is one chunk of the 4D Regge-exact midpoint analysis: it certifies cellwise that the folded numerator m2Num agrees with eight times a hand-written integer table explicitZ. The ambient goal is an exact algebraic identity for the M2–TT sector of the discrete gravity kernel.

m2Num a b c d i j is defined by folding a fixed coupling list, accumulating integer contributions contrib t a b c d i j over every coupling term t. explicitZ is a pattern-matched Fin 4^6 → ℤ table that records the expected closed form (typical nonzero values are ±2, ±4).

The local setting is pure finite enumeration: every index lives in Fin 4, so each concrete six-tuple is a decidable integer equality. Chunk 1 holds 256 such kernel decides; this declaration is the cell with indices 0,1,2,2,0,1.

One-line proof by decide. Both sides reduce to concrete integers: the left-hand side by evaluating the fold that defines m2Num at (0,1,2,2,0,1), the right-hand side by looking up explicitZ at the same multi-index and multiplying by 8. Lean’s kernel decision procedure checks the resulting ℤ equality; no lemmas beyond the two definitions are required.

Parent theorem m2Num_eq_eight_explicitZ assembles every cell into the universal statement $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. That universal identity is the algebraic backbone of the Regge-exact midpoint M2–TT certification in 4D discrete gravity.

In the Recognition Science gravity stack this is bookkeeping, not a new physical law: it closes one of the 4^6 finite cases so the midpoint curvature/mass kernel can be treated as an exact integer identity rather than a floating-point check. It does not itself invoke the forcing chain (T0–T8), φ, or the eight-tick octave; those enter only at higher layers that consume the certified kernel.