e_220132
plain-language theorem explainer
For the six-index tuple (2,2,0,1,3,2) in Fin 4, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts assembling the full Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator at $(2,2,0,1,3,2)$ equals eight times the explicit integer table: $m_2^{\mathrm{num}}(2,2,0,1,3,2)=8\,Z_{\mathrm{exp}}(2,2,0,1,3,2)$.
background
This module is chunk 10 of a 256-cell kernel certification that the Regge exact-midpoint numerator equals eight times a closed integer table on $(\mathrm{Fin},4)^6$. The local claim is one concrete cell of that table identity.
Upstream, m2Num is defined by folding contrib over couplingZList, yielding an integer for each six-tuple of face indices. explicitZ is the matching closed-form table: a pattern-matched function $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$) on selected index patterns.
The surrounding Gravity.Analysis development treats these equalities as decidable integer identities, split into chunks so each cell can be certified by the kernel without a monolithic proof term.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed: the fold defining the numerator evaluates fully, and the pattern match for the explicit table returns a single Int. Lean’s kernel decision procedure checks equality of those integers. No lemmas beyond the two definitions are invoked.
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{exp}}$ by exhausting all $\mathrm{Fin},4$ cases; this cell is one of the 256 branches that discharge. The identity is infrastructure for the Regge exact-midpoint M2TT analysis in the Gravity domain, not a forcing-chain (T0–T8) step. It closes a scaffolding slice of the numerator/table match so downstream curvature or continuum-limit arguments can quote a proved algebraic identity rather than a numeric check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.