e_220122
plain-language theorem explainer
One kernel cell of the Regge midpoint identity: the folded coupling numerator at index sextuple (2,2,0,1,2,2) equals eight times the explicit integer table at those indices. Gravity analysts cite it only as a discharged case inside the full Fin-4 exhaustion. The proof is a single computational decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,2,0,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table entry: $N(2,2,0,1,2,2)=8\,Z(2,2,0,1,2,2)$.
background
This module is chunk 10 of a 256-cell kernel certifying that the folded numerator of the 4D Regge exact-midpoint $M_2$ TT identity agrees with eight times a closed-form integer table on every sextuple of $\mathrm{Fin},4$ indices.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry. The table $Z$ is an explicit pattern-matched map $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$). Both live in the kernel-cert module imported here.
The local goal is purely arithmetic: evaluate both sides at one fixed sextuple and check equality in $\mathbb{Z}$.
proof idea
One-line computational proof: decide. Lean reduces both the fold that defines the numerator and the pattern match that defines the table at the concrete indices $(2,2,0,1,2,2)$, then checks the resulting integer equality. No lemmas are invoked beyond the decidability of integer equality on closed terms.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal claim by six nested fin_cases sweeps. Each chunk theorem such as this one closes one concrete cell of that $4^6$ grid so the assembler need not re-decide the arithmetic inline.
In the broader Gravity analysis stack this identity is bookkeeping for the exact midpoint form of the 4D Regge $M_2$ TT kernel: once numerator and table match everywhere, downstream curvature and continuum-limit arguments can quote the closed table instead of the fold. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure inside the discrete gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.