e_310233
plain-language theorem explainer
For multi-index (3,1,0,2,3,3) on Fin 4, the folded Regge midpoint coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one atom of the 256-case kernel identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. At the multi-index $(a,b,c,d,i,j)=(3,1,0,2,3,3)\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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-way split of the 4D Regge midpoint $M_2$ TT-identity kernel. The goal across chunks is the pointwise integer identity $m_2^{\mathrm{num}}=8\cdot Z$ on all six-tuples of indices in $\mathbb{F}_4$.
Here $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums the local contribution of each coupling term at the six indices. The companion table $Z$ is an explicit case-split function $\mathbb{F}_4^6\to\mathbb{Z}$ listing the closed-form integer values (typical entries $\pm 2,\pm 4$, and zeros off the support).
The ambient setting is discrete gravity analysis: verifying that a midpoint-evaluated Regge curvature/mass numerator matches a hand-written sparse integer kernel, so later continuum or continuum-limit arguments can quote a fully certified algebraic identity rather than a symbolic expansion.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six Fin 4 arguments are concrete literals, so the kernel reduces the equality of two Int values by evaluation. No lemmas are invoked beyond the definitions of m2Num (list fold of contributions) and explicitZ (pattern-matched table).
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):\mathbb{F}_4^6$ and discharges the goal by exhaustive fin_cases on the six indices. Each chunk theorem such as this one is a named, machine-checked cell of that $4^6=4096$-branch (effectively 256 nontrivial kernel cells) case tree.
In the Recognition gravity stack this closes the algebraic core of the 4D midpoint Regge $M_2$ TT identity: once numerator and explicit kernel agree everywhere, downstream curvature and mass-ladder arguments can treat the factor-of-eight normalization as proved rather than assumed. It is pure discrete-geometry bookkeeping, not a continuum Einstein-equation derivation, but it is the certificate those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.