e_120220

In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a local contribution at each coupling triple against the six free indices. The comparison target $Z_{\mathrm{ex}}$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to a universal factor of eight.

This module is chunk 6 of the 256-case decide barrage that discharges the identity one concrete multi-index at a time. The local setting is purely computational: both sides evaluate to concrete Int values, so equality is a finite check rather than an algebraic identity proof.

One-line proof by decide. Lean reduces both m2Num 1 2 0 2 2 0 (the fold over couplingZList) and 8 * explicitZ 1 2 0 2 2 0 (the table lookup times eight) to concrete integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.

The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof is a nested fin_cases sweep that bottoms out at these per-tuple decide lemmas; this declaration is the case $(1,2,0,2,2,0)$ inside that sweep.

In the broader Recognition gravity stack, the identity certifies that the midpoint Regge $m_2$ numerator collapses to an eightfold multiple of a sparse explicit kernel. That collapse is bookkeeping for the discrete curvature side of the RS gravity analysis, not a forcing-chain step (T0–T8), but it is required scaffolding before continuum or continuum-limit claims can quote a simplified $m_2$ expression.