e_210200
plain-language theorem explainer
At multi-index (2,1,0,2,0,0) the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble into the global identity. The proof is a single kernel decide on fixed Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,2,0,0)$ with each entry in $\{0,1,2,3\}$, the folded 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 9 of a 256-point kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times an explicit integer table on $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at the six indices, and the fold starts from 0. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$, and so on).
The local claim is the single lattice point $(2,1,0,2,0,0)$. Sibling chunks cover the other points; the assemble theorem quantifies over all six indices by fin_cases.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals, so the kernel reduces the equality to true without further lemmas. No algebraic rewriting is required beyond evaluation of m2Num (the fold of contrib) and of the matching explicitZ clause.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal goal by exhaustive fin_cases on each coordinate, invoking one chunk fact per point.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge analysis in 4D: it certifies that the folded coupling numerator is a pure multiple of the explicit Z table, so later curvature or mass-squared identities can quote the closed form rather than the fold. It is pure discrete kernel work, not a continuum GR theorem, and sits downstream of the kernel certificate definitions rather than of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.