e_313321
plain-language theorem explainer
For the concrete index sextuple (3,1,3,3,2,1) in (Fin 4)^6, the folded coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one of 256 kernel cases feeding the universal m2Num = 8·explicitZ identity. The proof is a single decide on ground integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}3,\,d{=}3,\,i{=}2,\,j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes via a local kernel, and the accumulator starts at zero. The comparison target is an explicit table $Z$ that returns a small integer (typically $\pm 2$ or $4$) by pattern match on the six indices.
The module is chunk 13 of a 256-case kernel certification: every concrete sextuple is discharged separately so that a later assembly theorem can quantify over all of $(\mathrm{Fin},4)^6$. The ambient claim is the exact midpoint mass-squared identity used in the discrete gravity sector of Recognition Science.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,1,3,3,2,1)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the table entry by eight. Both are closed integers, so the equality is decided by the kernel with no lemmas or case splits inside this declaration.
why it matters
This case is one leaf of the exhaustive fin_cases tree in m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. That universal identity is the algebraic backbone of the Regge exact midpoint $M_2$ TT certification in 4D. Without the chunked decides, the assembly cannot close. In the broader RS gravity stack it supports the discrete curvature bookkeeping that must match continuum limits once the eight-tick and $D=3$ forcing (T7–T8) are in place; it does not itself invoke $\phi$ or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.