e_312113
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (3,1,2,1,1,3) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts cite it as one of 256 finite checks that assemble into the global m2Num = 8·explicitZ theorem. The proof is a pure decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,1,1,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 kernel on six $\mathbb{F}_4$ arguments.
background
This module is chunk 13 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the full $(\mathbb{F}_4)^6$ index space for the 4D Regge exact-midpoint mass-squared identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at those six indices. The comparison object $Z$ is an explicit integer-valued kernel on six $\mathbb{F}_4$ arguments, given by a finite pattern match (sample values include $4$, $-2$, and other small integers on the listed patterns).
The ambient setting is discrete Regge-calculus bookkeeping in four dimensions: every index runs in $\mathrm{Fin},4$, so the identity is a finite table of integer equalities rather than an analytic continuum statement.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed to $3,1,2,1,1,3$, so the kernel decision procedure closes the equality with no lemmas and no case split inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices, dispatching each cell to a chunk equality of this form. Without the full 256-cell cover, the global numerator–kernel identity does not close.
In the gravity analysis stack this identity is bookkeeping infrastructure for the exact midpoint Regge $M^2$ / TT sector in 4D: it certifies that the folded coupling numerator is exactly eight copies of the explicit $Z$ table, so later curvature or mass-squared arguments can quote the closed form rather than the fold. It is not itself a continuum GR claim; it is a finite algebraic certificate inside that pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.