e_011302
plain-language theorem explainer
Pointwise identity: the midpoint Regge m2-numerator at index sextuple (0,1,1,3,0,2) equals eight times the explicit Z-table entry at those indices. Gravity analysts cite it as one kernel cell in the 4D TT midpoint certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,3,0,2)$ 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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel that certifies $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices arising in the 4D Regge midpoint TT analysis.
The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer weight at $(a,b,c,d,i,j)$, and the fold sums them. The companion table $Z$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single cell $(0,1,1,3,0,2)$. Sibling theorems cover the other cells in the same chunk.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple and checks integer equality. No lemmas are invoked beyond the definitions of the fold-numerator and the explicit Z table; the kernel reduces the closed numeric goal.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each case lands on a chunk cell such as this one.
In the broader gravity stack this identity is bookkeeping for the 4D Regge midpoint TT kernel: once every cell matches, the numerator is interchangeable with the closed-form table, simplifying later curvature and mass-gap arguments. It is pure discrete algebra, not a continuum GR claim, and does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.