e_013032
plain-language theorem explainer
For the six-index tuple (0,1,3,0,3,2) on Fin 4, the Regge midpoint m2 numerator equals eight times the explicit Z coupling. Gravity analysts cite it as one atomic case of the 4D midpoint M2–TT kernel identity. The proof is a single kernel decide on the closed integer expression.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}3$, $d{=}0$, $i{=}3$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded midpoint numerator satisfies $m_2^{\mathrm{num}}(0,1,3,0,3,2)=8\,Z_{\mathrm{explicit}}(0,1,3,0,3,2)$.
background
This module is chunk 1 of a 256-case kernel certification that the Regge midpoint m2 numerator equals eight times an explicit integer coupling table on $(\mathrm{Fin},4)^6$. The ambient setting is 4D discrete gravity analysis: index sextuples label pairs of edge/face data in the midpoint TT identity.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those indices. The comparison target $Z_{\mathrm{explicit}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern table (sample entries include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local claim is only the single sextuple $(0,1,3,0,3,2)$. Sibling theorems cover the other tuples in the same chunk; the assembly theorem quantifies over all of $\mathrm{Fin},4$.
proof idea
One-line computational proof: decide. Both sides are closed integer terms once the six concrete Fin 4 values are substituted into the fold definition of the numerator and the pattern table for explicit Z, so the kernel equality checker discharges the goal with no lemmas or case splits in this file.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by six nested fin_cases sweeps. Each atomic theorem such as this one is a leaf that the case split lands on (or is equivalent to under kernel evaluation).
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge M2–TT relation in 4D, not a forcing-chain landmark (T5–T8). It closes one cell of the finite certificate that the numerator factorization matches the explicit coupling table, so later continuum or continuum-limit arguments can quote a fully discharged discrete identity rather than an open summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.