e_013123
plain-language theorem explainer
For the six-index tuple (0,1,3,1,2,3) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With $m_2^{\mathrm{num}}$ the fold of coupling contributions over the 4D index list and $Z_{\mathrm{ex}}$ the explicit integer kernel on six $\mathrm{Fin}\,4$ indices, one has $m_2^{\mathrm{num}}(0,1,3,1,2,3)=8\,Z_{\mathrm{ex}}(0,1,3,1,2,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple of Fin 4 indices. The local setting is pure finite enumeration (256 kernel decides per chunk).
Upstream, m2Num a b c d i j is the fold of contrib over couplingZList, starting from 0. explicitZ is a pattern-matched Int table on the same six indices (sample entries: (0,0,1,1,2,2) maps to 4, (0,0,1,2,1,2) to -2). The identity asserts these two agree up to the constant factor 8.
The surrounding Gravity.Analysis development treats this as a certified algebraic identity inside the discrete curvature / TT-sector bookkeeping for Regge calculus in four dimensions.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the kernel closes the equality with no lemmas and no case split inside this declaration.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states the universal claim $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ and discharges it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete cell of that table.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint M2 TT identity in 4D, not a forcing-chain (T0–T8) step. It closes a finite algebraic obligation so later curvature and continuum-limit arguments can quote a fully certified numerator–kernel match rather than an unchecked expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.