e_002201
plain-language theorem explainer
Pointwise check that the folded M2 numerator coupling at multi-index (0,0,2,2,0,1) equals eight times the explicit integer Z-kernel at the same indices. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single native decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,2,2,0,1)$ in $(\mathbb{F}_4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 0 of a 256-cell kernel certification that the folded M2 numerator equals eight times an explicit integer table, written $m_2^{\mathrm{num}}=8\cdot Z$, in the 4D Regge exact-midpoint M2–TT identity analysis.
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 Fin-4 indices. The explicit kernel $Z$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal pairs $\mapsto -2$, and so on).
The local goal is not the universal statement, but one concrete cell of that table: indices $(0,0,2,2,0,1)$. Sibling theorems cover the other cells in the same chunk.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed, so the kernel decision procedure closes the equality with no lemmas and no case split in the source.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by exhaustive fin_cases on $(a,b,c,d,i,j)$ and dispatches each cell to a chunk theorem of this form. Without the pointwise identities, the universal equality $m_2^{\mathrm{num}}=8Z$ does not go through.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge M2–TT kernel in four dimensions (the spatial $D=3$ forcing from T8 sits upstream of the continuum limit, but this declaration itself is pure finite-index algebra). It closes one scaffold cell in the certified numerator table rather than a physical prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.