e_323213
plain-language theorem explainer
For the fixed multi-index $(3,2,3,2,1,3)$ on $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full Regge midpoint $M_2$ identity over all $4^6$ index sextuples. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the fold of coupling contributions over the fixed coupling list and $Z$ for the explicit integer kernel table, one has $N(3,2,3,2,1,3)=8\,Z(3,2,3,2,1,3)$.
background
This module is chunk 14 of a 256-way split that certifies the algebraic identity $N=8Z$ pointwise on $\mathrm{Fin},4^6$. The ambient setting is the exact midpoint $M_2$ identity for 4D Regge calculus used in the Recognition Science gravity analysis.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: each term contributes an integer $\mathrm{contrib}$ at the six indices, and the fold starts from $0$. The comparison value $Z=\mathrm{explicitZ}$ is an explicit case table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The chunk theorems discharge one concrete sextuple each so the assembler can recombine them by exhaustive $\mathrm{fin_cases}$.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are literals, so the kernel evaluates the fold defining $N$ and the matching clause of $Z$ and checks equality. No lemmas beyond the definitions of $\mathrm{m2Num}$ and $\mathrm{explicitZ}$ are invoked.
why it matters
Parent theorem is $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and proves it by nested $\mathrm{fin_cases}$ that land on these chunk equalities (including this one). The identity is the numerical heart of the Regge exact-midpoint $M_2$ certification in 4D: it replaces a folded coupling sum by a closed integer kernel, enabling later gravity-analysis steps that treat the midpoint contribution as an explicit sparse table rather than a symbolic fold. Within Recognition Science this sits in the gravity analysis layer that supports continuum limits built on the forced $D=3$ spatial skeleton and the discrete tick structure; it does not itself touch the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.