e_312013
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at Fin-4 indices (3,1,2,0,1,3) equals eight times the closed-form integer table entry. Gravity analysts cite it as one cell of the 4D Regge midpoint M2–TT kernel certification. The proof is a single kernel decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,2,0,1,3)$ with each index in $\mathbb{F}_4$, the summed coupling numerator equals eight times the explicit integer table value: $N(3,1,2,0,1,3)=8\,Z(3,1,2,0,1,3)$.
background
In the 4D Regge exact-midpoint analysis, the M2–TT identity is certified by matching a folded numerator against a closed-form integer table. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six Fin-4 indices. The table $Z$ is an explicit pattern-matched map $\mathbb{F}_4^6\to\mathbb{Z}$ (sample values include $4$, $-2$, and so on on the diagonal and off-diagonal patterns).
This module is chunk 13 of the 256-point kernel: each chunk discharges one concrete sextuple of the claimed relation $N=8Z$. The local setting is pure integer arithmetic on Fin 4, with no continuum limit or curvature hypotheses in scope.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contributions at the fixed indices $(3,1,2,0,1,3)$, the right-hand side by looking up explicitZ at those same indices and multiplying by 8. The kernel checks integer equality; no lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4,, N=8Z$ by exhausting all Fin-4 cases. That global identity is the algebraic core of the 4D Regge midpoint M2–TT kernel certificate in the Gravity analysis stack. Within Recognition Science it supports the discrete geometric side of the gravity sector (Regge-type edge and deficit bookkeeping), downstream of the forcing chain's $D=3$ spatial claim and the eight-tick octave structure, by locking a finite combinatorial identity rather than a continuum Einstein equation. No open scaffold remains on this cell: it is a closed decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.