e_010101
plain-language theorem explainer
For the concrete multi-index (0,1,0,1,0,1) on Fin 4, the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell of the 256-case kernel table. The proof is a single decide on fully evaluated integers.
Claim. For indices $a=0$, $b=1$, $c=0$, $d=1$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel entry $Z_{\mathrm{expl}}(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel certification that the Regge exact-midpoint numerator equals eight times an explicit integer table on all sextuples in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete cell of that table identity, not the universal statement.
proof idea
Both sides are closed integer terms once the six indices are fixed to $0,1,0,1,0,1$. The tactic decide evaluates $m_2^{\mathrm{num}}$ (the fold over the coupling list) and $8\cdot Z_{\mathrm{expl}}$ and checks propositional equality of the resulting Int values. No lemmas beyond the definitions of m2Num and explicitZ are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases and needs each cell proved. This declaration discharges the single cell $(0,1,0,1,0,1)$ inside chunk 1 of that kernel.
In the gravity analysis stack, the identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ is the certified algebraic core of the Regge exact-midpoint M2/TT comparison in 4D. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel bookkeeping that later continuum or continuum-limit arguments can quote without re-deciding 256 cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.