e_232132
plain-language theorem explainer
For the six-index tuple (2,3,2,1,3,2) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the coupling-fold numerator at $(a,b,c,d,i,j)=(2,3,2,1,3,2)$ equals $8$ times the explicit integer kernel value at those same indices.
background
This module is one chunk of the 4D Regge exact-midpoint M2–TT identity certification: the claim that the folded numerator m2Num equals eight times a closed-form integer table explicitZ on every six-tuple of Fin-4 indices (256 cases, split across chunk files).
m2Num a b c d i j is defined by folding a fixed coupling list, accumulating integer contributions at those indices. explicitZ is the matching sparse integer table (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns).
The local setting is pure finite enumeration over Fin 4; no continuum limit or physical units enter these lemmas.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete Fin-4 sextuple $(2,3,2,1,3,2)$ to integers and checks equality in the kernel. No algebraic lemmas are invoked beyond the definitions of the fold and the table.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states the identity for all Fin-4 indices and discharges the goal by nested fin_cases, each leaf a chunk theorem of this form. This file is chunk 11 of that 256-case cover.
In the gravity stack these identities underwrite the exact midpoint M2–TT algebraic certificate used in the discrete Regge analysis. They do not themselves invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; they are arithmetic scaffolding for the 4D kernel identity that those continuum arguments later quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.