e_312122
plain-language theorem explainer
For the six-index tuple (3,1,2,1,2,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell in the 4D Regge midpoint M2 identity grid. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(3,1,2,1,2,2)$ equals $8$ times the explicit integer kernel at the same indices: $N(3,1,2,1,2,2)=8\,Z(3,1,2,1,2,2)$.
background
This module is chunk 13 of a 256-cell decide grid establishing that the folded 4D midpoint numerator equals eight times an explicit integer kernel on every sextuple of Fin-4 indices. The setting is exact algebraic bookkeeping for a Regge-style midpoint identity in four dimensions, not continuum GR.
The numerator $N=m2Num$ is defined by folding a fixed coupling list and summing a local contribution at each term for the six indices. The kernel $Z=explicitZ$ is a sparse pattern of small integers (e.g. $\pm 2,4$) on selected index patterns, zero elsewhere by the match default.
Upstream, both $N$ and $Z$ live in the kernel certificate module; this chunk only evaluates one concrete cell.
proof idea
One-line decide on a ground equality of integers. Lean reduces $m2Num,3,1,2,1,2,2$ by evaluating the fold over the coupling list, reduces $explicitZ,3,1,2,1,2,2$ by the match table, multiplies by 8, and checks equality in $\mathbb{Z}$. No lemmas beyond kernel reduction.
why it matters
Feeds the assembler theorem $m2Num_eq_eight_explicitZ$, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N=8Z$ by exhaustive $fin_cases$ on all six indices. Each chunk such as this one discharges one concrete branch so the global identity is a pure case split rather than a symbolic sum argument.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint M2/TT bookkeeping in 4D Regge-type analysis. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; it is a finite combinatorial certificate those layers can trust when they quote the assembled equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.