e_312210
plain-language theorem explainer
For the six-index tuple (3,1,2,2,1,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=2$, $i=1$, $j=0$ in $\{0,1,2,3\}$, the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2TT numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator $N$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (sample entries include $4$, $-2$, and so on).
The local claim is the pointwise identity $N=8Z$ at one concrete multi-index. Upstream, both $N$ and $Z$ live in the kernel-cert module; downstream assembly will quantify over all $4^6$ tuples.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,1,2,2,1,0)$ and checks integer equality. No algebraic lemmas are invoked; the kernel reduces the fold that defines the numerator and the match that defines the explicit table to concrete Int values and compares them.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every chunk cell by exhaustive fin_cases on all six indices, obtaining $\forall a,b,c,d,i,j,, N=8Z$. This declaration is one of those cells (chunk 13).
In the Recognition gravity stack the identity is bookkeeping for the exact midpoint form of the 4D Regge M2TT coupling: once numerator and explicit kernel agree up to the universal factor eight, later analytic steps can quote the closed table instead of the fold. It does not itself touch T0–T8 or the J-cost forcing chain; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.