e_012202
plain-language theorem explainer
For the six-index pattern (0,1,2,2,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}2$, $d{=}2$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,1,2,2,0,2)=8\,Z(0,1,2,2,0,2)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator equals eight times a sparse explicit integer table. The ambient setting is exact algebraic identities for discrete gravity (Regge calculus) rather than continuum Einstein equations.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six Fin-4 indices. The comparison table $Z$ is a pattern-matched integer function on the same six indices; only a handful of patterns are nonzero (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
Chunk theorems pin one concrete sextuple at a time so the global identity can be assembled by exhaustive Fin cases without re-running the fold in the parent proof.
proof idea
One-line decide proof. Both sides reduce to concrete integers: the left by evaluating the fold of contributions at $(0,1,2,2,0,2)$, the right by looking up explicitZ at that pattern and multiplying by 8. Lean’s kernel closes the equality by computation; no lemmas are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by six nested Fin cases. Each chunk such as this one discharges one branch so the global midpoint M2TT identity in 4D rests on certified integer arithmetic rather than an opaque closed form.
In the Recognition gravity stack this is bookkeeping infrastructure for discrete curvature identities, not a forcing-chain landmark (T5–T8). It closes a scaffolding obligation: every index pattern must match before the exact midpoint identity is trusted downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.