e_030211
plain-language theorem explainer
Kernel certificate that the folded M2 numerator at multi-index (0,3,0,2,1,1) equals eight times the explicit integer Z-coupling at those same indices. Gravity analysts assembling the 4D Regge midpoint M2=8Z identity cite this as one of the 256 concrete cases. The proof is a single decidability check on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,2,1,1)$ in $(\mathbb{F}_4)^6$, the folded midpoint $M_2$ numerator equals eight times the explicit integer coupling $Z$ at those indices: $M_2^{\mathrm{num}}(0,3,0,2,1,1)=8\,Z(0,3,0,2,1,1)$.
background
This module is chunk 3 of a 256-case kernel that certifies $m2Num=8\cdot explicitZ$ pointwise on $(\mathbb{F}_4)^6$. The setting is the exact midpoint identity for the 4D Regge $M_2$ tensor in the gravity analysis stack.
The numerator $m2Num(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums contrib terms over couplingZList, yielding an integer. The comparison target explicitZ is a closed pattern-match table $\mathbb{F}_4^6\to\mathbb{Z}$ that records the expected coupling values (e.g. $4$, $-2$, and sparse defaults).
Chunk theorems pin one concrete six-tuple each so the assembly theorem can discharge the universal claim by exhaustive fin_cases without re-running the fold at proof time.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals, so Lean's decidable equality on Int evaluates the fold defining the numerator and the pattern match defining explicit $Z$, then checks $n=8z$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m2Num,a,b,c,d,i,j=8\cdot explicitZ,a,b,c,d,i,j$ and proves it by six nested fin_cases over $\mathbb{F}_4$. Each chunk such as this one supplies one leaf of that case tree.
In the Recognition gravity stack this identity is the algebraic backbone of the exact midpoint $M_2$ TT kernel in 4D Regge calculus: it replaces a summed coupling expansion by a sparse explicit table scaled by eight. Without the pointwise certificates the assembly cannot close, and downstream curvature or continuum-limit comparisons lose their exact integer bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.