e_022121
plain-language theorem explainer
Pointwise identity for multi-index (0,2,2,1,2,1): the folded Regge coupling numerator equals eight times the explicit integer Z table entry. Gravity analysts cite it when assembling the full 4D midpoint M2 TT kernel identity over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,1,2,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the tabulated explicit integer $Z$ at that multi-index: $N(0,2,2,1,2,1)=8\,Z(0,2,2,1,2,1)$.
background
This module is chunk 2 of a 256-way kernel certification that the 4D Regge midpoint M2 TT numerator matches eight times an explicit integer table. The ambient setting is discrete gravity analysis: curvature and coupling data live on Fin 4 labels (four simplex or edge slots).
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six indices. The comparison table $Z=\mathrm{explicitZ}$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite pattern of integer cases (e.g. $4$, $-2$, and zeros off-pattern).
The local claim is one concrete sextuple in that comparison. Upstream, only the definitions of the fold and the table are required; no analytic lemma beyond decidable integer arithmetic.
proof idea
One-line computational proof: decide. Both sides reduce to closed integer expressions once the six Fin 4 indices are substituted into the fold definition of the numerator and the case table for explicit $Z$. Lean’s kernel decision procedure checks equality of the resulting integers. No rewrite lemmas or induction are invoked.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,, N=8Z$ on $(\mathbb{F}_4)^6$, proved by exhaustive fin_cases. Each chunk theorem such as this one discharges one concrete case in that $4^6=4096$-leaf tree (here organized as 256 kernel decides per chunk family).
In the Recognition gravity stack this closes a certified algebraic identity for the midpoint Regge M2 TT sector in four dimensions, so later curvature or continuum-limit arguments can quote a fully expanded integer kernel rather than an opaque fold. It is bookkeeping inside the Gravity.Analysis layer, not a forcing-chain (T0–T8) step, but it hardens the discrete geometric substrate those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.