e_012101
plain-language theorem explainer
For the fixed multi-index (0,1,2,1,0,1) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a=0$, $b=1$, $c=2$, $d=1$, $i=0$, $j=1$ in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on sextuples of Fin 4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution function, and the fold starts at zero. The explicit kernel $Z$ is a closed-form case table on the same six indices, returning small integers such as $4$, $-2$, and so on.
The module is chunk 1 of a 256-way kernel split that discharges $m_2^{\mathrm{num}}=8Z$ pointwise. The ambient goal is the exact midpoint M2TT identity in four dimensions, certified by matching the folded numerator against eight times the tabulated kernel on every index sextuple.
proof idea
Both sides are closed integer expressions at a fully concrete sextuple, so decide evaluates $m_2^{\mathrm{num}}(0,1,2,1,0,1)$ and $8\cdot Z(0,1,2,1,0,1)$ in the kernel and checks equality. No lemmas are invoked beyond the definitions of the fold and the case table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin 4 sextuple by nested fin_cases and needs one equality per cell; this declaration is the cell for $(0,1,2,1,0,1)$. That universal 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 pure discrete-curvature bookkeeping that keeps the midpoint identity fully machine-checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.