e_012233
plain-language theorem explainer
For the concrete index sextuple (0,1,2,2,3,3) on Fin 4, the folded midpoint m2 numerator equals eight times the explicit integer Z coupling. Gravity analysts cite it as one of 256 kernel cases that assemble the full pointwise identity. The proof is a single kernel decide on the evaluated integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}2$, $d{=}2$, $i{=}3$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded m2 numerator equals eight times the explicit integer coupling $Z$ at those indices: $N_{\mathrm{m2}}(0,1,2,2,3,3)=8\,Z(0,1,2,2,3,3)$.
background
This module is chunk 1 of a 256-case kernel certification that the midpoint Regge m2 numerator equals eight times an explicit integer table on all sextuples in $(\mathrm{Fin},4)^6$. The setting is 4D discrete gravity analysis: index legs run over four values, and both sides of the identity are pure integers.
The numerator $N_{\mathrm{m2}}$ is defined by folding a fixed coupling list and summing a contribution functional at the six indices. The right-hand side is an explicit case table explicitZ on the same six Fin-4 arguments, returning small integers (e.g. $\pm 2$, $4$) on the nonzero patterns. The local claim is only the equality at one fixed sextuple.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values once the six Fin-4 literals are substituted into the fold definition of the numerator and the case table for explicit $Z$; the kernel checks integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases and routes each leaf to a chunk theorem of this form. Without the full set of 256 decides, the assembly cannot close.
In the gravity stack this is bookkeeping infrastructure for the exact midpoint M2/TT identity in 4D Regge analysis, not a forcing-chain landmark (T0–T8). It closes a finite computational gap so later curvature or continuum-limit arguments can treat $N_{\mathrm{m2}}=8Z$ as an unconditional algebraic fact on the discrete index set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.