e_021021
plain-language theorem explainer
For the six-index tuple (0,2,1,0,2,1) on Fin 4, the folded M2 numerator equals eight times the explicit integer kernel Z. Analysts certifying the 4D Regge midpoint M2–TT identity cite this as one concrete case among the 256-kernel split. The proof is a single decide that evaluates both integer expressions.
Claim. At multi-index $(0,2,1,0,2,1)$ with each entry in $\{0,1,2,3\}$, the M2 numerator equals eight times the explicit kernel value: $N_{M_2}(0,2,1,0,2,1)=8\,Z(0,2,1,0,2,1)$.
background
In the 4D Regge midpoint analysis, the M2 numerator on six Fin-4 indices is the integer fold $N_{M_2}(a,b,c,d,i,j)=\sum_t\mathrm{contrib}(t;a,b,c,d,i,j)$ over a fixed coupling list. The companion map $Z$ is an explicit integer kernel on the same indices, given by a finite case table (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
This module is chunk 2 of a 256-way case split whose sole job is to certify $N_{M_2}=8Z$ pointwise. The setting is pure finite-domain integer arithmetic, so each fixed multi-index is decidable by the kernel.
proof idea
One-line kernel proof. decide evaluates the fold that defines the numerator and the pattern-match that defines explicit $Z$ at the concrete indices $(0,2,1,0,2,1)$, then checks the resulting integers for equality. No intermediate lemmas are invoked beyond those two definitions.
why it matters
The parent assembly theorem states $\forall a,b,c,d,i,j,,N_{M_2}(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ and discharges the quantifiers by exhaustive fin_cases on all six Fin-4 arguments. Each residual concrete goal is one of these chunk equalities. Closing $N_{M_2}=8Z$ everywhere is a computational certificate inside the exact midpoint M2–TT identity for 4D Regge gravity. It is bookkeeping, not a new physical law, but without the full case table the midpoint identity does not typecheck in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.