e_203103
plain-language theorem explainer
For the concrete multi-index (2,0,3,1,0,3) on Fin 4, the Regge midpoint numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D M2–TT identity. The proof is a single decide on two fully evaluated integers.
Claim. For $a=2$, $b=0$, $c=3$, $d=1$, $i=0$, $j=3$ in $\{0,1,2,3\}$, the folded 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 exact-midpoint analysis, two integer kernels on six Fin-4 indices are compared. The numerator m2Num is the fold of a contribution map over a fixed coupling list: it sums every local term that the midpoint stencil attaches to the sextuple $(a,b,c,d,i,j)$. The comparison table explicitZ is a piecewise Int-valued function on the same domain, with a finite list of nonzero patterns (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$) and zero elsewhere.
The module is one chunk of the exhaustive case split that asserts $m_2^{\mathrm{num}}=8,Z$ at every point of $(\mathrm{Fin},4)^6$. Chunk 8 holds 256 such kernel decides; the present declaration is the single point $(2,0,3,1,0,3)$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of the numerator and the pattern-match definition of the explicit kernel, so the equality is a closed arithmetic fact with no further lemmas.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every sextuple by nested fin_cases on the six indices. Each leaf of that case tree is one of these chunk theorems; without the present equality the assembly fails at $(2,0,3,1,0,3)$.
In the broader Recognition gravity stack this identity is the algebraic core of the exact midpoint M2–TT relation in 4D: it converts the folded stencil numerator into a multiple of a sparse explicit kernel, which is the form needed for later continuum and continuum-limit arguments. It does not itself touch the forcing chain (T0–T8) or the J-cost, but it is infrastructure for the discrete gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.