e_021232
plain-language theorem explainer
For the six-index slot (0,2,1,2,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=2$, $c=1$, $d=2$, $i=3$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,1,2,3,2)=8\,Z(0,2,1,2,3,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices appear. The numerator $N(a,b,c,d,i,j)$ is obtained by folding a fixed coupling list and summing each term's contribution at those indices. The companion map $Z$ is an explicit piecewise integer table (values such as $4$, $-2$, and so on) that is meant to be the closed form of that fold.
The local module is chunk 2 of a 256-case kernel certification: each theorem pins one concrete six-tuple so that the global identity $N=8Z$ can be assembled by exhaustive case split. The setting is pure finite arithmetic over $\mathrm{Fin},4$; no continuum limit or metric signature is invoked at this layer.
proof idea
One-line decide proof. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the pattern table for the explicit kernel; the kernel checker confirms equality.
why it matters
Feeds the parent assembly theorem that states $\forall a,b,c,d,i,j,, N=8Z$ by nested fin_cases over all six indices. That global identity is the algebraic core of the exact midpoint M2 TT certificate in 4D Regge gravity analysis. Within Recognition Science gravity work it is bookkeeping infrastructure rather than a forcing-chain landmark: it closes one cell of the discrete kernel so higher curvature or mass-ladder arguments can treat the midpoint identity as proved rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.