e_321013
plain-language theorem explainer
For the Fin-4 sextuple (3,2,1,0,1,3), the folded M2 coupling numerator equals eight times the explicit integer Z-table entry. Cited by the assembly theorem that universalizes N2=8Z over all 4^6 index tuples in the 4D Regge midpoint analysis. Proof is a single kernel decide evaluating both closed definitions at that concrete point.
Claim. For indices $(a,b,c,d,i,j)=(3,2,1,0,1,3)$ with each index in $\{0,1,2,3\}$, the folded M2 numerator equals eight times the explicit Z-table value: $N_2(3,2,1,0,1,3)=8\,Z(3,2,1,0,1,3)$.
background
In the 4D Regge exact-midpoint analysis, the M2 numerator on a six-tuple of Fin-4 indices is the integer fold $N_2(a,b,c,d,i,j)=\sum_{t\in L}C(t;a,b,c,d,i,j)$ over a fixed coupling list $L$. The companion object $Z$ is an explicit pattern-matched table $(\mathbb{F}_4)^6\to\mathbb{Z}$, with representative values such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
This module is chunk 14 of a 256-case kernel certification that $N_2=8Z$ holds pointwise. Upstream, only the two definitions (the fold and the table) are required; no analytic lemmas intervene. The parent assembly then reintroduces the universal quantifier by exhaustive fin_cases on all six indices.
proof idea
One-line wrapper: decide fully evaluates the fold that defines the numerator and the pattern match that defines the explicit table at the concrete sextuple $(3,2,1,0,1,3)$, then checks the resulting integer equality in the kernel. No intermediate lemmas are applied.
why it matters
Feeds the assembly theorem that states $\forall a,b,c,d,i,j\in\mathbb{F}_4,\ N_2=8Z$, whose proof is six nested Fin-4 case splits discharging one kernel fact per cell. That global identity is the algebraic core of the exact midpoint M2 TT relation in the 4D Regge gravity sector. It is infrastructure for discrete curvature bookkeeping on the recognition lattice rather than a step of the T0-T8 forcing chain, but it is required machinery once the gravitational analysis is opened.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.