e_020122
plain-language theorem explainer
For the six Fin-4 indices (0,2,0,1,2,2), the midpoint M2 numerator equals eight times the explicit kernel value Z. Gravity analysts cite it when assembling the full 4D Regge midpoint identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}0$, $d{=}1$, $i{=}2$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $N_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the exhaustive check that the 4D Regge midpoint M2 numerator equals eight times an explicit integer kernel on every sextuple of Fin-4 indices. The module header states the goal as $m2Num = 8\cdot explicitZ$, chunk 2, via 256 kernel decides.
The numerator $N_2$ is defined by folding a contribution function over a fixed coupling list: start at 0 and add each term's contribution at the six indices. The explicit kernel $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern match (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The present declaration fixes one concrete sextuple $(0,2,0,1,2,2)$ inside that grid. Sibling theorems cover the other index combinations in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side by evaluating the fold of contributions at the fixed indices, the right-hand side by unfolding the pattern match for $Z$ (or the default branch) and multiplying by 8. No lemmas are invoked beyond decidable equality on $\mathbb{Z}$.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; N_2=8Z$ and discharges the universal claim by fin_cases on all six indices, routing each cell to a chunk theorem of this form.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2/TT kernel in 4D Regge calculus: once every cell matches, the numerator is interchangeable with the closed-form kernel. It does not itself touch the forcing chain (T5–T8), RCL, or the $\phi$-ladder; it is pure discrete-kernel certification supporting the continuum gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.