e_033011
plain-language theorem explainer
Pointwise check that the folded M2 numerator coupling equals eight times the explicit Z-table entry at multi-index (0,3,3,0,1,1). Gravity analysts assembling the 4D Regge midpoint TT identity cite the full family of such kernel facts. The proof is a single kernel decision on two concrete integers.
Claim. At indices $(a,b,c,d,i,j)=(0,3,3,0,1,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D Regge midpoint mass-squared numerator matches an explicit closed form. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex lattice with values in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list, accumulating integer contributions at each multi-index. The comparison target $Z$ is an explicit case-table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample entries include $4$ on diagonal pairs such as $(0,0,1,1,2,2)$ and $-2$ on mixed pairs such as $(0,0,1,2,1,2)$).
The local claim is one coordinate of the global identity $m_2^{\mathrm{num}}=8Z$ on the full $4^6$ grid.
proof idea
Both sides evaluate to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed. The tactic decide runs the kernel equality checker on those two integers and closes the goal. No algebraic rewriting or upstream lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete case in that case-split tree.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint TT mass-squared coupling in 4D Regge calculus. It does not itself invoke the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$), but it sits under the discrete-gravity layer those landmarks constrain. Closing all 256 decides removes a scaffolding obligation on the numerator side of the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.