e_010230
plain-language theorem explainer
For the six-index tuple (0,1,0,2,3,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic decide-cell in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}0$, $d{=}2$, $i{=}3$, $j{=}0$ in $\mathrm{Fin}\,4$, the integer $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit six-index kernel table.
background
In the 4D Regge midpoint analysis, two integer-valued six-index maps on $\mathrm{Fin},4$ are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contribution function, and the fold starts at zero. The companion map $Z$ (explicitZ) is a closed-form case table on the same six indices, returning small integers such as $4$, $-2$, and so on for the listed patterns.
The module is chunk 1 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. The ambient goal is an exact midpoint identity for the M2TT sector of discrete gravity, reduced to finitely many integer equalities on $\mathrm{Fin},4^6$.
proof idea
One-line proof by decide. Both sides evaluate to concrete integers for the fixed tuple $(0,1,0,2,3,0)$: the left via the fold definition of $m_2^{\mathrm{num}}$, the right via table lookup in $Z$ scaled by 8. No lemmas are invoked beyond kernel computation of those definitions.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8Z$ for all six indices, which exhausts $\mathrm{Fin},4$ by nested fin_cases and dispatches each cell to a chunk equality of this form. That global identity is the certified algebraic core of the Regge exact-midpoint M2TT relation in four dimensions. Within Recognition gravity, such kernel equalities pin the discrete curvature bookkeeping before continuum or phenomenological limits are taken; they do not themselves invoke the forcing chain (T5–T8) or the J-cost, but they stabilize the 4D geometric side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.