e_223232
plain-language theorem explainer
For the six-index tuple (2,2,3,2,3,2) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=2$, $c=3$, $d=2$, $i=3$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-cell case split proving that the 4D Regge midpoint M2 TT numerator equals eight times an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$. The local slogan is $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $Z_{\mathrm{explicit}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer values (e.g. $4$, $-2$, and zeros off-pattern).
The ambient setting is exact algebraic certification of a discrete gravity identity (Regge calculus, midpoint evaluation, TT sector in four dimensions), not a continuum limit argument.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the decision procedure checks integer equality with no lemmas or rewriting. No induction and no appeal to the fold structure beyond evaluation.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by nested fin_cases on all six indices; each leaf is one of these chunk equalities. This cell is the leaf for $(2,2,3,2,3,2)$.
In the Recognition gravity stack, the certified M2 TT midpoint identity is infrastructure for discrete curvature and coupling bookkeeping on the eight-tick / 4D side of the forcing chain (T7 octave structure, T8 $D=3$ spatial plus time). Closing every kernel cell removes a scaffolding gap between the folded numerator and the closed-form integer table used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.