e_323211
plain-language theorem explainer
Pointwise identity: the folded Regge numerator at multi-index (3,2,3,2,1,1) equals eight times the explicit integer table at that same index. Gravity analysts cite it as one kernel cell in the 4D midpoint M2–TT certification. The proof is a single native decide on concrete Int values.
Claim. For indices $a{=}3,b{=}2,c{=}3,d{=}2,i{=}1,j{=}1$ in $\{0,1,2,3\}$, the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-cell kernel certification that the 4D Regge midpoint numerator matches an explicit integer table. The ambient setting is the exact midpoint M2–TT identity in discrete gravity: one must check, index by index on $(\mathrm{Fin},4)^6$, that a folded sum of coupling contributions agrees with a hand-written closed form.
The numerator $N=\texttt{m2Num}$ is defined by folding a fixed coupling list and summing a local contribution at each sextuple of indices. The comparison object $Z=\texttt{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern-match table (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on). The claim of the whole campaign is $N=8Z$ at every cell.
proof idea
Both sides are closed integer terms at a fully concrete sextuple, so no algebraic rewriting is needed. The proof is the single tactic decide, which evaluates the fold defining the numerator and the table lookup defining the explicit form, then checks integer equality.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one supplies one concrete cell of that kernel, so the assembly can treat the identity as a finished finite check rather than an open computation.
In the broader Recognition gravity stack this closes a discrete curvature/identity obligation in the 4D Regge midpoint analysis: once every cell satisfies $N=8Z$, the midpoint M2–TT algebraic identity is certified on the full index set. It is bookkeeping infrastructure, not a new physical law, but without the cell-by-cell match the exact discrete identity does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.