e_212033
plain-language theorem explainer
For the six-index slot (2,1,2,0,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite this as one of the 256 kernel cells that assemble the exact midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the coupling-fold numerator satisfies $m_2^{\mathrm{num}}(2,1,2,0,3,3)=8\,Z_{\mathrm{expl}}(2,1,2,0,3,3)$, where $Z_{\mathrm{expl}}$ is the explicit integer table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the fixed coupling list.
background
This module is chunk 9 of a 256-cell kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ equals eight times an explicit integer table $Z_{\mathrm{expl}}$ on every six-tuple of Fin-4 indices. The setting is 4D discrete gravity: midpoint evaluation of the M2–TT identity that relates curvature/coupling data on the lattice.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of contrib over couplingZList, starting from 0. The companion table explicitZ is a total function Fin 4^6 → ℤ with hard-coded integer values on each pattern (e.g. 4, −2, …). The claim here is only the single cell with arguments (2,1,2,0,3,3).
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers (the fold for m2Num and the matching clause of explicitZ), so the equality is discharged by Lean’s decision procedure on Int arithmetic with no lemmas or case splits in this file.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement ∀ a b c d i j, m2Num = 8 · explicitZ by exhaustive fin_cases on Fin 4; each leaf is one of these chunk theorems. Closing all 256 cells certifies the exact midpoint M2–TT numerator identity used in the 4D Regge/gravity analysis stack. It is bookkeeping infrastructure rather than a new physical law, but without it the global algebraic identity remains unproved in the mirror.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.