e_022201
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (0,2,2,2,0,1) equals eight times the explicit integer table at that same index. Gravity analysts cite it as one kernel cell in the 4D m2Num = 8·Z certification. The proof is a single decidability check on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,2,2,0,1)$ on $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,2,2,2,0,1)=8\,Z(0,2,2,2,0,1)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator coincides with eight times an explicit integer table. Indices run over $\mathrm{Fin},4$ sextuples $(a,b,c,d,i,j)$.
The numerator $N$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the given multi-index. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on distinguished index patterns).
The local goal is purely algebraic bookkeeping: verify $N=8Z$ at one concrete cell so a later exhaustive assembly can conclude the identity for every sextuple.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,2,2,2,0,1)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the pattern-matched table entry by eight. Both are closed integer expressions, so the equality is discharged by the decidable equality instance on $\mathbb{Z}$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by nested fin_cases over all six $\mathrm{Fin},4$ arguments, invoking one kernel cell theorem per case. This chunk (module doc: "m2Num = 8·explicitZ, chunk 2") is mechanical scaffolding inside the Gravity analysis stack for the Regge exact-midpoint M2 TT identity in 4D.
In the broader Recognition Science gravity program, certifying that the folded numerator matches a sparse explicit table is the computational bottleneck before continuum or continuum-limit comparisons. The result does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure for the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.