e_013023
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (0,1,3,0,2,3) equals eight times the explicit Z-table entry at those indices. Gravity analysts cite it as one kernel cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,0,2,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 1 of a 256-cell kernel certification that the 4D Regge-exact midpoint M2 numerator equals eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (four discrete directions).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at the six indices, and the fold accumulates the total. The companion table explicitZ is a pattern-matched function $\mathbb{F}_4^6\to\mathbb{Z}$ listing the expected closed values (e.g. $4$, $-2$, and zeros off the matched patterns).
The local claim is the single cell of that comparison at $(0,1,3,0,2,3)$.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold of contrib versus 8 times the matched explicitZ clause), and the decidable equality on integers closes the goal with no lemmas or case splits.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8,Z$, by exhausting all six indices. That global identity is the algebraic core of the 4D Regge-exact midpoint M2–TT certification in the Gravity analysis stack.
In the Recognition framework this sits inside discrete gravity bookkeeping (Regge-type edge/face couplings on a 4D lattice), not the T0–T8 forcing chain itself. It closes one of the 256 kernel cells so the assembled numerator identity can be cited without residual sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.