e_300010
plain-language theorem explainer
For the multi-index tuple (3,0,0,0,1,0) on Fin 4, the summed Regge midpoint numerator m2Num equals eight times the sparse kernel value explicitZ. Gravity analysts cite the identity when assembling the full 4D midpoint mass-squared certificate. The proof is a single decide on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=0$, $d=0$, $i=1$, $j=0$ in $\mathrm{Fin}\,4$, the folded coupling sum $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit sparse kernel entry $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis the numerator m2Num folds a fixed coupling list, adding one integer contribution for each coupling triple at the six Fin-4 indices. The companion map explicitZ is a sparse pattern on those same indices: most tuples evaluate to zero, while a handful of matched pairs return small constants such as 4 or -2.
The present module is one of the 256 kernel-decide chunks that certify the global relation m2Num = 8 · explicitZ. Chunk 12 isolates a block of index sextuples; the surrounding KernelCert module supplies both definitions used here.
proof idea
The statement is a pure ground equality of two concrete Int expressions. Lean’s decide tactic evaluates the fold that defines m2Num at (3,0,0,0,1,0) and the corresponding explicitZ clause, then checks that the two sides differ by the factor 8. No lemmas beyond the two definitions are required.
why it matters
The identity is one atomic case consumed by m2Num_eq_eight_explicitZ, which exhausts all Fin-4 sextuples by nested fin_cases and therefore needs every chunk theorem. That global equality is the algebraic core of the 4D Regge midpoint mass-squared certificate in the Gravity analysis layer. It does not itself invoke the T0–T8 forcing chain, yet it supplies a verified discrete kernel step that later continuum or continuum-limit arguments in the same gravity stack can quote without re-checking arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.