e_033201
plain-language theorem explainer
For the fixed multi-index $(0,3,3,2,0,1)$ on $\mathrm{Fin}\,4$, the summed Regge coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts cite it as one atomic cell in the exhaustive $4^6$ case split that proves the global $m_2$ numerator identity. The proof is a single kernel decision 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(0,3,3,2,0,1)=8\,Z(0,3,3,2,0,1)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed list of coupling terms: each term contributes an integer depending on the six $\mathrm{Fin},4$ indices, and the fold starts from $0$. The comparison object $Z$ is an explicit case-table $\mathrm{Fin},4^6\to\mathbb{Z}$ listing the closed-form kernel values (e.g. $4$, $-2$, and so on on the diagonal and off-diagonal patterns).
Module documentation states the local goal bluntly: prove $N=8\cdot Z$ on chunk 3 by 256 kernel decides. Upstream, both $N$ and $Z$ live in the kernel-certificate file; this chunk only instantiates one sextuple.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold for $N$ on the fixed indices, and the matching clause of the $Z$ table) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
The parent theorem is the universal statement that $N(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ for every sextuple in $\mathrm{Fin},4$. That assembler runs nested fin_cases on all six indices and discharges each leaf by a chunk theorem of this form. Establishing the factor-of-eight match between the summed coupling numerator and the explicit kernel is a concrete algebraic step inside the 4D Regge midpoint TT-identity analysis used in the gravity sector of the monolith. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is infrastructure for the discrete curvature bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.