e_332012
plain-language theorem explainer
For the six-index slot (3,3,2,0,1,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel entry explicitZ. 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 kernel decide on integer arithmetic.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator at $(3,3,2,0,1,2)$ satisfies $m_2^{\mathrm{num}}(3,3,2,0,1,2)=8\,Z(3,3,2,0,1,2)$, where $Z$ is the explicit integer kernel table.
background
This module is chunk 15 of a 256-cell kernel certification that the 4D Regge midpoint M2 numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, matching discrete 4-simplex edge/face labels in the Regge calculus setting.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums a local contribution at each coupling triple against the six indices. The companion table $Z(a,b,c,d,i,j)$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical nonzero values $\pm 2,,4$ on the listed support).
The local claim is one concrete cell of the identity $m_2^{\mathrm{num}}=8Z$. Upstream definitions supply both sides; no analytic continuum limit is invoked here.
proof idea
One-line proof by decide. Lean reduces both sides of the equality on the concrete six-tuple $(3,3,2,0,1,2)$: the fold defining the numerator evaluates to an integer, the explicit table lookup yields an integer, and the kernel checks that the former is eight times the latter. No lemmas beyond the two definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six $\mathrm{Fin},4$ indices and discharges the universal statement by exhaustive fin_cases, invoking one cell theorem per tuple. This declaration is the cell for $(3,3,2,0,1,2)$ inside chunk 15 of that assembly.
In the Recognition gravity stack, the exact midpoint M2–TT identity is bookkeeping for discrete curvature/coupling consistency on the 4D Regge complex. Certifying numerator equals $8Z$ cellwise removes a sorry-shaped gap in that algebraic identity. It does not itself force $D=3$ or the eight-tick octave; those live upstream in the forcing chain. It is pure finite integer verification supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.