e_033103
plain-language theorem explainer
For the six-index tuple (0,3,3,1,0,3) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2–TT identity certification. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,1,0,3)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The setting is the exact midpoint evaluation of the 4D Regge M2–TT identity used in the gravity analysis stack.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it accumulates integer contributions contrib t a b c d i j over couplingZList. The comparison target explicitZ is a closed-form case table on six Fin-4 indices, returning small integers such as $4$, $-2$, and so on for the nonzero patterns.
Each chunk theorem pins one concrete multi-index so the assembler can discharge the universal statement by exhaustive fin_cases without re-deriving the fold.
proof idea
One-line proof: by decide. Lean reduces both sides at the concrete indices $(0,3,3,1,0,3)$ to integers (the fold for $m_2^{\mathrm{num}}$ versus $8$ times the matching explicitZ clause) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles all 256 index cells into $\forall a b c d i j,, m_2^{\mathrm{num}}=8\cdot Z$ by nested fin_cases; this declaration is the cell for $(0,3,3,1,0,3)$. That universal identity is the algebraic backbone of the exact midpoint M2–TT certification in 4D Regge gravity analysis. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete kernel bookkeeping supporting the continuum gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.