e_213020
plain-language theorem explainer
For the concrete 4D index sextuple (2,1,3,0,2,0), the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 4^6 case split that establishes the global M2–TT numerator identity. The proof is a single kernel decide on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,0,2,0)$ with each coordinate in $\{0,1,2,3\}$, the midpoint numerator satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{exp}}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list: each term adds the local coupling weight at $(a,b,c,d,i,j)$. The comparison target $Z_{\mathrm{exp}}$ is an explicit piecewise integer table on the same six indices (typical nonzero entries are $\pm 2,\pm 4$).
The module is chunk 9 of a 256-way decide partition of the identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{exp}}$. The ambient goal is an exact algebraic certificate for the midpoint M2–TT identity in four dimensions, with all arithmetic reduced to concrete Fin-4 cases.
proof idea
One-line computational proof: decide evaluates both sides at the fixed sextuple $(2,1,3,0,2,0)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $Z_{\mathrm{exp}}$ and multiplies by 8. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two definitions are required.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ and discharges the universal quantifier by exhaustive fin_cases. The chunk therefore closes one of the 4096 concrete obligations in the 4D Regge midpoint M2–TT numerator certificate.
Within Recognition Science gravity work, such exact kernel identities underwrite discrete curvature bookkeeping on the eight-tick lattice (T7) in $D=3$ spatial dimensions (T8). They are pure integer checks: no continuum limit or variational argument is invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.