e_312132
plain-language theorem explainer
At the six Fin-4 indices (3,1,2,1,3,2), the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one concrete cell of the 256-case kernel identity. The proof is a single decide on fully concrete integers.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=1$, $i=3$, $j=2$ 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
This module is one chunk of the 4D Regge exact-midpoint identity that asserts $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of indices in $\mathrm{Fin},4$. The module doc frames the work as "m2Num = 8·explicitZ, chunk 13 (256 kernel decides)."
Upstream, $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: it sums a contribution function over that list at the six indices. The companion table $Z$ is an explicit piecewise integer function on $(\mathrm{Fin},4)^6$, with sample values such as $4$, $-2$, and so on at listed patterns.
The ambient setting is discrete Regge gravity analysis: these integer identities certify that a midpoint mass-squared numerator factors cleanly through the tabulated $Z$ kernel before continuum or continuum-limit arguments are attached.
proof idea
Both sides are closed integer expressions once the six Fin-4 arguments are fixed. The tactic decide evaluates the fold that defines the numerator and the matching clause of the explicit $Z$ table, then checks equality of the resulting integers. No lemmas beyond the definitions of the numerator and the table are required; the goal is pure ground arithmetic.
why it matters
The parent theorem is the universal statement that $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ for all six indices. That assembly walks every Fin-4 combination; this declaration discharges the single cell $(3,1,2,1,3,2)$ inside chunk 13 of the 256-case kernel.
In the Recognition gravity stack, such kernel identities underwrite exact algebraic control of discrete curvature and mass-squared bookkeeping before continuum constants (including the RS-native $G=\varphi^5/\pi$ band) are read off. The result is pure integer bookkeeping: it does not itself invoke the forcing chain T0–T8, but it is the kind of certified discrete identity those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.