e_313001
plain-language theorem explainer
For the six-index slot (3,1,3,0,0,1) on Fin 4, the folded Regge numerator coupling equals eight times the explicit integer kernel entry. Gravity analysts cite it as one atomic case in the exhaustive 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded numerator coupling at $(a,b,c,d,i,j)=(3,1,3,0,0,1)$ satisfies $m_2^{\mathrm{num}}(3,1,3,0,0,1)=8\,Z(3,1,3,0,0,1)$, where $Z$ is the explicit integer kernel table.
background
This module is chunk 13 of the certified identity $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge midpoint kernel. Indices run over $\mathrm{Fin},4$, so six slots give a finite table of integer equalities.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of contrib over couplingZList, summing integer coupling contributions at that multi-index. The comparison value $Z$ is the sparse explicit table explicitZ: a pattern-matched map $\mathrm{Fin},4^6\to\mathbb{Z}$ with nonzero entries such as $4$ on diagonal-type slots and $-2$ on mixed pairs.
The local goal is mechanical: discharge one concrete six-tuple so the assembler can reassemble the universal statement by fin_cases.
proof idea
One-line decide. Both sides reduce to closed integer expressions at the fixed indices $(3,1,3,0,0,1)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via the pattern match on $Z$ (or zero if unmatched). The kernel checks integer equality; no lemmas beyond the two defs are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases, each leaf a chunk theorem of this form. This declaration is the leaf for $(3,1,3,0,0,1)$.
In the gravity analysis stack, that universal identity is the certified algebraic core of the Regge exact midpoint M2–TT relation in 4D: the folded coupling numerator is exactly eight times the explicit kernel. Without the chunk leaves, the assembler cannot close. It is pure finite-check scaffolding for the continuum/Regge comparison, not a continuum PDE statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.