e_011201
plain-language theorem explainer
For the six-index slot (0,1,1,2,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel cells. The proof is a pure kernel decide on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,2,0,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The local goal, stated in the module header, is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index tuples by kernel decides (here chunk 1, 256 cells).
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 integer-valued kernel on six $\mathrm{Fin},4$ indices, given by a finite pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
Both definitions live in the KernelCert module imported here. The present declaration fixes one concrete six-tuple and asserts the scalar identity on that cell.
proof idea
One-line kernel proof: by decide. Lean reduces both sides of $m_2^{\mathrm{num}}(0,1,1,2,0,1)=8\cdot Z(0,1,1,2,0,1)$ to concrete integers (the fold over the coupling list on the left, the pattern match on the right) and checks equality by computation. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
The parent theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices is assembled by exhaustive fin_cases on $(a,b,c,d,i,j)$, each leaf a cell identity of this form. This declaration supplies the leaf for $(0,1,1,2,0,1)$.
In the Recognition gravity stack, the exact midpoint M2 TT identity is part of the discrete curvature / Regge analysis supporting the continuum limit of the recognition calculus. Closing the numerator-versus-explicit-kernel match cell-by-cell removes a computational gap in that certification. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is infrastructure under the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.