e_013301
plain-language theorem explainer
For the six-index slot (0,1,3,3,0,1) 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 4D midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,1,3,3,0,1)=8\,Z_{\mathrm{ex}}(0,1,3,3,0,1)$, 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 is chunk 1 of an exhaustive verification that the 4D Regge midpoint numerator equals eight times a closed-form integer kernel on every six-tuple of $\mathrm{Fin},4$ indices. The ambient setting is discrete gravity analysis: matching a summed coupling expression against an explicit sparse table.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding contrib over couplingZList from zero. The comparison target $Z_{\mathrm{ex}}$ is a pattern-matched integer table on six $\mathrm{Fin},4$ arguments (nonzero only on a sparse set of index patterns, with values such as $4$ and $-2$).
The full identity is $\forall$ six indices, $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$. Because the domain is finite and tiny ($4^6=4096$ points, handled in chunks of kernel decides), each concrete slot is discharged separately.
proof idea
One-line proof: decide. Both sides reduce to concrete integers once the six indices are literals. Lean’s kernel decision procedure evaluates the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z_{\mathrm{ex}}$, then checks integer equality. No lemmas are invoked beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple via nested fin_cases and needs each concrete slot proved. This declaration is the (0,1,3,3,0,1) atom in chunk 1 of that assembly.
In the Recognition gravity stack, the identity certifies that the midpoint Regge M2 numerator collapses to an explicit sparse kernel, clearing a computational bottleneck before continuum or continuum-limit arguments. It is bookkeeping, not a new physical law: it locks the discrete algebraic identity that later geometric claims rely on.
No forcing-chain landmark (T5–T8, RCL, $\varphi$) is directly at stake; the result is infrastructure inside the 4D Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.