e_211202
plain-language theorem explainer
For the six-index slot (2,1,1,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 global Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,b{=}1,c{=}1,d{=}2,i{=}0,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(2,1,1,2,0,2)=8\,Z(2,1,1,2,0,2)$.
background
This module is chunk 9 of a 256-case kernel certification that the Regge-exact midpoint numerator equals eight times a tabulated integer kernel on all six-tuples in $(\mathrm{Fin},4)^6$.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. The kernel $Z$ is an explicit pattern-matched integer table on the same six indices (typical nonzero entries are $\pm 2$ or $4$).
The local goal is pointwise equality $N=8Z$ at one concrete slot, later assembled into the universal identity over all indices.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at $(2,1,1,2,0,2)$, the right by looking up explicitZ and multiplying by $8$. Lean’s kernel decision procedure checks the integer equality.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over $(\mathrm{Fin},4)^6$. Each chunk theorem such as this one discharges one concrete branch so the global Regge midpoint M2/TT identity in 4D can quote a fully certified numerator–kernel relation rather than an opaque computation.
In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/mass side, not a forcing-chain landmark (T5–T8), but it is required before continuum or phenomenological claims that rely on the exact midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.