e_333232
plain-language theorem explainer
Pointwise identity: the midpoint Regge mass-squared numerator at multi-index (3,3,3,2,3,2) equals eight times the explicit Z-table entry there. Gravity analysts assembling the 4D kernel identity cite it as one of 256 concrete cases. The proof is a single kernel decide on fixed Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(3,3,3,2,3,2)$ 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 table on six $\mathbb{F}_4$ arguments.
background
This module is chunk 15 of a 256-case kernel certifying that the midpoint Regge $m_2$ numerator matches eight times an explicit integer table on every six-tuple of $\mathbb{F}_4$ indices. The local setting is pure finite enumeration: no continuum limit, only integer arithmetic on the discrete index set.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution functional over a fixed coupling list, starting from zero. The companion table $Z$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments (sample clauses return $4$, $-2$, etc.). Both live in the kernel-cert module imported here.
The equality $m_2^{\mathrm{num}}=8Z$ is the algebraic content needed before assembling curvature or mass-squared identities in the 4D Regge midpoint analysis.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $3,3,3,2,3,2$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit table. The kernel closes the goal because both expressions reduce to closed integer terms.
why it matters
Feeds the universal assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the claim by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one is a leaf of that case tree.
In the gravity stack this identity is bookkeeping for the exact midpoint Regge kernel in 4D: once every multi-index matches, the numerator can be replaced by the closed $Z$-table in downstream curvature or mass-squared arguments. It does not itself touch the forcing chain (T0–T8), $\phi$-ladder masses, or $\alpha$; it is discrete linear-algebra support under the Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.