e_323301
plain-language theorem explainer
For the Fin-4 index sextuple (3,2,3,3,0,1), the folded Regge midpoint numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts assembling the 4D midpoint M2TT identity cite this as one decided cell in chunk 14 of the 256-kernel certificate. Proof is a single decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}2$, $c{=}3$, $d{=}3$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\cdot Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six $\mathrm{Fin}\,4$ indices.
background
This module is one certificate chunk in the 4D Regge exact-midpoint M2TT identity: it asserts the pointwise relation $m_2^{\mathrm{num}}=8\cdot Z$ on a block of kernel cells (chunk 14; 256 decides).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z$ is an explicit six-index integer table on $\mathrm{Fin},4$ (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the KernelCert module imported here. The local goal is only the single cell $(3,2,3,3,0,1)$, not the universal quantification.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed, so the kernel decision procedure discharges equality with no lemmas or rewriting.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies a decided cell so the universal midpoint identity can be glued without re-running the fold at assemble time.
In the Recognition gravity stack this is bookkeeping for the exact 4D Regge midpoint M2TT kernel, not a forcing-chain (T0–T8) step. It closes one concrete obligation inside the larger claim that the numerator factors as eight times the explicit kernel everywhere on the $4^6$ index space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.