e_312220
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (3,1,2,2,2,0) equals eight times the explicit integer table at that same point. Gravity analysts cite it as one cell of the 4D kernel certification that m2Num = 8·explicitZ everywhere. The proof is a single decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,2,2,2,0)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(3,1,2,2,2,0)=8\,Z_{\mathrm{expl}}(3,1,2,2,2,0)$.
background
This module is chunk 13 of a 256-cell kernel certification that the folded numerator of the 4D Regge exact-midpoint mass-squared identity agrees with an explicit integer table, up to the universal factor 8.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling entry at the six $\mathrm{Fin},4$ indices. The comparison target $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).
The local claim is one concrete sextuple in that table, not the universal statement. Upstream definitions live in the kernel-cert module that supplies both $m_2^{\mathrm{num}}$ and $Z_{\mathrm{expl}}$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are fixed, so the kernel decision procedure discharges equality with no algebraic rewriting and no named lemmas beyond the two definitions being compared.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six coordinates. Each chunk theorem such as this one closes one cell of that case tree.
In the Recognition gravity stack this is bookkeeping infrastructure for the Regge exact-midpoint 4D identity: once every cell matches, the folded numerator may be replaced by the closed table times eight, simplifying later curvature and mass-squared arguments. It does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder; it is pure discrete kernel arithmetic supporting those later gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.