e_313221
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (3,1,3,2,2,1) equals eight times the explicit integer table entry. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. Proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,3,2,2,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the closed-form table: $m_2^{\mathrm{num}}(3,1,3,2,2,1)=8\,Z_{\mathrm{expl}}(3,1,3,2,2,1)$.
background
This module is chunk 13 of a 256-cell kernel certifying that the folded numerator of a 4D Regge midpoint mass-squared identity agrees with an explicit integer table, scaled by eight. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$.
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 given six indices. The table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local claim is the single cell at $(3,1,3,2,2,1)$. Sibling theorems cover the other cells in the same chunk; the assembly theorem quantifies over all six indices.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed, so the kernel equality checker discharges $m_2^{\mathrm{num}}(3,1,3,2,2,1)=8\cdot Z_{\mathrm{expl}}(3,1,3,2,2,1)$ with no manual algebra. No upstream lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on the six indices. Each cell such as this one is a leaf of that case split.
In the gravity analysis stack, the identity replaces a folded coupling sum by a closed integer table, simplifying midpoint Regge mass-squared bookkeeping in 4D. It is infrastructure rather than a forcing-chain landmark (not T5–T8, RCL, or the phi ladder); its role is to make the numerator side of the Regge identity fully explicit and machine-checked.
Open surface: only the global assembly and downstream Regge identities depend on the full 256-cell cover; a single missing or wrong cell would break the universal statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.