e_301231
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at Fin-4 indices (3,0,1,2,3,1) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one cell of the 256-kernel certification that m2Num = 8·explicitZ. Proof is a single decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,0,1,2,3,1)$ with each coordinate in $\mathbb{F}_4$, the summed coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(3,0,1,2,3,1)=8\,Z_{\mathrm{expl}}(3,0,1,2,3,1)$.
background
This module is chunk 12 of a 256-cell kernel certification that the discrete M2 numerator equals eight times a closed-form integer table on all Fin-4 index sextuples. The setting is 4D Regge/midpoint analysis of the TT sector identity for the M2 operator.
The numerator m2Num a b c d i j is defined by folding a fixed coupling list: it accumulates contrib t a b c d i j over every term t in couplingZList, yielding an Int. The comparison table explicitZ is a pattern-matched function Fin 4^6 → Int with sparse nonzero entries (e.g. 4 on diagonal-type pairs, −2 on selected off-diagonal pairs).
The local claim is only the single cell with indices (3,0,1,2,3,1). Sibling theorems cover the other cells in this chunk; the assembly theorem quantifies over all sextuples.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed, so the kernel decision procedure discharges equality with no lemmas, rewrites, or case splits inside this declaration.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num = 8 · explicitZ, proved by exhaustive fin_cases on the six indices. Each chunk cell such as this one is a named witness that the folded coupling sum matches the explicit table at that point.
In the gravity stack this identity is bookkeeping for the exact midpoint M2 TT kernel in 4D: once every cell is certified, the closed form explicitZ may replace the fold in downstream curvature/mass analyses. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete linear-algebra certification inside the Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.