e_301021
plain-language theorem explainer
For the six-index combination (3,0,1,0,2,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}0$, $c{=}1$, $d{=}0$, $i{=}2$, $j{=}1$ in $\mathrm{Fin}\,4$, the midpoint 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
In the Regge exact-midpoint 4D analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a coupling list: start at $0$ and add a contribution for each coupling term at the six Fin-4 indices. The companion map $Z$ is an explicit integer-valued kernel on the same six indices, given by a finite pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
This module is chunk 12 of the 256 kernel decides that check $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is pure integer arithmetic on a finite index set; no continuum limit or continuum curvature identity is invoked here.
proof idea
One-line kernel decide: both sides reduce to concrete Int values once the six Fin-4 arguments are fixed, so decide closes the equality. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$ are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:, m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over all six indices. Each chunk such as this one discharges one concrete cell so the global identity is a pure case split rather than a symbolic rewrite. In the Recognition gravity stack this identity is the algebraic certificate that the midpoint Regge $m_2$ numerator matches the closed-form eightfold kernel used downstream in 4D TT-sector checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.