e_312001
plain-language theorem explainer
For the six-index tuple (3,1,2,0,0,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 point-checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}2$, $d{=}0$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $N(3,1,2,0,0,1)=8\,Z(3,1,2,0,0,1)$.
background
This module is chunk 13 of a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on all six-tuples in $(\mathrm{Fin},4)^6$. The local slogan is $m2Num = 8\cdot explicitZ$.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. The closed form $Z$ is a sparse pattern of small integers (e.g. $\pm 2,,4$) on selected index patterns and zero elsewhere.
The ambient setting is 4D Regge calculus analysis for the midpoint $M_2$ identity in the Recognition Science gravity stack. Each chunk theorem pins one concrete six-tuple so the assembler can recombine them by exhaustive fin_cases.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values for the fixed indices $(3,1,2,0,0,1)$, so the equality is discharged by computational reflection with no lemmas beyond the definitions of the folded numerator and the explicit kernel.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N=8Z$ by six nested fin_cases over the 256 points. Without each chunk equality the global identity does not close.
In the gravity analysis path this identity is the algebraic certificate that the midpoint $M_2$ numerator matches the explicit kernel used downstream in Regge curvature bookkeeping. It is pure discrete linear algebra on $\mathrm{Fin},4$ indices, not a continuum GR claim, but it is a required exact step before continuum or continuum-limit statements can be trusted.
No open scaffolding remains on this point: the decide closes the cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.