e_303333
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (3,0,3,3,3,3) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one of 256 kernel cells in the Regge midpoint M2–TT 4D certification. The proof is a single `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,3,3,3,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contrib, summed from zero. The comparison target is an explicit sparse table $Z$ on the same six indices (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonals $\mapsto -2$).
This module is chunk 12 of the 256-cell kernel certification that $m_2^{\mathrm{num}}=8Z$ everywhere. The local setting is pure finite enumeration: no continuum limit, no floating point.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(3,0,3,3,3,3)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the fold m2Num and the pattern-matched table explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one cell so the universal identity is a pure case split with no analytic gap. In the broader gravity stack this identity is the algebraic core of the Regge midpoint M2–TT match in 4D; it does not itself invoke the RS forcing chain (T5–T8), but it sits inside the discrete curvature bookkeeping that those continuum claims later rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.