e_021213
plain-language theorem explainer
For the six-index slot (0,2,1,2,1,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}2$, $i{=}1$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,1,2,1,3)=8\,Z(0,2,1,2,1,3)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator matches a closed integer table. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six Fin-4 indices. The table $Z$ is an explicit case-split map $\mathrm{Fin},4^6\to\mathbb{Z}$ listing the target integers (e.g. $\pm 2,,4$ on the diagonal-type slots shown upstream).
The local claim is the single hex-tuple $(0,2,1,2,1,3)$ inside chunk 2. Upstream only supplies the two definitions being compared; no analytic lemma is needed beyond evaluation of those defs at concrete values.
proof idea
One-line decide. Both sides reduce to concrete integers once m2Num unfolds the fold over couplingZList and explicitZ matches its pattern, so the kernel closes the equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases on all six indices. Each chunk lemma such as this one discharges one concrete branch so the global identity is a pure case split rather than an algebraic derivation. In the gravity stack this certifies the exact midpoint M2TT numerator identity used in the 4D Regge analysis; it is bookkeeping infrastructure, not a new physical law, but without the full 256-case cover the assembly theorem does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.