e_021323
plain-language theorem explainer
For the fixed index sextuple (0,2,1,3,2,3) on Fin 4, the folded numerator m2Num equals eight times the explicit Z-table entry. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT kernel identity. The proof is a single kernel decide on two concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,2,1,3,2,3)=8\,Z_{\mathrm{explicit}}(0,2,1,3,2,3)$.
background
The module is one chunk of the 4D Regge exact-midpoint M2TT identity: it asserts casewise that the folded numerator equals eight times a closed-form integer table. Here $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList, accumulating each term's contribution at those six indices. The companion table $Z_{\mathrm{explicit}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero values (e.g. $4$ on matched pairs such as $(0,0,1,1,2,2)$, $-2$ on crossed pairs).
Chunk 2 packages 256 such kernel decides. The ambient goal is the pointwise identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ on every sextuple, which underpins the exact midpoint analysis of the discrete gravity kernel.
proof idea
One-line proof: decide. Both sides reduce to concrete integers (the fold over the coupling list versus eight times the table lookup at $(0,2,1,3,2,3)$), so the kernel discharges equality by computation. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z_{\mathrm{explicit}}$ are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhausting all sextuples. That universal identity is the certified algebraic core of the 4D Regge exact-midpoint M2TT analysis in the Gravity domain. Without the chunk decides, the fold-versus-table match stays uncertified. It is pure discrete-kernel bookkeeping, not a continuum GR claim, and does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.