e_313330
plain-language theorem explainer
Pointwise identity: the folded coupling numerator m2Num at multi-index (3,1,3,3,3,0) equals eight times the explicit integer table explicitZ at those same Fin-4 indices. Gravity analysts cite it as one of 256 kernel cells in the Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,3,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer lookup table on six $\mathrm{Fin}\,4$ arguments.
background
This module is chunk 13 of a 256-cell kernel certification that the numerator mass-squared coupling equals eight times a closed-form integer table, written $m_2^{\mathrm{num}}=8\cdot Z$ on all of $(\mathrm{Fin},4)^6$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: it accumulates contrib terms over couplingZList into an Int. The companion explicitZ is a pattern-matched integer table on six Fin 4 indices (sample entries include $4$, $-2$, and so on for distinguished index patterns).
The local setting is exact midpoint analysis for a 4D Regge-type M2TT identity in the Gravity domain: every concrete six-tuple must match before the universal statement can be assembled.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values at the fixed indices $(3,1,3,3,3,0)$, so the kernel decision procedure discharges the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk cell per tuple. Without each pointwise decide (including this $(3,1,3,3,3,0)$ cell), the universal glue fails.
In the Recognition gravity stack this closes a numerator identity used in Regge-midpoint curvature bookkeeping in 4D. It is pure finite enumeration support, not a forcing-chain (T0–T8) step, but it is load-bearing for the certified M2TT midpoint algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.