e_030201
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at multi-index (0,3,0,2,0,1) equals eight times the explicit kernel table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint M₂TT numerator identity over (Fin 4)⁶. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,3,0,2,0,1)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,3,0,2,0,1)=8\,Z_{\mathrm{expl}}(0,3,0,2,0,1)$.
background
This module is chunk 3 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on every 4D multi-index. The ambient setting is exact midpoint analysis for the Regge M₂TT identity in four dimensions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution at those six Fin-4 slots. The comparison table $Z_{\mathrm{expl}}$ is an explicit six-argument integer function on Fin 4, with closed values such as $4$, $-2$, and so on at listed patterns (and implicitly 0 elsewhere in the match).
The claim is one concrete cell of that equality, not the quantified statement.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin-4 indices are fixed at $(0,3,0,2,0,1)$, so the kernel equality checker discharges $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ with no lemmas beyond the definitions of the fold and the explicit table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a named cell in that 4⁴·4² cover.
In the gravity stack this closes the algebraic numerator identity behind the exact midpoint Regge M₂TT analysis in 4D. It is bookkeeping, not a new physical law: once every cell matches, the folded coupling form may be replaced by the closed explicit kernel everywhere downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.