e_033121
plain-language theorem explainer
For the six-index slot (0,3,3,1,2,1) on Fin 4, the folded coupling numerator equals eight times the explicit closed-form integer table. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT numerator identity. The proof is a single kernel decide on two concrete Int values.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,3,3,1,2,1)$ equals eight times the explicit integer table entry: $N_{M_2}(0,3,3,1,2,1)=8\,Z_{\mathrm{ex}}(0,3,3,1,2,1)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D Regge midpoint $M_2$–TT numerator equals eight times an explicit integer table on all multi-indices in $(\mathrm{Fin},4)^6$.
The numerator $N_{M_2}$ (Lean m2Num) is the fold of a fixed coupling list: sum the local contribution of each coupling term at the six indices. The table $Z_{\mathrm{ex}}$ (Lean explicitZ) is a pattern-matched integer function on the same six indices, with sparse nonzero values such as $\pm 2,\pm 4$ on selected diagonal and off-diagonal patterns.
The local claim is one concrete cell of that equality. Upstream definitions supply only the fold and the table; no analytic closed form is re-derived here.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,3,3,1,2,1)$: the left via folding the coupling contribution list, the right via the pattern match on explicitZ. The kernel checks integer equality; no lemmas beyond evaluation are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, N_{M_2}=8 Z_{\mathrm{ex}}$ by exhaustive fin_cases on all six Fin 4 arguments, dispatching each cell to a chunk lemma of this form. This cell is one of those 256 decides.
In the gravity analysis stack, the identity certifies that the midpoint Regge $M_2$ numerator matches the explicit kernel table used downstream in 4D TT-sector checks. It is bookkeeping infrastructure for the exact discrete identity, not a continuum GR derivation. Framework landmarks (T0–T8, $\varphi$, eight-tick) are not directly invoked; the result is pure finite combinatorial certification inside the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.