e_033101
plain-language theorem explainer
For the six-index tuple (0,3,3,1,0,1) on Fin 4, the folded numerator m2Num equals eight times the tabulated explicitZ kernel entry. Gravity analysts assembling the exact 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,1,0,1)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,3,3,1,0,1)=8\,Z_{\mathrm{explicit}}(0,3,3,1,0,1)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling triple at the given indices. The comparison target $Z_{\mathrm{explicit}}$ is a sparse case table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 3 of a 256-cell partition of the Fin-4^6 domain. Its sole job is to certify $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ on that chunk by kernel decision, so a later assembler can glue the cells into a universal identity.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (the fold over the coupling list versus eight times the matching explicitZ clause or default), and Lean’s decision procedure checks equality.
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhaustive fin_cases over Fin 4. That identity is the algebraic backbone of the exact 4D Regge midpoint M2–TT comparison in the Gravity analysis stack. Without each chunk cell (including this one), the assembler cannot close the forall. Landmark link is local to the Regge/gravity side rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.