e_013221
plain-language theorem explainer
Pointwise identity: the midpoint Regge mass-squared numerator at multi-index (0,1,3,2,2,1) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ certificate over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,2,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint mass-squared TT identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ on a block of kernel points by pure decision.
Upstream, $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: it sums integer contributions over that list at a six-index in $(\mathrm{Fin},4)^6$. The companion table $Z$ is an explicit case-split function on the same six indices, returning small integers (e.g. $4$, $-2$) on the supported patterns and serving as the closed-form target.
The present declaration fixes one concrete multi-index $(0,1,3,2,2,1)$ inside that kernel and asserts the numerical equality at that point.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple. The left side reduces by unfolding the fold that defines the numerator; the right side multiplies the table lookup by eight. Both sides are closed integers, so the kernel decides equality with no further lemmas.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal quantifier by exhaustive fin_cases over $(\mathrm{Fin},4)^6$. Each chunk theorem such as this one closes one kernel cell in that case tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared TT sector in 4D: it replaces a folded coupling sum by an eightfold multiple of a sparse explicit table, so later curvature and continuum-limit arguments can quote a closed integer form rather than a list fold. It does not itself invoke the T0–T8 forcing chain; it is pure discrete tensor algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.