e_022133
plain-language theorem explainer
For the six-index slot (0,2,2,1,3,3) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,1,3,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $m_2^{\mathrm{num}}(0,2,2,1,3,3)=8\,Z_{\mathrm{explicit}}(0,2,2,1,3,3)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint M2–TT identity certification. The goal across the chunk family is the pointwise integer identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ on all six-tuples in $(\mathrm{Fin},4)^6$.
Here $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: it accumulates every local contribution contrib at those indices. $Z_{\mathrm{explicit}}$ is the sparse closed-form table of the same kernel (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonal pairs $\mapsto -2$).
Module doc fixes the local contract: prove $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ cell-by-cell via 256 kernel decides, this file being chunk 2.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values once the six Fin-4 indices are substituted into the fold definition of m2Num and the pattern-match table explicitZ, so the equality is a closed integer computation discharged by the kernel.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhaustive fin_cases on all six indices; each case lands on a chunk lemma of this form. Without the cell-wise certificates the assemble step cannot close.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint M2–TT comparison in 4D Regge calculus: it converts a summed coupling expression into an explicit sparse integer kernel, which is what later curvature and continuum-limit arguments consume. It is bookkeeping inside the Gravity domain rather than a T0–T8 forcing step, but it is load-bearing for any claim that the discrete midpoint operator matches the continuum TT projector on the nose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.