e_211330
plain-language theorem explainer
For the multi-index (2,1,1,3,3,0) on Fin 4, the folded Regge coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts cite it when assembling the full 4D midpoint identity m2Num = 8·explicitZ. The proof is a single kernel decide on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. For $(a,b,c,d,i,j)=(2,1,1,3,3,0)$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel table entry at those indices.
background
This module is one chunk of the 4D Regge exact-midpoint certification: it records that the folded numerator equals eight times a sparse explicit kernel table, case by case over Fin 4 sextuples (256 decides in total; this file is chunk 9).
The numerator m2Num is defined by folding a fixed coupling list: start at 0 and add a contribution for each coupling term at the six indices. The comparison target explicitZ is a hand-written Int-valued table on Fin 4^6 (nonzero only on a thin set of index patterns such as (0,0,1,1,2,2)mapsto 4 and several -2 entries).
Both definitions live in the KernelCert module imported here. The local goal is only the equality at one concrete sextuple, not the universal statement.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals (left via the fold definition of the numerator, right via the match table for the explicit kernel), so the decidable Int equality closes with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every Fin 4 sextuple and is proved by exhausting all six indices with fin_cases. Each chunk theorem such as this one discharges one concrete cell of that 4^6 grid.
In the gravity analysis stack this identity is the algebraic backbone of the Regge exact-midpoint M2 TT certificate in 4D: it replaces a folded coupling sum by an eightfold multiple of a sparse explicit kernel, which is what downstream curvature and continuum-limit arguments actually consume. It is pure finite combinatorics on Fin 4; it does not itself invoke the RS forcing chain (T5–T8) or the J-cost, but it sits inside the discrete gravity layer those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.