e_233202
plain-language theorem explainer
For the six-index tuple (2,3,3,2,0,2) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT kernel identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a{=}2,b{=}3,c{=}3,d{=}2,i{=}0,j{=}2$ in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,3,3,2,0,2)=8\,Z_{\mathrm{expl}}(2,3,3,2,0,2)$.
background
This module is chunk 11 of a 256-cell case split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on the 4D Regge exact-midpoint M2TT kernel. Indices run over $\mathrm{Fin},4$, i.e. discrete edge/face labels in the 4-simplex bookkeeping.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing the local contribution of each coupling term at those six indices. The comparison object $Z_{\mathrm{expl}}$ is an explicit integer-valued pattern match on the same six indices (sample clauses return $4$, $-2$, etc.).
The local goal is purely arithmetic: evaluate both sides at one fixed multi-index and check equality in $\mathbb{Z}$.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted: the fold defining the numerator becomes a finite sum of known contributions, and explicitZ hits a single match clause (or the default). Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas and no manual algebra.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ and proves it by nested fin_cases, each leaf a chunk theorem of this form. This declaration is the leaf for $(2,3,3,2,0,2)$.
In the gravity stack the identity certifies that the folded midpoint numerator agrees with the closed-form eightfold explicit kernel, a bookkeeping step inside the 4D Regge exact-midpoint M2TT analysis. It does not itself invoke Recognition forcing (T5–T8) or the mass ladder; it is pure discrete kernel arithmetic supporting the continuum gravity side of the mirror.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.