e_012020

This module is one of the 256-case decide chunks that certify the algebraic identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for the 4D Regge midpoint M2–TT kernel. The local setting is pure integer arithmetic on six Fin-4 indices: no continuum limit, no curvature hypotheses.

Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of a fixed coupling list, summing each contribution at those indices. The companion $Z_{\mathrm{expl}}$ is an explicit piecewise integer table on the same six indices (typical nonzero entries are $\pm 2,,4$). The claim is that the fold evaluates to eight times the table entry at one concrete point.

One-line computational proof: by decide. Lean reduces both sides of the equality on the fixed Fin-4 sextuple to concrete integers (the fold of couplingZList versus 8 * explicitZ 0 1 2 0 2 0) and checks they match. No lemmas beyond the two definitions are invoked.

Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the certified numerator form of the 4D Regge midpoint M2–TT identity used in the gravity analysis stack. The chunking (256 kernel decides) keeps each goal inside the decide budget while still covering the full discrete index space. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched here; the result is pure discrete kernel bookkeeping inside the gravity layer.