e_022332
plain-language theorem explainer
For the six-index tuple (0,2,2,3,3,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the full 4D Regge midpoint identity m2Num = 8·explicitZ. The proof is a single kernel decide on the concrete integers.
Claim. For indices $a=0$, $b=2$, $c=2$, $d=3$, $i=3$, $j=2$ in $\mathrm{Fin}\,4$, the midpoint numerator obtained by folding the coupling list equals eight times the explicit integer kernel at those indices: $N(0,2,2,3,3,2)=8\,Z(0,2,2,3,3,2)$.
background
This module is one chunk of a 256-case kernel certification that the Regge midpoint numerator equals eight times an explicit integer table on all six-tuples in $(\mathrm{Fin},4)^6$. The local setting is pure integer arithmetic: no continuum limit, only exact equality of two combinatorial expressions.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing a contribution at each term for the six indices. The table $Z=\mathrm{explicitZ}$ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on for distinguished index patterns).
The identity $N=8Z$ is the algebraic content being certified case-by-case before the universal statement is assembled by exhaustive fin_cases.
proof idea
One-line proof by decide. Both sides reduce to concrete integers for the fixed tuple $(0,2,2,3,3,2)$: the fold that defines the numerator and the pattern match that defines the explicit kernel. Lean’s decision procedure checks the integer equality $N=8Z$ with no further lemmas.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,,N=8Z$ by running fin_cases on all six indices and dispatching each concrete goal to a chunk lemma of this form. Without the per-tuple certificates the universal midpoint identity does not close.
In the Recognition gravity stack this is bookkeeping for the exact 4D Regge midpoint $M_2$ identity: the numerator built from couplings must match the closed kernel used downstream in curvature and mass-gap analyses. It is not itself a forcing-chain step (T0–T8), but it is part of the certified discrete-gravity substrate those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.