e_212010
plain-language theorem explainer
For the six-index tuple (2,1,2,0,1,0) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,2,0,1,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(2,1,2,0,1,0)=8\,Z_{\mathrm{explicit}}(2,1,2,0,1,0)$.
background
The ambient module certifies the exact midpoint M2–TT identity in 4D Regge calculus by checking that a folded numerator equals eight times an explicit integer kernel on every cell of $(\mathrm{Fin},4)^6$. The module doc frames this file as chunk 9 of that 256-cell decide sweep.
Upstream, m2Num is the integer obtained by folding contrib over couplingZList at a fixed six-index address. 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$ on diagonal-type pairs, $-2$ on crossed pairs). The claim is the pointwise equality of those two integers at one concrete address.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (the fold on the left, the pattern match on the right), and Lean’s kernel decision procedure discharges the equality with no lemmas or rewriting.
why it matters
This cell is one brick in the exhaustive cover that yields the universal statement m2Num_eq_eight_explicitZ: $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$. That assembled identity is the algebraic core of the exact 4D Regge midpoint M2–TT certification in the Gravity analysis stack. Without the chunk-wise decides, the fin_cases assembly cannot close. It is pure discrete kernel bookkeeping, not a continuum GR derivation, but it is required scaffolding for the exact discrete identity the framework uses on the gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.