e_210330
plain-language theorem explainer
For the multi-index sextuple (2,1,0,3,3,0) on Fin 4, the folded coupling numerator m2Num equals eight times the tabulated explicit kernel value. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite this as one atomic case. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=0$, $d=3$, $i=3$, $j=0$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel entry at that sextuple: $N(2,1,0,3,3,0)=8\,Z(2,1,0,3,3,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to check casewise that the folded numerator equals eight times an explicit integer table (chunk 9 among the kernel decides).
The numerator is defined by folding a fixed coupling list: start at 0 and add a contribution for each coupling term at the six Fin-4 indices. The explicit table is a pattern-matched integer function on six Fin-4 arguments (sample values include 4, -2, and so on for distinguished index patterns).
Upstream, both the fold and the table live in the kernel certificate module. Downstream assembly will quantify over all sextuples by fin_cases; each chunk theorem such as this one discharges one concrete point.
proof idea
One-line computational proof: decide. Lean reduces both sides at the concrete indices (2,1,0,3,3,0) to integers (the fold of contributions versus eight times the matched table entry) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Parent theorem is the universal identity: for every sextuple of Fin-4 indices, the folded numerator equals eight times the explicit kernel. That parent is proved by nested fin_cases, so it depends on a grid of pointwise facts; this declaration is the point (2,1,0,3,3,0) in chunk 9.
In the gravity analysis stack, the identity is the algebraic backbone of the Regge exact-midpoint M2 TT certificate in 4D. It converts a summed coupling expression into a closed integer table, which is what later curvature and deficit bookkeeping consume. It does not itself touch the RS forcing chain (T5 J-cost, T8 D=3), but it sits inside the discrete-gravity layer that must match continuum limits once the octave and dimension constraints are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.