e_010211
plain-language theorem explainer
For the six-index slot (0,1,0,2,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}0$, $d{=}2$, $i{=}1$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $N(0,1,0,2,1,1)=8\,Z(0,1,0,2,1,1)$.
background
This module is chunk 1 of a 256-way case split proving that the Regge midpoint numerator equals eight times a closed-form kernel on all six-tuples in $(\mathrm{Fin},4)^6$. The numerator $N=m2Num$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The kernel $Z=explicitZ$ is an explicit integer-valued pattern on those same six indices (sample values include $4$, $-2$, and so on for distinguished index patterns).
The ambient setting is 4D Regge calculus at the exact midpoint of a simplex edge, where a mass-squared / TT-identity style algebraic identity is being certified by exhaustive finite check rather than by a symbolic closed form. Each chunk theorem pins one concrete six-tuple so the assembler can recombine them by fin_cases.
proof idea
One-line kernel decide: both sides are concrete Int values once the six Fin 4 arguments are fixed, so decide evaluates the fold defining the numerator against eight times the matching clause (or default) of the explicit kernel and closes equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by six nested fin_cases over Fin 4. That global identity is the algebraic certificate that the midpoint Regge numerator factors as eight times a sparse explicit kernel, a bookkeeping step inside the 4D gravity analysis stack. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure finite kernel hygiene supporting the Regge/TT side of the gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.