e_202022
plain-language theorem explainer
For the multi-index (2,0,2,0,2,2) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts building the 4D Regge midpoint M2–TT identity cite these per-cell equalities when assembling the global identity. The proof is a single kernel decide on concrete integers.
Claim. For $a=2$, $b=0$, $c=2$, $d=0$, $i=2$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-cell kernel certificate for the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator equals eight times an explicit integer table on every multi-index in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at those six indices. The comparison table $Z_{\mathrm{explicit}}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
Local setting: each chunk theorem pins one concrete cell so the global assembly can discharge all $4^6$ cases without re-deriving the fold.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed at $(2,0,2,0,2,2)$, so the kernel equality checker closes the goal with no lemmas or rewriting.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proceeds by exhaustive fin_cases on the six indices. This cell is one of the 256 kernel decides that underwrite that universal identity.
In the Recognition gravity stack, the Regge midpoint M2–TT identity is analytic scaffolding for discrete curvature bookkeeping in 4D. Closing the numerator-versus-table match cell-by-cell keeps the certificate fully computational and free of analytic gaps at this layer. No T0–T8 forcing step is invoked here; the link is purely to the gravity-analysis kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.