e_200101
plain-language theorem explainer
For the six Fin-4 indices (2,0,0,1,0,1), the midpoint Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 256-point identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}0$, $c{=}0$, $d{=}1$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each triple contributes an integer term depending on six $\mathrm{Fin},4$ indices, and the fold starts from zero. The companion table $\mathrm{explicitZ}$ is a sparse case-split on those same six indices, returning small integers such as $4$, $-2$, or (by default) $0$.
The local module is chunk 8 of a 256-case kernel certification whose sole claim is $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ at every index tuple. Each chunk file holds a block of pointwise equalities discharged by kernel decision procedures rather than by symbolic algebra on the fold.
proof idea
One-line decide. Both sides evaluate to concrete Int values once the six indices are substituted: the left-hand side runs the fold of contrib over couplingZList, the right-hand side looks up explicitZ 2 0 0 1 0 1 and multiplies by 8. Lean’s decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which universalizes the identity by fin_cases on all six indices and therefore depends on every pointwise chunk theorem of this form. That global equality is the certified bridge between the folded coupling definition of the midpoint $M_2$ numerator and the closed-form kernel table used in the exact Regge midpoint $M_2$–TT identity in 4D. Within Recognition gravity, it is pure computational scaffolding for the discrete curvature side, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.