e_200002
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (2,0,0,0,0,2) equals eight times the explicit integer Z-kernel there. Gravity analysts cite it as one atomic case in the 4D TT midpoint certification. Closed by a single kernel decide on both integer sides.
Claim. At multi-index $(2,0,0,0,0,2)\in(\mathrm{Fin}\,4)^6$, the midpoint Regge mass-squared numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,0,0,0,0,2)=8\,Z(2,0,0,0,0,2)$.
background
In the 4D Regge midpoint TT analysis, two integer-valued kernels on six indices in $\mathrm{Fin},4$ are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling-contribution list: sum every local contrib at $(a,b,c,d,i,j)$. The comparison target $Z$ is an explicit piecewise map $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses send matched pairs such as $(0,0,1,1,2,2)$ to $4$ and crossed pairs such as $(0,0,1,2,1,2)$ to $-2$).
This module is chunk 8 of the kernel-decide battery whose global claim is $m_2^{\mathrm{num}}=8,Z$ at every multi-index. The present declaration fixes one concrete six-tuple, $(2,0,0,0,0,2)$.
proof idea
One-line computational close: decide evaluates both the folded numerator and the explicit $Z$ clause at $(2,0,0,0,0,2)$ and checks the integer equality $m_2^{\mathrm{num}}=8Z$. No lemmas are invoked beyond the definitions of the two kernels.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ by exhausting all six $\mathrm{Fin},4$ coordinates. That universal identity is the algebraic core of the exact midpoint $M_2$ TT certification in 4D Regge gravity inside the monolith. Each chunk decide (including this one) is a pure certificate cell: no analytic gap, only finite integer arithmetic. It does not itself touch the T0–T8 forcing chain; it sits downstream in the gravity-analysis layer that consumes the forced $D=3$ spatial setting and the discrete octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.