e_213023
plain-language theorem explainer
For the concrete multi-index (2,1,3,0,2,3) on Fin 4, the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D midpoint M2 TT identity cite this as one of 256 kernel cells. The proof is a single decide on fixed integer data.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}3$, $d{=}0$, $i{=}2$, $j{=}3$ in $\mathrm{Fin}\,4$, the discrete midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a coupling list: each term contributes via a local contrib and the accumulator starts at $0$. The comparison target is explicitZ, a sparse case table of small integers (entries such as $4$, $-2$, and so on on selected index patterns).
This module is chunk 9 of the 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The ambient goal is an exact algebraic identity for the midpoint M2 TT sector in discrete gravity, reduced to finitely many integer equalities on $\mathrm{Fin},4^6$.
proof idea
One-line computational discharge: decide evaluates both sides at the fixed sextuple $(2,1,3,0,2,3)$ and checks integer equality. No lemmas are invoked beyond the concrete unfoldings of $m_2^{\mathrm{num}}$ (fold over the coupling list) and of the explicitZ case table at those indices.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices. Each cell such as this one closes one branch of that case tree.
In the Recognition gravity stack this is pure discrete-kernel bookkeeping for the Regge midpoint identity in four dimensions: once every cell matches, the global factor-of-eight relation is certified and can be used upstream of continuum or continuum-limit arguments. It does not itself touch the forcing chain (T0–T8), $\varphi$, or the eight-tick octave; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.