e_220002
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at multi-index (2,2,0,0,0,2) equals eight times the explicit integer table at that same index. Gravity analysts cite it as one cell of the 256-case kernel that certifies m2Num = 8·explicitZ on all of (Fin 4)^6. The proof is a single decidability check on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,2,0,0,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(2,2,0,0,0,2)=8\,Z(2,2,0,0,0,2)$.
background
This module is chunk 10 of a 256-cell kernel certifying that the Regge exact-midpoint numerator equals eight times an explicit integer table on every 6-tuple of indices in $\mathrm{Fin},4$. The local setting is pure finite enumeration: no continuum limit, no continuum curvature identities.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing per-term contributions at the six indices. The table $Z=\mathrm{explicitZ}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and zero off the matched patterns).
The global target is the universal statement $\forall a,b,c,d,i,j,, N=8Z$, proved by exhausting all $4^6$ cells. Each chunk theorem such as this one discharges one concrete cell.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the pattern match of the explicit table; Lean’s decidable equality on Int closes the goal with no lemmas and no rewriting.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which introduces six free $\mathrm{Fin},4$ variables and runs nested fin_cases over the full $4^6$ grid, invoking one cell identity per case. Without the cell theorems the assembler has nothing to apply.
In the gravity analysis stack this identity is bookkeeping infrastructure for the Regge exact-midpoint $M_2$ TT kernel in 4D: it converts a summed coupling expression into a sparse explicit integer table, which is the form needed for later exact algebraic identities. It does not itself touch the Recognition forcing chain (T5–T8), $\phi$, or the eight-tick octave; it is a finite combinatorial certificate inside the gravity side-analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.