e_201000

This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the local claim is that the summed numerator $m_2^{\mathrm{num}}$ equals eight times an explicit integer table $Z$, discharged by 256 kernel decides.

Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as a left fold of per-term contributions over a fixed coupling list. The companion $Z$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite pattern match (nonzero only on a sparse set of index patterns, with values such as $\pm 2,\pm 4$).

The six arguments live in $\mathbb{F}_4$ (discrete 4-values), so the full identity is a finite table of integer equalities. This declaration pins one cell of that table.

One-line computational discharge: by decide. Lean evaluates both sides of the integer equality at the concrete multi-index $(2,0,1,0,0,0)$ (folding the coupling list on the left, pattern-matching $Z$ on the right) and accepts the closed goal. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel.

Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8Z$, by exhaustive fin_cases on all six indices and routing each cell to its chunk decide. Without the full set of pointwise equalities, the closed-form factor of eight cannot be lifted off the kernel table.

In the gravity analysis stack this is bookkeeping for the 4D Regge midpoint M2TT identity: replacing a folded coupling sum by an explicit sparse integer kernel simplifies later exact identities used in the discrete curvature/mass-squared sector. It is not itself a forcing-chain step (T0–T8); it is infrastructure under the gravity side of the monolith.