e_020002
plain-language theorem explainer
For the six-index slot (0,2,0,0,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic decide-cell in the 4D Regge midpoint M2 identity. 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,0,0,0,2)$ equals $8$ times the explicit integer kernel at the same indices: $N(0,2,0,0,0,2)=8\,Z(0,2,0,0,0,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 identity certification: the claim that the folded numerator m2Num equals eight times a sparse explicit integer table explicitZ on every 6-tuple of Fin-4 indices (256 cells, decided in batches).
m2Num a b c d i j is defined by folding a fixed coupling list, accumulating integer contributions at those six indices. explicitZ is the matching closed-form lookup: a pattern-matched Int table (e.g. $4$, $-2$, and zeros off the listed patterns) used as the target right-hand side.
The local setting is pure finite enumeration over $\mathrm{Fin},4^6$, not continuum GR. Chunk 2 holds the cells whose leading index pattern matches this batch; the present declaration is the single cell with indices $(0,2,0,0,0,2)$.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of couplingZList contributions at $(0,2,0,0,0,2)$, the right by multiplying the explicitZ table entry by $8$. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m2Num=8\cdot explicitZ$ by exhaustive fin_cases on all six Fin-4 arguments and discharge of each cell. Without these chunk equalities the global M2 numerator identity does not close.
In the Recognition gravity stack this is bookkeeping for the discrete Regge/midpoint curvature kernel in 4D (spatial $D=3$ plus time in the continuum limit story), not a new dynamical law. It locks the algebraic identity between the folded coupling sum and the sparse explicit $Z$ table so later mass/gravity derivations can quote a single forall rather than 256 raw decides.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.