e_122121
plain-language theorem explainer
Finite-index certificate that the Regge midpoint mass-squared numerator equals eight times the explicit Z kernel at multi-index (1,2,2,1,2,1). Gravity analysts cite it as one cell of the 4^6 case split that builds the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on an integer equality.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,1,2,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
This module is chunk 6 of a brute-force verification that the 4D Regge midpoint mass-squared numerator matches eight times a closed-form kernel on every multi-index in $(\mathrm{Fin},4)^6$. The ambient setting is discrete gravity analysis: couplings are tabulated, then folded into an integer numerator.
Upstream, m2Num is defined by folding a contribution map over couplingZList, starting from 0, so it is a pure integer sum of tabulated terms at six Fin-4 slots. explicitZ is the matching closed-form table: a pattern-matched function $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$) on selected index patterns and (implicitly) zero elsewhere.
The local claim is one concrete cell of that table equality. Sibling theorems cover the other index tuples in the same chunk; the assembly theorem quantifies over all six indices.
proof idea
One-line computational certificate: decide. Both sides are closed integer terms once the six Fin-4 arguments are concrete literals, so the kernel evaluates m2Num 1 2 2 1 2 1 by running the fold over couplingZList, evaluates explicitZ by pattern match, multiplies by 8, and checks propositional equality of the resulting Int values. No lemmas are invoked beyond the decidability instance for integer equality.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by nested fin_cases on all six indices. Each concrete goal is exactly one chunk theorem of this shape; this declaration closes the cell $(1,2,2,1,2,1)$.
In the Recognition gravity stack, that global identity is the algebraic bridge from the tabulated midpoint Regge coupling data to the explicit kernel used in mass-squared and TT-sector identities. Without the cell-by-cell certificates, the assembly cannot finish. The work is pure finite verification (no continuum limit, no dynamical PDE), but it is load-bearing for any later claim that quotes $m_2^{\mathrm{num}}=8Z$ on Fin-4 indices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.