e_113301
plain-language theorem explainer
Pointwise identity: the folded mass-squared numerator at multi-index (1,1,3,3,0,1) equals eight times the explicit integer Z-table entry there. Gravity analysts assembling the 4D Regge midpoint M2–TT kernel cite it as one of 256 kernel decides. Proof is a pure computational `decide` on concrete Fin-4 indices.
Claim. For indices $a=b=1$, $c=d=3$, $i=0$, $j=1$ in $\mathbb{F}_4$, 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 5 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge exact-midpoint kernel. Indices run over $\mathrm{Fin},4$ (four discrete directions).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The explicit table $Z$ is a closed-form integer pattern on those same six indices (typical nonzero values $4$, $-2$, and symmetric permutations).
The local goal is only the single sextuple $(1,1,3,3,0,1)$. Sibling chunks cover the other $255$ points; the assembly theorem then quantifies over all indices.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted into the fold definition of the numerator and the pattern-match definition of the explicit table, so the equality is a decidable Int fact with no lemmas required.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six indices and discharge of each leaf by a chunk such as this one.
In the gravity analysis stack this identity certifies that the discrete midpoint mass-squared numerator matches the closed Z-kernel used in the 4D Regge–TT sector. It is pure linear-algebra bookkeeping on the coupling list, not a dynamical claim about curvature or matter; it closes one leaf of the kernel certificate that upstream continuum or continuum-limit arguments may assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.