e_301032
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (3,0,1,0,3,2) equals eight times the explicit Z table entry there. Gravity analysts cite it when assembling the full 4D kernel identity m2Num = 8·explicitZ. The proof is a single kernel decide on fixed Fin 4 indices.
Claim. For indices $(a,b,c,d,i,j)=(3,0,1,0,3,2)$ in $(\mathbb{F}_4)^6$, the integer $m_2$-numerator equals eight times the explicit coupling table value: $m_2(3,0,1,0,3,2)=8\,Z(3,0,1,0,3,2)$.
background
This module is chunk 12 of a 256-way split of the 4D midpoint Regge identity $m_2=8Z$. Each chunk discharges a block of fixed multi-indices by kernel decision rather than a symbolic argument.
The numerator $m_2(a,b,c,d,i,j)$ is the fold of coupling contributions over a fixed list: it sums contrib terms for the six Fin-4 indices. The comparison target explicitZ is a sparse integer table on $(\mathbb{F}_4)^6$ (nonzero only on a short list of index patterns, with values such as $\pm 2,\pm 4$).
The local claim is one concrete cell of that table equality. Upstream definitions live in the kernel certificate module; the present file only specializes them at $(3,0,1,0,3,2)$.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms once the six Fin-4 arguments are literals, so the kernel evaluates the fold defining the numerator and the matching clause (or default) of the explicit table and checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2=8Z$ on $(\mathbb{F}_4)^6$ and proves it by exhaustive fin_cases. That global identity is the algebraic core of the 4D midpoint Regge $M_2$/$TT$ certificate in the Gravity analysis stack.
In the Recognition framework this sits on the gravity side of the discrete geometric bookkeeping (Regge-type edge and deficit bookkeeping compatible with the eight-tick / $D=3$ forcing chain), not on the J-uniqueness or $\varphi$-ladder mass steps. It closes one of 256 kernel cells so the assembled equality has no sorry and no residual case split in the parent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.