e_033303
plain-language theorem explainer
For the multi-index (0,3,3,3,0,3) on Fin 4, the Regge midpoint m₂ numerator equals eight times the explicit Z coupling at those slots. Gravity analysts cite it when assembling the full 4D kernel identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. Let $m_2$ be the integer numerator obtained by folding the coupling list, and let $Z$ be the explicit integer coupling table on $(\mathrm{Fin}\,4)^6$. Then $m_2(0,3,3,3,0,3) = 8\,Z(0,3,3,3,0,3)$.
background
This module sits in the 4D Regge exact-midpoint analysis: one proves that a folded numerator m2Num agrees with eight times a closed-form table explicitZ on every 6-tuple of Fin-4 indices. The module doc states the local goal bluntly: "m2Num = 8·explicitZ, chunk 3 (256 kernel decides)."
m2Num a b c d i j is the integer fold of contrib over couplingZList. explicitZ is a pattern-matched Int table on six Fin-4 arguments (sample clauses give values such as 4, −2, …). Chunk files discharge one block of the $4^6$ cases by concrete evaluation rather than by a symbolic identity.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms at fixed Fin-4 indices, so the kernel reduces the equality to true with no lemmas or rewriting.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement ∀ a b c d i j, m2Num = 8·explicitZ by exhaustive fin_cases on the six indices; this chunk supplies one of those concrete cells. In the gravity stack the identity certifies that the midpoint TT m₂ numerator matches the explicit Z coupling used in the 4D Regge kernel, so later curvature and continuum-limit arguments can quote the closed form instead of the fold. It is bookkeeping inside the Gravity domain, not a forcing-chain (T0–T8) step, but it hardens the discrete geometric side that RS gravity analyses rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.