e_310333
plain-language theorem explainer
For multi-index (3,1,0,3,3,3), the Regge midpoint mass-squared numerator equals eight times the explicit Z-kernel integer. Gravity analysts cite it as one of 256 concrete kernel decides that assemble the global 4D identity. Proof is a single native decide on fixed Fin-4 indices.
Claim. At indices $(a,b,c,d,i,j)=(3,1,0,3,3,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2$ equals $8$ times the explicit integer kernel $Z$ at those indices.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to show the folded numerator equals eight times an explicit kernel table, discharged by 256 kernel decides.
The numerator $m_2(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer contrib and the accumulator starts at 0. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite case table (sample entries include $4$, $-2$, and so on).
Indices live in $\mathrm{Fin},4$, matching the four discrete directions of the 4D midpoint stencil under analysis.
proof idea
One-line computational proof: decide. Both sides are closed integer terms once the six $\mathrm{Fin},4$ arguments are literals, so the kernel reduces the equality to true by evaluation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8,Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one closes one concrete cell of that $4^6$ grid.
In the broader Gravity analysis stack this identity is the algebraic backbone of the Regge exact-midpoint mass-squared TT relation in 4D. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel bookkeeping that later curvature and continuum limits can quote without re-checking the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.