e_311332
plain-language theorem explainer
For the six-index tuple (3,1,1,3,3,2) on Fin 4, the folded coupling numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite it as one atomic cell of the 4D Regge midpoint M2–TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(3,1,1,3,3,2)$. The integer obtained by folding the coupling contribution list at these indices equals $8$ times the explicit integer table entry at the same indices.
background
This module is one chunk of the exhaustive verification that the 4D Regge-exact midpoint M2–TT numerator equals eight times a sparse closed-form table. The local slogan is "m2Num = 8·explicitZ, chunk 13 (256 kernel decides)."
The numerator m2Num is defined by folding a fixed coupling list: start from 0 and add each contribution evaluated at the six Fin-4 indices. The table explicitZ is a pattern-matched integer function on the same six indices (typical nonzero values are $\pm 2,\pm 4$, with most tuples implicitly zero).
Both definitions live in the kernel-certificate module imported here. The present lemma fixes one concrete multi-index and asserts the scalar equality at that point.
proof idea
One-line computational proof: by decide. Lean reduces both sides to concrete integers (the fold for the numerator and the match for the table) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple by nested fin_cases and needs one decide cell per tuple. This declaration is the cell for (3,1,1,3,3,2).
In the gravity analysis stack, the identity m2Num = 8·explicitZ is the algebraic backbone of the Regge-exact midpoint M2–TT certificate in 4D. Closing all chunks discharges the numerator side of that certificate; the present fact is pure bookkeeping inside that exhaustion, not a new physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.