e_313010
plain-language theorem explainer
One kernel cell of the 4D Regge midpoint identity: the folded coupling numerator at index tuple (3,1,3,0,1,0) equals eight times the explicit integer kernel at that tuple. Gravity analysts cite it only as a brick in the full six-index case split. Proof is a single `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,0,1,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the TT-sector mass-squared numerator is assembled by folding a fixed coupling list: each term contributes an integer depending on six indices in $\mathrm{Fin},4$, and $m_2^{\mathrm{num}}$ is that fold starting from zero. The companion map $Z$ is an explicit piecewise-integer table on the same six indices (sample values include $4$, $-2$, and so on).
The module is chunk 13 of a 256-cell kernel certification whose sole job is to check $m_2^{\mathrm{num}}=8Z$ pointwise. The present cell is the single tuple $(3,1,3,0,1,0)$. Upstream definitions supply only the fold and the table; no continuum geometry is invoked here.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int expressions (the fold of contrib over couplingZList versus eight times the matching explicitZ clause) and closes the equality by computation. No lemmas beyond the two definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six $\mathrm{Fin},4$ indices and discharges the goal by exhaustive fin_cases; each leaf is one of these e_* cells. Without the pointwise identities the assembly cannot finish. In the broader Recognition gravity stack this certifies that the discrete midpoint M2 numerator is exactly eight times the closed-form kernel, a purely combinatorial step toward the Regge TT identity in four dimensions. It does not itself touch the forcing chain (T0–T8), $\phi$, or continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.