e_123201
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index sextuple (1,2,3,2,0,1) equals eight times the explicit integer table at that point. Gravity analysts cite it as one kernel cell in the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete Int values.
Claim. For indices $(a,b,c,d,i,j)=(1,2,3,2,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table entry: $m_2^{\mathrm{num}}(1,2,3,2,0,1)=8\,Z_{\mathrm{expl}}(1,2,3,2,0,1)$.
background
This module is chunk 6 of a 256-cell kernel certification that the folded numerator of the 4D Regge midpoint M2–TT identity agrees with eight times an explicit integer table on every sextuple of Fin 4 indices.
The numerator m2Num a b c d i j is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib t a b c d i j. The comparison table explicitZ is a total function Fin 4^6 → ℤ given by a finite pattern of integer cases (typical values 4, −2, and the remaining default).
The local claim is one concrete cell of that comparison. Upstream, both sides are pure definitions in the kernel certificate module; no analytic hypotheses are carried.
proof idea
One-line computational proof: by decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are literals, so the kernel decision procedure discharges equality of the two Int values with no lemmas or case splits in this file.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every sextuple by nested fin_cases and invokes the matching chunk cell at each leaf. This declaration is the leaf for (1,2,3,2,0,1) inside chunk 6.
In the Recognition gravity stack, the identity m2Num = 8 · explicitZ is bookkeeping for the exact midpoint evaluation of the 4D Regge M2–TT coupling: the folded sum must match a sparse explicit integer kernel before continuum or continuum-limit arguments. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete linear-algebra certification under the gravity analysis modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.