e_211003
plain-language theorem explainer
For the six-index slot (2,1,1,0,0,3) on Fin 4, the folded Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2–TT identity. The proof is a single `decide` on the concrete integer equality after unfolding the fold and the pattern match.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(2,1,1,0,0,3)$. Writing $m_2^{\mathrm{num}}$ for the folded coupling numerator and $Z_{\mathrm{ex}}$ for the explicit integer kernel, one has $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{ex}}(a,b,c,d,i,j)$.
background
The module is one chunk of the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple in $(\mathrm{Fin},4)^6$. There are $4^6=4096$ slots; they are partitioned into decide-chunks (here chunk 9).
Upstream, m2Num is defined by folding contrib over couplingZList, yielding an Int for each six-index. explicitZ is the closed pattern-match table that returns the expected kernel integer (e.g. $\pm 2,\pm 4$, or $0$ off the listed patterns). The local goal is only the single equality at indices $(2,1,1,0,0,3)$.
proof idea
One-line computational proof: by decide. Lean unfolds m2Num (the fold of contrib over the coupling list) and explicitZ (the pattern match) at the concrete Fin-4 literals, reduces both sides to integer numerals, and checks equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ by exhaustive fin_cases on all six indices and discharge of each leaf by a chunk theorem of this form. That global identity is the algebraic core of the 4D Regge midpoint M2–TT kernel certificate in the Gravity analysis stack. It does not itself touch the RS forcing chain (T5–T8) or the J-cost; it is pure discrete-gravity bookkeeping needed before continuum or phenomenological claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.