e_202201
plain-language theorem explainer
For the six-index slot (2,0,2,2,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}0$, $c{=}2$, $d{=}2$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $N(2,0,2,2,0,1)=8\,Z(2,0,2,2,0,1)$.
background
In the Regge exact-midpoint 4D analysis, the numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The companion explicitZ is a closed-form integer table on six Fin 4 indices (sample clauses give values such as 4, -2, etc.).
This module is chunk 8 of the 256 kernel decides that certify, pointwise, that the folded numerator is exactly eight times that table. The local setting is pure finite enumeration over Fin 4^6, not continuum gravity.
Upstream, both sides are pure definitions in the kernel certificate module; no analytic hypothesis is carried.
proof idea
One-line kernel decide. Both sides reduce to concrete Int values for the fixed sextuple (2,0,2,2,0,1), so decide discharges the equality by computation. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
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 on all six indices. Each chunk theorem such as this one is a leaf of that case tree.
In the Recognition gravity stack this identity is bookkeeping for the Regge midpoint mass-squared / TT kernel in 4D: it guarantees the folded coupling form matches the explicit integer kernel used downstream. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder; it is a finite combinatorial certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.