e_211132
plain-language theorem explainer
Pointwise kernel identity: the folded M2 numerator coupling at multi-index (2,1,1,1,3,2) equals eight times the explicit integer Z-kernel at that same index. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one of 256 concrete cells. The proof is a single native decide on fixed Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,1,1,3,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 kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-cell kernel certification that the Regge-exact midpoint M2 numerator equals eight times a closed-form integer table in four dimensions. Indices run over $\mathrm{Fin},4$, labeling discrete directions in the 4D simplicial setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each list term's contribution at the six indices. The comparison object $Z$ is an explicit case-table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns).
The local claim is only the single cell $(2,1,1,1,3,2)$. Sibling theorems cover the other cells; the assemble layer quantifies over all six indices.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are literal numerals, so the kernel reduces $m_2^{\mathrm{num}}$ via the fold definition and $Z$ via its match table, then checks numeral equality in $\mathbb{Z}$. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the universal assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices (ReggeExactMidpointM2TTIdentity4DM2NumAssemble). That assembly runs nested fin-cases and discharges each cell by a chunk identity of this form; without the cell equalities the midpoint M2–TT 4D kernel certificate does not close.
In the gravity stack this is bookkeeping infrastructure for an exact discrete identity, not a new dynamical law. It sits downstream of the kernel-cert definitions and upstream of the full quantified midpoint identity used in the Regge analysis path. No forcing-chain landmark (T5–T8, RCL, $\varphi$) is decided here; the result is pure integer algebra on the coupling table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.