e_123002
plain-language theorem explainer
For the single index sextuple (1,2,3,0,0,2) in (Fin 4)^6, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2TT identity. The proof is a pure kernel decision (`decide`) with no algebraic rewriting.
Claim. For indices $a{=}1,b{=}2,c{=}3,d{=}0,i{=}0,j{=}2$ in $\mathrm{Fin}\,4$, the integer numerator coupling sum $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge-exact midpoint numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: couplings on oriented 4-simplices with midpoint edge data.
The numerator side m2Num is defined by folding a fixed contribution list couplingZList over six Fin 4 indices, accumulating integer contrib terms. The right-hand side explicitZ is a sparse pattern-matched table Fin 4^6 → ℤ (nonzero only on a handful of index patterns such as (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ −2).
The local claim is one concrete sextuple evaluation inside that table identity, not the universal statement.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality (the fold that defines the numerator, and the pattern match that defines the explicit kernel) to concrete Int literals and checks equality in the kernel. No lemmas are invoked; no rewriting or case split appears in this chunk.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which asserts the identity for every sextuple in (Fin 4)^6 by exhaustive fin_cases and therefore depends on each atomic cell such as this one. The module header frames the work as “m2Num = 8·explicitZ, chunk 6 (256 kernel decides)”: this declaration is one of those 256 decides.
In the broader Recognition gravity stack the identity certifies that the discrete midpoint M2TT numerator collapses to a sparse explicit kernel, a bookkeeping step toward exact Regge-type curvature identities in four dimensions. It does not itself touch the forcing chain (T0–T8), φ-ladder masses, or α; it is pure discrete-gravity algebra supporting later continuum or continuum-limit claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.