e_021001
plain-language theorem explainer
For the six-index tuple (0,2,1,0,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}0$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a sparse explicit integer table $Z$ on $(\mathrm{Fin},4)^6$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those indices. The companion $Z$ is a pattern-matched integer table (nonzero only on a short list of index patterns such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal slots).
The local goal is exhaustive equality $m_2^{\mathrm{num}}=8Z$ cell by cell, so a later assemble theorem can reassemble the universal statement by fin_cases on all six indices.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed six-tuple $(0,2,1,0,0,1)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via $8$ times the pattern match in $Z$. No lemmas beyond kernel evaluation are invoked.
why it matters
Feeds the parent assemble theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by casing through every Fin-4 sextuple and discharging each cell with a chunk equality of this form.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint M2/TT kernel in 4D Regge calculus: once the numerator is certified equal to eight times the sparse table, higher curvature and continuum-limit arguments can quote a closed form instead of a fold. It is pure discrete linear algebra on the coupling list, not a continuum GR claim, and sits downstream of the kernel certificate module rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.