e_201211
plain-language theorem explainer
For the six-index slot (2,0,1,2,1,1) on Fin 4, the folded numerator m2Num equals eight times the tabulated explicitZ value. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on both integer sides.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,2,1,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(2,0,1,2,1,1)=8\,Z_{\mathrm{explicit}}(2,0,1,2,1,1)$.
background
This module is chunk 8 of a case-split certification that the 4D Regge-midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a closed integer table $Z_{\mathrm{explicit}}$. Both maps take six $\mathrm{Fin},4$ indices and return an Int.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding contrib over couplingZList from zero. The table $Z_{\mathrm{explicit}}$ is a pattern-match on the six indices (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$). The local goal is only the single multi-index $(2,0,1,2,1,1)$ inside that finite grid.
proof idea
One-line decide. Lean’s kernel evaluates both the fold that defines $m_2^{\mathrm{num}}$ at $(2,0,1,2,1,1)$ and the matching clause of $Z_{\mathrm{explicit}}$, then checks the integer equality against the factor $8$. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhausting $\mathrm{Fin},4$ on each slot. This chunk supplies one concrete cell of that exhaustion (module doc: “m2Num = 8·explicitZ, chunk 8 (256 kernel decides)”).
In the gravity analysis stack the identity is the algebraic backbone of the exact midpoint M2TT kernel certificate: once every cell matches, the numerator may be replaced by the sparse explicit table in downstream curvature and mass-gap arguments. It is pure discrete bookkeeping, not a continuum GR claim, and does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.