e_021033
plain-language theorem explainer
For the multi-index (0,2,1,0,3,3) on Fin 4, the folded M2 numerator equals eight times the explicit Z-kernel entry. Gravity analysts cite it when discharging one concrete cell of the 4D Regge midpoint M2=8Z identity. The proof is a single kernel decide on the two integer definitions.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}0$, $i{=}3$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded M2 numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer Z-kernel $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge-calculus analysis of the exact midpoint M2–TT identity. The local goal, stated in the module doc, is to verify $m_2^{\mathrm{num}}=8\cdot Z$ on one 256-cell chunk of the six-index kernel by pure decision.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of a fixed coupling list: each term contributes an integer via a local contrib rule, summed from zero. The comparison target explicitZ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both sides are therefore closed integer expressions at any concrete six-tuple, so equality is a decidable arithmetic fact rather than an analytic identity.
proof idea
One-line proof: decide. Lean reduces both the fold that defines the M2 numerator and the pattern-matched explicit Z value at the fixed indices $(0,2,1,0,3,3)$, then checks the resulting integer equality $n=8z$ in the kernel. No lemmas are invoked beyond the two definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every six-index cell into the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases. This declaration is one concrete cell in chunk 2 of that cover.
In the broader Recognition gravity stack, the identity certifies that the discrete midpoint M2 numerator matches the closed-form Z kernel used in the 4D Regge TT analysis. It is bookkeeping infrastructure, not a new physical law: once every chunk cell is decided, the assembled equality can be cited without re-running the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.