e_013330
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,1,3,3,3,0) equals eight times the explicit integer table at that same point. Gravity analysts cite it as one kernel cell in the 4D midpoint M2TT numerator certification. The proof is a single native `decide` on concrete integers.
Claim. For the multi-index $(0,1,3,3,3,0)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form table entry: $m_2^{\mathrm{num}}(0,1,3,3,3,0)=8\,Z_{\mathrm{expl}}(0,1,3,3,3,0)$.
background
This module is chunk 1 of a kernel certification that the 4D Regge midpoint numerator m2Num agrees with eight times an explicit integer table explicitZ on every sextuple of Fin 4 indices (256 decides per chunk).
m2Num a b c d i j is the fold of a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList. explicitZ is a pattern-matched closed form Fin 4^6 → ℤ (sample clauses include (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ -2).
The local goal is purely algebraic bookkeeping: evaluate both sides at one concrete multi-index and check equality in ℤ.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel decision procedure discharges the equality with no lemmas and no case split.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every a b c d i j : Fin 4 by exhaustive fin_cases. That universal equality is the numerator half of the Regge exact midpoint M2TT identity in 4D gravity analysis inside the monolith.
In the broader Recognition stack this is scaffolding for the discrete geometric side of the gravity sector (Regge calculus on the eight-tick / D=3 forced lattice), not a forcing-chain (T0–T8) step. It closes one of 256 kernel cells in chunk 1 so the assemble proof can treat the identity as fully decided rather than axiomatic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.