e_310101
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (3,1,0,1,0,1) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts cite it as one of 256 kernel cells in the m2Num = 8·Z certification. The proof is a single decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,1,0,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the midpoint Regge mass-squared numerator equals eight times an explicit integer table. Indices run over $\mathbb{F}_4$ (Lean Fin 4), six of them at a time.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a contribution for each coupling triple at the given multi-index. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on).
The local claim is only the single cell $(3,1,0,1,0,1)$. Sibling theorems cover the other cells in the chunk; the assembly theorem quantifies over all of $\mathbb{F}_4^6$.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the kernel decision procedure closes the equality with no lemmas and no case splits in this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over the six indices and discharge of each cell. That global identity is the algebraic backbone of the 4D midpoint Regge $M^2$ TT-channel certification in the Gravity analysis stack.
Within Recognition Science gravity work, the factor-of-eight match between the folded coupling numerator and the explicit $Z$ table is the concrete computational certificate that the discrete curvature kernel is under control before continuum or phenomenological claims are attached. This cell is one obligatory brick in that 256-decide wall; it does not itself touch T0–T8 or the RCL, but it locks a numerator identity those later gravity layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.