e_022013
plain-language theorem explainer
For the six-index slot (0,2,2,0,1,3) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one atomic case in the exhaustive midpoint M2TT identity. The proof is a single kernel decide on integer arithmetic.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,2,2,0,1,3)=8\,Z_{\mathrm{ex}}(0,2,2,0,1,3)$, where $Z_{\mathrm{ex}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the fixed coupling list.
background
This module sits in the Gravity analysis stack for the exact midpoint form of a 4D Regge M2TT identity. The local goal, per the module doc, is to certify $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{ex}}$ on a chunk of the six-index kernel by pure decision.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of contrib over couplingZList, yielding an integer. The comparison target $Z_{\mathrm{ex}}$ is an explicit six-argument integer function on $\mathrm{Fin},4$, tabulated on the sparse support of the coupling (e.g. value $4$ on $(0,0,1,1,2,2)$, $-2$ on several crossed pairs, and so on).
The six indices run independently over a 4-point discrete set, so the identity is a finite family of integer equations. Chunk modules discharge named tuples; an assemble theorem glues them into the universal statement.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete indices $(0,2,2,0,1,3)$—the fold that defines $m_2^{\mathrm{num}}$ and the matching clause (or default) of $Z_{\mathrm{ex}}$—and checks integer equality in the kernel. No lemmas are invoked beyond the two upstream definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ and proves it by nested fin_cases on all six $\mathrm{Fin},4$ arguments. Each surviving goal is one of these chunk equalities; this declaration closes the slot $(0,2,2,0,1,3)$.
In the Recognition gravity stack, that universal numerator identity is the algebraic certificate that the midpoint-evaluated M2TT kernel matches eight times the explicit $Z$ table, a finite check supporting the exact Regge analysis rather than a continuum limit argument. It does not itself touch T0–T8 or the RCL; it is infrastructure under the discrete gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.