e_322013
plain-language theorem explainer
For the six-index slot (3,2,2,0,1,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel decides. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=2$, $c=2$, $d=0$, $i=1$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-case kernel certification that the Regge exact-midpoint $M_2$ TT numerator equals eight times a closed-form integer table on six $\mathrm{Fin},4$ indices.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling term at the six indices. The table $Z$ is an explicit case-split map $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local goal is purely arithmetic: for each concrete six-tuple, check $m_2^{\mathrm{num}}=8Z$ by evaluation, then reassemble the universal statement by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals: the left side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right side multiplies the matching clause of the explicit $Z$ table by eight. No lemmas beyond kernel evaluation are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4$, $m_2^{\mathrm{num}}=8Z$ by six nested fin_cases over the 256 slots. Each chunk theorem such as this one discharges one concrete cell so the universal identity is a pure case split with no analytic remainder.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint $M_2$ TT kernel certificate: once numerator and table match everywhere, downstream Regge/TT comparisons can quote a single closed factor of eight rather than a folded sum. It is bookkeeping inside the 4D kernel, not a new physical law, but it is load-bearing for any claim that the midpoint discretization identity holds exactly on the discrete index set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.