e_013233
plain-language theorem explainer
Single index case of the 4D midpoint Regge identity: the folded mass-squared numerator at (0,1,3,2,3,3) equals eight times the explicit Z-table entry. Gravity analysts cite it only as one cell in the exhaustive Fin-4 kernel. The proof is a bare kernel decide on the unfolded integer equality.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,3,3)$ 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 coupling $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry for the given indices. The comparison target is an explicit piecewise table $Z$ on the same sextuples, with small integer values such as $4$, $-2$, and so on at the listed patterns.
The module is a pure kernel chunk: it discharges one of 256 decide-goals in chunk 1 of the identity $m_2^{\mathrm{num}}=8Z$. No continuum geometry is invoked here; the objects are finite combinatorial couplings on a 4-label index set.
proof idea
One-line kernel proof: decide evaluates both sides after unfolding the fold that defines the numerator and the pattern-match table that defines $Z$, then checks the resulting integer equality at the concrete sextuple $(0,1,3,2,3,3)$. No lemmas beyond definitional reduction are required.
why it matters
Feeds the assembled universal statement that $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ for every sextuple in $(\mathrm{Fin},4)^6$. That parent theorem is proved by nested fin_cases on all six indices; each concrete cell such as this one is a discharged branch of that case split.
In the broader gravity stack this identity is bookkeeping for the exact midpoint mass-squared coupling in 4D Regge analysis. It does not itself invoke Recognition landmarks (T5 J-cost, $\varphi$, eight-tick), but it is part of the certified discrete curvature/mass pipeline those landmarks eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.