e_333110
plain-language theorem explainer
For the single multi-index (3,3,3,1,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a pure kernel decide on integer equality.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $m_2^{\mathrm{num}}$ for the fold of coupling contributions and $Z_{\mathrm{ex}}$ for the explicit integer kernel, one has $m_2^{\mathrm{num}}(3,3,3,1,1,0)=8\,Z_{\mathrm{ex}}(3,3,3,1,1,0)$.
background
In the 4D Regge midpoint analysis the squared-mass numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term adds an integer contribution depending on six Fin-4 indices. The companion map $Z_{\mathrm{ex}}$ is an explicit piecewise-integer function on the same six indices (sample values include $\pm 2,,4$ on the diagonal and off-diagonal patterns).
The local module is chunk 15 of a 256-cell partition that certifies the pointwise identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ by exhaustive kernel evaluation. Indices run over the discrete 4-simplex edge/vertex labels used in the Regge triangulation.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the concrete sextuple $(3,3,3,1,1,0)$ inside the Lean kernel and closes the goal. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z_{\mathrm{ex}}$ are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by nested fin_cases on the six Fin-4 arguments; each cell such as this one discharges one concrete branch. Establishing $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ pointwise is the algebraic core of the exact midpoint M2–TT identity in the 4D Regge gravity analysis. It sits inside the broader Recognition gravity stack that ultimately constrains continuum limits against the forced $D=3$ spatial skeleton (T8) and the eight-tick discrete clock (T7), though this cell itself is purely combinatorial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.