e_231023

This module is chunk 11 of a case-split certification that the 4D midpoint Regge numerator equals eight times an explicit integer kernel on every sextuple of Fin-4 indices (256 kernel decides per chunk).

The numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an Int. The comparison target explicitZ is a total function Fin 4^6 → Int given by an exhaustive pattern match (e.g. (0,0,1,1,2,2) ↦ 4, (0,0,1,2,1,2) ↦ -2, and so on).

The local goal is purely algebraic bookkeeping inside the Regge-exact midpoint analysis: no continuum limit or physical units enter at this layer.

One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of the numerator and the pattern-match definition of the explicit kernel; Lean’s decision procedure checks equality of those integers.

Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all a b c d i j : Fin 4 by exhausting the finite index space. That global equality is the certified algebraic core of the 4D midpoint M2TT identity in the Regge gravity analysis stack. Without the chunk lemmas, the assembler cannot discharge every sextuple. The result is pure discrete tensor algebra; it does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law, but it is infrastructure those gravity layers sit on.