e_212203
plain-language theorem explainer
At multi-index (2,1,2,2,0,3) on (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one of the 256 kernel cells in the m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}2,\,d{=}2,\,i{=}0,\,j{=}3$ in $\mathbb{F}_4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value at that multi-index.
background
This module is chunk 9 of a 256-cell kernel certification that the 4D Regge midpoint numerator matches a closed integer table. The ambient setting is exact midpoint identities for discrete gravity couplings on a 4-simplex skeleton with indices in $\mathbb{F}_4$.
The numerator is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The comparison target is an explicit pattern-matched integer table on $(\mathrm{Fin},4)^6$, with sample values such as $4$, $-2$, and so on at distinguished index patterns.
The local claim is only one concrete cell of that table identity. Sibling theorems cover the other multi-indices; the assembly theorem quantifies over all six indices.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold of contributions versus eight times the table entry), so the equality is discharged by Lean's decision procedure on closed integer arithmetic. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,,\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and proves it by exhaustive fin_cases on each $\mathrm{Fin},4$ coordinate, dispatching each cell to a chunk theorem of this form.
In the gravity analysis stack this closes the numerator side of the Regge exact-midpoint M2/TT identity in 4D: once every kernel cell matches, the folded coupling is interchangeable with the explicit table. That identity is bookkeeping inside discrete curvature/coupling algebra rather than a forcing-chain landmark (T5–T8), but it is required scaffolding for certified 4D Regge identities used downstream in the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.