e_231122
plain-language theorem explainer
One kernel case of the 4D midpoint Regge identity: the folded coupling numerator at multi-index (2,3,1,1,2,2) equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it only as a brick in the full six-index identity. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,1,1,2,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator in 4D coincides with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, matching the four spacetime directions of the discrete calculus.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each coupling triple for the six free indices. The comparison target explicitZ is a sparse pattern-matched table $\mathrm{Fin},4^6\to\mathbb{Z}$ (typical nonzero values $\pm 2,,4$) that packages the same combinatorics in closed form.
The local claim is only the single tuple $(2,3,1,1,2,2)$. Sibling chunks cover the remaining tuples; the assembly theorem quantifies over all six indices.
proof idea
One-line computational discharge: decide evaluates both sides at the concrete six-tuple. The left side runs the fold that defines the numerator; the right side multiplies the table value of the explicit kernel by eight. No lemmas are invoked beyond the two definitions and decidable integer equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and is proved by exhausting $\mathrm{Fin},4$ on each index. That global identity is the algebraic core of the exact midpoint $m_2$ TT identity in the 4D Regge analysis stack.
Within Recognition Science gravity work, the identity certifies that the discrete curvature coupling used downstream matches its closed kernel, so later continuum or continuum-limit arguments can quote the factor-of-eight form without re-expanding the fold. It is pure kernel bookkeeping: no appeal to the forcing chain (T0–T8), RCL, or $\phi$-ladder is required here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.