e_021200
plain-language theorem explainer
For the six Fin-4 indices (0,2,1,2,0,0), the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell in the exhaustive 4^6 case split that assembles the global identity. The proof is a single decide on concrete integers.
Claim. With indices $a{=}0$, $b{=}2$, $c{=}1$, $d{=}2$, $i{=}0$, $j{=}0$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit kernel integer: $N(0,2,1,2,0,0)=8\,Z(0,2,1,2,0,0)$.
background
This module sits in the 4D Regge midpoint analysis for the M2TT identity. The numerator $N=\texttt{m2Num}$ is defined by folding a fixed coupling list and summing local contributions at six $\mathrm{Fin},4$ slots (two edge pairs and a tensor index pair). The comparison target $Z=\texttt{explicitZ}$ is a hand-written integer kernel on the same six indices, with sparse nonzero values such as $\pm2$ and $4$ on selected patterns.
The module goal, stated up front, is the pointwise identity $N=8Z$ on a 256-cell chunk of the $4^6$ index cube, each cell discharged by kernel decide. Upstream, $N$ is the fold of $\texttt{contrib}$ over $\texttt{couplingZList}$, and $Z$ is the pattern-matching table of explicit integers.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,2,1,2,0,0)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the numerator fold and the explicit kernel table.
why it matters
Feeds the assembler theorem $\forall a,b,c,d,i,j,, N=8Z$, which runs nested fin_cases over all six indices and lands on chunk lemmas such as this one. That global identity is the certified algebraic core of the exact midpoint M2TT relation in 4D Regge calculus inside the Gravity analysis stack. It is bookkeeping rather than a forcing-chain step (T0–T8), but it closes a concrete computational obligation on the discrete curvature side of Recognition gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.