e_102013
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (1,0,2,0,1,3) equals eight times the explicit Z kernel value there. Gravity analysts cite it when assembling the full Fin 4^6 identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,2,0,1,3)$ in $\{0,1,2,3\}^6$, the integer $m_2$ numerator equals eight times the explicit $Z$-kernel entry: $m_2(1,0,2,0,1,3)=8\,Z(1,0,2,0,1,3)$.
background
This module is chunk 4 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times a closed-form integer kernel $Z$ on all six-tuples of $\mathrm{Fin},4$.
The numerator $m_2(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local weight, and the fold starts at $0$. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on).
The local setting is pure discrete 4D gravity bookkeeping: no continuum limit is taken here; only exact integer equality of two kernel presentations.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are fixed to $1,0,2,0,1,3$, so the kernel reduces the equality to a decidable proposition on $\mathbb{Z}$ and discharges it.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2=8,Z$ by exhausting all six indices. That universal identity is the algebraic core of the Regge exact midpoint $M_2$ TT identity certification in 4D.
Within Recognition Science gravity analysis, matching the folded coupling numerator to an explicit sparse $Z$ table is the step that makes the midpoint discrete curvature kernel inspectable and reusable downstream. This declaration is one of the 256 pointwise bricks; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but it stabilizes the discrete gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.