e_310200
plain-language theorem explainer
At multi-index (3,1,0,2,0,0) the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one concrete cell of the 256-case kernel identity. The proof is a single native decide on fully concrete Fin-4 arguments.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,2,0,0)$ with each entry 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
This module is chunk 13 of a 256-cell case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the four-dimensional midpoint Regge kernel. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer weight at the six-index slot $(a,b,c,d,i,j)$, and the fold sums those weights from zero. The comparison object $Z$ is an explicit piecewise integer table on the same six indices (typical nonzero values $\pm 2,,4$ on matched pairs).
The local goal is purely algebraic identity of two integer-valued maps, not a continuum limit or a variational principle. Upstream definitions supply the table and the fold; no analytic estimates enter.
proof idea
One-line computational proof: decide. Both sides evaluate at a fully concrete six-tuple of Fin 4 values, so Lean reduces the fold that defines the numerator and the pattern-match that defines $Z$ to bare integers and checks equality by the kernel decision procedure. No lemmas are invoked beyond that reduction.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhaustive fin_cases and dispatches each cell to a chunk lemma of this form. Closing all 256 cells certifies that the midpoint Regge $m_2$ numerator is exactly eight times the explicit $Z$-kernel in 4D, a discrete algebraic step inside the Gravity analysis stack. It does not itself touch the T0–T8 forcing chain, $\phi$-ladder masses, or continuum Einstein equations; it is bookkeeping that makes the exact midpoint identity machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.