e_310131
plain-language theorem explainer
For the six-index tuple (3,1,0,1,3,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell in the exhaustive 4^6 case split that certifies the Regge exact-midpoint M2 TT identity in four dimensions. The proof is a single kernel decide on integer equality.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,1,3,1)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel: $m_2^{\mathrm{num}}(3,1,0,1,3,1)=8\,Z_{\mathrm{explicit}}(3,1,0,1,3,1)$.
background
This module sits in the Gravity analysis stack that certifies an exact midpoint identity for the Regge M2 TT sector in four dimensions. The local claim, stated in the module doc, is that the numerator m2Num equals eight times a closed-form integer kernel explicitZ, discharged in 256 decide chunks.
m2Num is defined by folding a fixed coupling list: it accumulates contrib t a b c d i j over every term t in couplingZList, starting from 0. explicitZ is a pattern-matched integer table on six Fin 4 indices (sample clauses send $(0,0,1,1,2,2)$ and $(0,0,1,1,3,3)$ to $4$, and several off-diagonal patterns to $-2$). Both live in the KernelCert module imported here.
The six arguments run over the discrete 4D index set, so the full identity is a finite check of $4^6=4096$ cells; this file owns chunk 13 of that partition.
proof idea
One-line proof: by decide. Lean reduces both sides of the integer equality for the concrete indices $(3,1,0,1,3,1)$ and confirms they match. No lemmas are invoked beyond the reducible definitions of m2Num (the fold over couplingZList) and explicitZ (the pattern table).
why it matters
The 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 exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies a concrete cell so the assemble step can close without re-deciding the whole table in one place.
In the Recognition gravity stack this identity is infrastructure for the Regge exact-midpoint M2 TT analysis in 4D, not a direct T0–T8 forcing step. It keeps the discrete curvature/coupling algebra on a certified integer footing before continuum or phenomenological claims are attached. No open scaffold remains on this cell: the decide closes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.