e_313311
plain-language theorem explainer
Single multi-index identity: the Regge midpoint mass-squared numerator at (3,1,3,3,1,1) equals eight times the explicit Z-table entry. Gravity analysts cite it only as one cell of the 256-case kernel that assembles the full m2Num = 8·explicitZ theorem. Proof is a pure kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,1,1)$ 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
In the 4D Regge midpoint analysis, two integer kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the given multi-index. The comparison target is an explicit piecewise table $Z$ that returns small integers (typically $\pm 2,\pm 4$, or $0$) on each of the $4^6=4096$ slots, of which only a sparse support is nonzero.
This module is chunk 13 of a 256-way split of the identity $m_2^{\mathrm{num}}=8Z$. Each chunk discharges a block of concrete index tuples by kernel decision, so the assembler can later recombine them under exhaustive fin_cases.
The local claim is only the single tuple $(3,1,3,3,1,1)$; neighboring e_* siblings cover the rest of the chunk.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions once the six indices are literal Fin 4 values, so the equality is a decidable Int fact with no algebraic rewriting or named lemmas beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the parent assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases over Fin 4, invoking one cell theorem per tuple. That global identity is the certified midpoint mass-squared numerator relation used in the 4D Regge gravity analysis stack.
Within Recognition Science gravity work this is pure computational scaffolding: it closes one concrete cell so the analytic claim can be quoted without residual sorry. It does not itself touch the forcing chain (T0–T8), RCL, or the $\phi$-ladder; those enter only upstream of the Regge setup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.