e_021031
plain-language theorem explainer
For the six-index tuple (0,2,1,0,3,1) on Fin 4, the folded Regge numerator m₂ equals eight times the explicit kernel value Z. Gravity analysts cite it as one cell of the 4D midpoint M₂–TT identity. The proof is a single kernel decide on the integer equality.
Claim. With indices $(a,b,c,d,i,j)=(0,2,1,0,3,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the certified 4D Regge midpoint identity that equates the folded numerator $m_2$ to eight times an explicit sparse kernel $Z$. The local setting is pure integer arithmetic on six $\mathrm{Fin},4$ indices: no continuum limit is taken here.
Upstream, $m_2$ is defined by folding a fixed coupling list and summing a contribution functional at the given indices. The comparison object $Z$ is an explicit case-table $\mathrm{Fin},4^6\to\mathbb{Z}$ with a handful of nonzero entries (e.g. $4$, $-2$) and zero elsewhere. The identity $m_2=8Z$ is the algebraic content being certified cell by cell.
Chunk 2 holds 256 such kernel decides; the present declaration is the cell at multi-index $(0,2,1,0,3,1)$.
proof idea
One-line proof: decide. Both sides are closed integer terms once the six concrete $\mathrm{Fin},4$ values are substituted into the fold definition of $m_2$ and the case table for $Z$, so the kernel reduces the equality to true by computation. No lemmas beyond the definitions of $m_2$ and $Z$ are invoked.
why it matters
The cell feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8Z$ by exhausting all six $\mathrm{Fin},4$ indices. That universal identity is the algebraic core of the Regge exact-midpoint $M_2$–TT certificate in four dimensions: it converts a folded coupling sum into a sparse explicit kernel that later gravity arguments can quote without re-expanding the fold.
In the broader Recognition gravity stack this is bookkeeping, not a new physical law. It closes one computational obligation on the path from discrete Regge data to the continuum TT sector, and it does not itself invoke $\phi$, the eight-tick octave, or the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.