e_022002
plain-language theorem explainer
For the six-index slot (0,2,2,0,0,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=2$, $c=2$, $d=0$, $i=0$, $j=2$ in $\{0,1,2,3\}$, the midpoint numerator $N_2(a,b,c,d,i,j)$ obtained by folding the coupling list equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis for 4D gravity, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N_2$ (Lean m2Num) is defined by folding a fixed coupling list and summing local contributions at each tuple $(a,b,c,d,i,j)$. The comparison target $Z$ (Lean explicitZ) is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults) on the same index domain.
The module is one chunk of a 256-way case split that discharges $N_2 = 8Z$ pointwise. The local setting is purely combinatorial: no continuum limit or curvature hypothesis is invoked; only exact integer equality of two Fin-4 kernels matters for the later assembly theorem.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted: the fold defining $N_2$ evaluates, and the pattern match defining $Z$ evaluates. Lean’s kernel decision procedure checks the resulting numeral equality $N_2(0,2,2,0,0,2) = 8,Z(0,2,2,0,0,2)$.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N_2=8Z$ by exhaustive fin_cases over Fin 4. That global identity is the algebraic certificate that the midpoint numerator matches eight times the explicit Regge kernel, a step in the 4D TT-identity analysis for discrete gravity in the Recognition stack.
It does not itself touch the forcing chain (T0–T8), RCL, or $\phi$-ladder mass formulae; it is infrastructure inside the gravity analysis layer that keeps the midpoint/TT bookkeeping exact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.