e_211313
plain-language theorem explainer
For the six Fin-4 indices (2,1,1,3,1,3), the integer numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts cite this as one of the 256 kernel cells that assemble the exact midpoint M2–TT identity in 4D Regge calculus. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}1$, $d{=}3$, $i{=}1$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices appear. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each triple contributes an integer via a local kernel, and the fold sums them. The companion table $\mathrm{explicitZ}$ is a sparse case-split on the same six indices, returning small integers such as $4$, $-2$, or $0$.
The module is chunk 9 of a 256-cell kernel certification: every ordered 6-tuple in $(\mathrm{Fin},4)^6$ must satisfy $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$. That global identity is the algebraic content of the exact midpoint M2–TT relation used downstream in the gravity stack.
Upstream, both maps are defined in the KernelCert module; this chunk only evaluates one concrete cell.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(2,1,1,3,1,3)$ and checks integer equality. No lemmas are invoked; the kernel definitions reduce to closed integers under the decision procedure.
why it matters
The parent theorem m2Num_eq_eight_explicitZ quantifies over all six indices by exhaustive fin_cases, and each leaf is one of these chunk theorems. Without the full 256-cell cover, the exact midpoint M2–TT identity in 4D remains uncertified.
In the Recognition gravity analysis this identity is the discrete algebraic step that lets the continuum TT projector emerge from the Regge midpoint stencil. It sits inside the Gravity domain rather than the T0–T8 forcing chain, but it is load-bearing for any later claim that the discrete curvature kernel matches the continuum massless spin-2 projector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.