e_201330
plain-language theorem explainer
Pointwise check that the midpoint Regge mass-squared numerator equals eight times the explicit integer kernel Z at the Fin-4 sextuple (2,0,1,3,3,0). Gravity analysts assembling the 4D Regge midpoint M2TT identity cite it as one of 256 kernel cells. The proof is a pure decide on concrete integers from the folded coupling list.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,3,3,0)$ with each coordinate 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 value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-cell kernel certification that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer table on every sextuple of indices in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add, for each coupling term $t$, the integer contribution of $t$ at $(a,b,c,d,i,j)$. The comparison table $Z$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ whose nonzero values are small integers such as $\pm 2,,4$ on selected index patterns.
The local goal is only the single cell $(2,0,1,3,3,0)$; the universal statement is assembled downstream by exhausting all $4^6$ cells.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple. The left side runs the fold that defines the numerator; the right side multiplies the looked-up explicit $Z$ entry by $8$. Equality of the resulting integers is discharged by the kernel decision procedure, with no algebraic rewriting.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, each leaf a chunk theorem of this form. That universal identity is the certified algebraic core of the 4D Regge exact-midpoint M2TT analysis in the Gravity domain. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel bookkeeping supporting the continuum gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.