e_320232
plain-language theorem explainer
For the six-index tuple (3,2,0,2,3,2) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(3,2,0,2,3,2)$. Then the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2TT identity. The numerator $N$ (Lean m2Num) is defined by folding a fixed coupling list: start at $0$ and add each contribution term evaluated at the six Fin-4 indices. The explicit kernel $Z$ (Lean explicitZ) is a closed-form integer table on the same six indices, with sample values such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The local claim is one cell of the identity $N=8Z$. The module is chunk 14 of a 256-way split of the Fin-4 kernel, each cell discharged by a decidable integer equality. Upstream definitions supply only the table and the fold; no analytic closed form is assumed beyond those defs.
proof idea
One-line proof: decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted into the fold definition of the numerator and the pattern-match table for the explicit kernel. Lean’s kernel decides the resulting integer equality with no lemmas or rewriting.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple by nested fin_cases and invokes this cell (and its siblings) to conclude $\forall a,b,c,d,i,j,, N=8Z$. That global identity is the algebraic core of the 4D Regge exact-midpoint M2TT certificate in the Gravity analysis stack.
In the Recognition Science gravity line this certifies that the discrete curvature coupling numerator matches the explicit kernel used downstream for continuum comparison. It does not itself touch the T0–T8 forcing chain, $\phi$-ladder masses, or $\alpha$ band; it is pure index algebra supporting the Regge side of the gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.