e_020021
plain-language theorem explainer
For the six-index tuple (0,2,0,0,2,1) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when discharging one cell of the 4D midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,2,0,0,2,1)=8\,Z_{\mathrm{ex}}(0,2,0,0,2,1)$, where $Z_{\mathrm{ex}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of all coupling contributions at those indices.
background
The ambient module certifies, cell by cell, that the 4D Regge midpoint numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$ six times (two edge pairs and a tensor slot), matching the discrete curvature bookkeeping of the M2TT identity.
Upstream, m2Num is defined by folding contrib over couplingZList from zero, so it is a pure integer sum of coupling terms at a fixed multi-index. explicitZ is the matching closed-form table: a pattern-matched function $\mathrm{Fin},4^6\to\mathbb{Z}$ that returns small integers (typically $\pm 2,\pm 4$, or zero off the support).
Local setting (module doc): this file is chunk 2 of the 256 kernel decides that establish $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{ex}}$ pointwise.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines the numerator at $(0,2,0,0,2,1)$; the right-hand side multiplies the table lookup explicitZ 0 2 0 0 2 1 by eight. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one discharges one concrete cell so the assembly stays inside kernel limits.
In the Recognition gravity stack this identity is the algebraic core of the exact midpoint Regge M2TT relation in four dimensions: it converts a summed coupling expansion into a sparse closed form, which is what later curvature and continuum-limit arguments consume. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it is pure discrete-gravity bookkeeping that those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.