e_312012
plain-language theorem explainer
Case check that the Regge midpoint mass-squared numerator at multi-index (3,1,2,0,1,2) equals eight times the explicit integer kernel Z there. Gravity analysts cite it as one cell of the 256-way kernel table. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,0,1,2)$ in $(\mathrm{Fin}\,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 $m_2$ numerator equals eight times an explicit integer table $Z$ on $(\mathrm{Fin},4)^6$. The ambient setting is 4D discrete gravity analysis: couplings are summed over a fixed list, and the resulting numerator is compared pointwise to a closed-form kernel.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding couplingZList and accumulating a contribution at each multi-index. The explicit kernel $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer values (e.g. $4$, $-2$, and related entries on diagonal and off-diagonal slots). Both live in the kernel-cert module imported here.
The local claim is only the single cell $(3,1,2,0,1,2)$; sibling theorems cover the other cells in the same chunk.
proof idea
One-line computational proof: decide. After the six Fin-4 indices are substituted, both sides reduce to concrete integers (the fold for the numerator versus the matched clause of the explicit kernel, scaled by 8), and the kernel decision procedure discharges equality.
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$ and proves it by exhaustive fin_cases on all six indices. Each cell theorem such as this one closes one branch of that case split.
In the Recognition gravity stack, the identity is bookkeeping for the exact midpoint Regge mass-squared kernel in 4D: once every cell matches, the folded coupling definition may be replaced by the closed $8Z$ table in downstream curvature and continuum-limit arguments. It does not itself invoke the T0–T8 forcing chain; it is discrete-geometry infrastructure those continuum claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.