e_000332
plain-language theorem explainer
For the six-index slot (0,0,0,3,3,2) on Fin 4, the folded numerator m2Num equals eight times the tabulated closed form explicitZ. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. For the concrete values $(a,b,c,d,i,j)=(0,0,0,3,3,2)$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding the coupling list equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge-calculus analysis of the exact midpoint M2 TT identity. The local setting is chunk 0 of a 256-way case split: each theorem checks $m_2^{\mathrm{num}}=8\cdot Z$ at one multi-index in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at those six indices. The comparison target $Z$ is an explicit piecewise integer function on the same six Fin-4 arguments (tabulated values such as $4$, $-2$, and so on).
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are supplied by the kernel certificate module; this declaration only evaluates them at one point.
proof idea
One-line computational proof: decide. Lean reduces both sides at the concrete indices $(0,0,0,3,3,2)$ to closed integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of the folded numerator and the explicit table.
why it matters
The parent theorem is the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$, assembled by exhaustive Fin-case split over all six indices. Each chunk theorem such as this one discharges one cell of that $4^6=4096$-sized grid (here in the chunk-0 block of 256 kernel decides).
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint discrete curvature/TT sector in four dimensions: it certifies that the summed coupling numerator matches the closed-form table used downstream. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure integer algebra supporting the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.