e_130202
plain-language theorem explainer
For the six Fin-4 indices (1,3,0,2,0,2), the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it as one of the 256 kernel cells in the Regge exact-midpoint M2TT identity. The proof is a single `decide` on concrete integer arithmetic.
Claim. With indices in $\{0,1,2,3\}$, the midpoint numerator satisfies $m_2^{\mathrm{num}}(1,3,0,2,0,2)=8\,Z_{\mathrm{explicit}}(1,3,0,2,0,2)$.
background
This module is chunk 7 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times an explicit integer table. The ambient setting is discrete gravity: edge couplings on a 4-simplex (or 4-cube) lattice, with all six arguments ranging over Fin 4.
m2Num a b c d i j is defined by folding a fixed coupling list and summing a local contribution at each term. explicitZ is the matching closed-form integer table (pattern-matched on the six indices), with sample values such as $4$, $-2$, and so on. The claim under audit is one concrete cell of the equality m2Num = 8 · explicitZ.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the literal indices $(1,3,0,2,0,2)$ to concrete integers (via the fold definition of m2Num and the pattern match of explicitZ) and checks equality in the kernel. No lemmas are invoked beyond the two definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles all $4^6$ cells by nested fin_cases and cites each chunk theorem such as this one. That global identity is the algebraic core of the Regge exact-midpoint M2TT certification in 4D gravity analysis inside the monolith. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is infrastructure for the discrete curvature / mass-side gravity bookkeeping that later interfaces with RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.