e_222001
plain-language theorem explainer
At multi-index (2,2,2,0,0,1) the folded Regge midpoint M2 numerator equals eight times the explicit kernel integer. Gravity analysts cite it as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete Int equality after unfolding both sides.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,2,2,0,0,1)$ with each entry in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-cell kernel certification that the midpoint M2 numerator equals eight times an explicit integer table on $(\mathbb{F}_4)^6$. The setting is 4D Regge calculus analysis inside the Gravity domain of Recognition Science: discrete curvature couplings are reduced to finite integer arithmetic so the identity can be machine-checked.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a large pattern-match table (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). Both live in the KernelCert module imported here.
Sibling theorems in the same chunk discharge neighboring multi-indices the same way; the assemble module then quantifies over all six Fin 4 arguments.
proof idea
One-line kernel proof: by decide. Lean unfolds m2Num 2 2 2 0 0 1 (the fold of contrib over couplingZList) and explicitZ 2 2 2 0 0 1 (the matching clause of the explicit table), reduces both sides to concrete integers, and checks $n = 8\cdot z$ by the decidable equality instance on Int. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j:\mathbb{F}_4,; m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases, each leaf a chunk theorem of this form. This declaration is the leaf for $(2,2,2,0,0,1)$.
In the broader Gravity analysis stack, the identity certifies that the midpoint M2 TT coupling in 4D Regge calculus collapses to a sparse explicit kernel, replacing a symbolic fold by a lookup. That reduction is bookkeeping for discrete curvature identities used downstream in the RS gravity pipeline; it does not itself invoke the T0–T8 forcing chain, but it keeps the 4D geometric side fully machine-checked.
Open scaffolding risk is only combinatorial: every Fin 4 sextuple must appear in some chunk. Missing a cell would leave a hole in the assemble proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.