e_023020
plain-language theorem explainer
For the six-index tuple $(0,2,3,0,2,0)$ on $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when discharging one cell of the $4^6$ case split that proves the global midpoint $M_2$ identity. The proof is a single `decide` on concrete integer arithmetic.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the fold of coupling contributions over the fixed coupling list and $Z$ for the explicit integer kernel on the same six indices, one has $N(0,2,3,0,2,0)=8\,Z(0,2,3,0,2,0)$.
background
This module is chunk 2 of a kernel certification that the four-dimensional Regge midpoint numerator $N$ coincides with eight times an explicit integer table $Z$. Both $N$ and $Z$ are functions of six indices in $\mathrm{Fin},4$.
Upstream, $N$ (written m2Num) is defined by folding a contribution map over a fixed coupling list, starting from $0$. The table $Z$ (written explicitZ) is a pattern-matched integer function on the same six indices; sample clauses send $(0,0,1,1,2,2)$ to $4$ and $(0,0,1,2,1,2)$ to $-2$.
The local goal is purely computational: evaluate both sides on one concrete multi-index and check equality in $\mathbb{Z}$.
proof idea
One-line proof by decide. Lean reduces both the fold that defines the numerator and the pattern match that defines the explicit kernel at the concrete indices $(0,2,3,0,2,0)$, then closes the resulting integer equality by the kernel decision procedure. No lemmas are invoked beyond the two definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $N=8Z$ for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof is a complete fin_cases split; each leaf is one of these chunk equalities. This declaration discharges the leaf $(0,2,3,0,2,0)$ inside chunk 2 of that $256$-decide partition.
In the broader gravity stack the identity is the algebraic core of the exact midpoint $M_2$ TT certificate for four-dimensional Regge calculus. It does not itself invoke Recognition landmarks (T5--T8, RCL, $\varphi$), but it is infrastructure those continuum limits rely on once the discrete kernel is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.