e_220100
plain-language theorem explainer
For the six-index slot (2,2,0,1,0,0) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2 TT identity. The proof is a single kernel decide on integer equality.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator at $(2,2,0,1,0,0)$ equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(2,2,0,1,0,0)=8\,Z_{\mathrm{ex}}(2,2,0,1,0,0)$.
background
This module is chunk 10 of a case-split certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a sparse explicit integer kernel $Z_{\mathrm{ex}}$. Both maps take six $\mathrm{Fin},4$ indices (two edge pairs and a tensor slot).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each contribution at the given indices. $Z_{\mathrm{ex}}$ is a pattern-matched integer table (entries such as $4$, $-2$, and $0$ on complementary slots). The local goal is pure integer identity on one concrete multi-index, not a continuum limit argument.
The surrounding Gravity.Analysis development treats the full identity as $4^6$ finite checks, partitioned into decide chunks so the kernel can discharge each slot without a hand-written algebraic expansion.
proof idea
One-line proof: decide. Lean evaluates both sides of the integer equality at the concrete indices $(2,2,0,1,0,0)$ and accepts definitional equality. No lemmas beyond the evaluable definitions of $m_2^{\mathrm{num}}$ and $Z_{\mathrm{ex}}$ are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 slot into the global statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$, by exhaustive fin_cases. This chunk entry supplies the $(2,2,0,1,0,0)$ obligation inside that cover.
In the Recognition gravity stack, the identity is bookkeeping for the exact midpoint Regge M2 TT kernel in four dimensions: once numerator and explicit table match everywhere, later curvature and continuum comparisons can quote a single closed form instead of the folded coupling sum. It is infrastructure, not a new dynamical law; it does not by itself force $D=3$ or the eight-tick octave, but it hardens the 4D discrete gravity layer those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.