e_122202
plain-language theorem explainer
For the index sextuple (1,2,2,2,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise equalities when assembling the global 4D midpoint Regge identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}2,d{=}2,i{=}0,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(1,2,2,2,0,2)=8\,Z(1,2,2,2,0,2)$.
background
This module is chunk 6 of a 256-case kernel certification that the 4D midpoint Regge numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, labeling discrete edge/face slots in the Regge calculus setup.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The comparison table $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and zero off the support).
The local claim is one concrete sextuple in that table: $(1,2,2,2,0,2)$. Sibling chunks cover the remaining points; the assemble theorem recombines them.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of couplingZList contributions at the fixed indices, the right by unfolding the pattern match for explicitZ (or the default zero). Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assemble theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk such as this one discharges one (or a block of) decide obligations so the global identity stays kernel-checkable.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint 4D Regge–TT analysis: it certifies that the discrete numerator matches the closed-form kernel used downstream. It is not itself a forcing-chain step (T0–T8); it is computational support inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.