e_133333
plain-language theorem explainer
At multi-index (1,3,3,3,3,3) the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it when assembling the pointwise M2 numerator identity over all Fin-4 sextuples. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,\,b{=}c{=}d{=}i{=}j{=}3$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, the M2 TT identity is checked by comparing two integer-valued kernels on six indices each ranging over $\mathbb{F}_4$. The folded numerator sums contribution terms over a fixed coupling list; the explicit table is a sparse case-split returning small integers (typically $\pm 2,,4$, or $0$).
This module is chunk 7 of that kernel certification: it discharges one concrete sextuple among the $4^6=4096$ points, grouped so each chunk is a batch of decide lemmas. Upstream, the two sides are the fold definition of the numerator and the pattern-matched explicit table.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,3,3,3,3,3)$ and checks integer equality. No algebraic rewriting; the kernel certifies the concrete arithmetic directly.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathbb{F}_4)^6$ by exhaustive fin_cases and invokes each chunk lemma at the matching point. That global equality is the numerator half of the Regge exact-midpoint M2 TT identity in 4D gravity analysis. Landmark link is structural (discrete curvature / TT sector bookkeeping), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.