e_201203
plain-language theorem explainer
At the concrete 4D index sextuple (2,0,1,2,0,3), the folded Regge midpoint mass-squared numerator equals eight times the explicit integer coupling Z. Gravity analysts cite it as one of 256 kernel cells that assemble the full identity. The proof is a single decide on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,2,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer table of midpoint Regge couplings.
background
This module is chunk 8 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathbb{F}_4)^6$. The setting is 4D Regge calculus at the exact midpoint: discrete curvature couplings are reduced to integer tables rather than symbolic tensors.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer via a local kernel, and the accumulator starts at 0. The comparison target $Z$ is an explicit case table $\mathbb{F}_4^6\to\mathbb{Z}$ (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$). Both live in the kernel-cert module imported here.
The full quantified statement is assembled downstream by exhausting all six Fin-4 indices; each chunk theorem discharges one concrete cell.
proof idea
One-line computational proof: decide evaluates both sides at the fixed sextuple $(2,0,1,2,0,3)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the table lookup $Z(2,0,1,2,0,3)$ by 8. Equality of the resulting integers is decided by the kernel.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by nested fin_cases over all six indices; this declaration is the cell for $(2,0,1,2,0,3)$ in that case tree (chunk 8 of the 256 decides).
In the Recognition gravity stack, the identity converts a folded discrete curvature numerator into a closed integer coupling table, which is the algebraic input for midpoint Regge mass-squared identities in 4D. It does not itself touch the forcing chain (T0–T8) or the RCL; it is infrastructure under the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.