e_321112
plain-language theorem explainer
For the multi-index $(3,2,1,1,1,2)$ on $\mathrm{Fin}\,4$, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one cell of the $4^6$ case split that proves the global $m_2$ numerator identity. The proof is a single `decide` on the certified kernel.
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 on six indices, one has $N(3,2,1,1,1,2)=8\,Z(3,2,1,1,1,2)$.
background
This module is chunk 14 of a 256-way kernel certification that the four-dimensional Regge midpoint $m_2$ numerator equals eight times an explicit integer table. Indices run in $\mathrm{Fin},4$, matching the four spacetime directions in the TT (transverse-traceless) sector.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at $0$. The explicit kernel $Z$ is a pure pattern-match on those same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero support.
The local claim is one concrete cell of that table: the multi-index $(3,2,1,1,1,2)$. Sibling chunks cover the other cells; the assembly theorem quantifies over all six indices.
proof idea
One-line computational proof: decide evaluates both sides on the concrete $\mathrm{Fin},4$ tuple and checks integer equality. No algebraic rewriting is needed; the kernel certificate and the fold definition are closed enough for the decision procedure.
why it matters
The parent theorem is the full identity $\forall a,b,c,d,i,j,, N=8Z$, proved by nested fin_cases that dispatch to these chunk lemmas (including this one). That identity is the algebraic backbone of the exact midpoint $m_2$ TT analysis in the Regge gravity sector of the monolith.
In the broader Recognition framework this sits in the gravity analysis layer rather than the T0–T8 forcing chain: it certifies a discrete curvature/coupling identity used when matching continuum limits and ladder normalizations, not a derivation of $\phi$, $D=3$, or the eight-tick octave. Closing every chunk removes scaffolding from the $m_2$ numerator claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.