e_123233
plain-language theorem explainer
For the single multi-index (1,2,3,2,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one of the 256 kernel cells. The proof is a pure `decide` discharge of integer equality after unfolding both sides.
Claim. With indices in $\mathrm{Fin}\,4$, $m_2^{\mathrm{num}}(1,2,3,2,3,3)=8\,Z_{\mathrm{explicit}}(1,2,3,2,3,3)$, where $m_2^{\mathrm{num}}$ is the fold of coupling contributions and $Z_{\mathrm{explicit}}$ is the sparse integer table of the kernel certificate.
background
The ambient module certifies the exact midpoint M2–TT identity in 4D Regge calculus by showing that a folded numerator built from coupling contributions equals eight times a sparse closed-form table. Concretely, m2Num a b c d i j accumulates contrib over couplingZList, while explicitZ is a pattern-matched integer function on six Fin 4 indices (nonzero only on a short list of index patterns such as (0,0,1,1,2,2) ↦ 4).
The local file is chunk 6 of a 256-cell kernel: each cell fixes one concrete six-tuple and asserts the scalar identity at that point. The parent assembly then quantifies over all of Fin 4^6 by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. After unfolding m2Num (the fold) and explicitZ (the matching table) at the concrete indices 1,2,3,2,3,3, both sides reduce to closed integers; the kernel decides equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ, which asserts ∀ a b c d i j, m2Num = 8 · explicitZ by casing every Fin 4 coordinate and landing on cells such as this one. That identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in 4D gravity analysis: it replaces a summed coupling expression by an explicit sparse integer kernel, enabling exact (not approximate) midpoint evaluations. Inside Recognition Science gravity work this is bookkeeping infrastructure rather than a T0–T8 landmark, but it is required before continuum or continuum-limit claims that quote the midpoint identity can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.