e_022122
plain-language theorem explainer
For the six-index slot (0,2,2,1,2,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2–TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,2,2,1,2,2)$ equals eight times the explicit integer kernel at the same indices: $N(0,2,2,1,2,2)=8\,Z(0,2,2,1,2,2)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels $0,1,2,3$.
The numerator $N=m2Num$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling triple at the six indices. The table $Z=explicitZ$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments; only a handful of ordered sextuples are nonzero (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
The local goal is pointwise equality $N=8Z$ on every sextuple, proved by exhaustive decide rather than by a symbolic identity over the fold.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side evaluates the fold of couplingZList at the fixed indices $(0,2,2,1,2,2)$, the right-hand side multiplies the pattern-matched explicitZ entry by eight. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by nested fin_cases over all $4^6$ slots. Each chunk theorem such as this one discharges one concrete case so the global identity is a pure case split rather than a sorry-laden stub.
In the gravity analysis stack this identity is the algebraic core of the exact midpoint M2–TT relation in 4D Regge calculus: once the numerator is replaced by $8Z$, subsequent curvature and deficit identities can quote a closed integer kernel instead of an opaque fold. It is bookkeeping inside the Recognition gravity layer, not a forcing-chain (T0–T8) step, but it hardens the discrete geometric side that later couples to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.