e_233301
plain-language theorem explainer
For the discrete index tuple (2,3,3,3,0,1), the midpoint Regge mass-numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 4D kernel identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}3$, $c{=}3$, $d{=}3$, $i{=}0$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-cell decide table proving that the Regge midpoint mass numerator equals eight times an explicit integer kernel on every 4D index sextuple. The ambient setting is discrete gravity analysis: couplings on $\mathrm{Fin},4$ edges assembled into a numerator that should match a closed-form kernel.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution at each term for the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same indices (typical values $\pm 2,,4$, and zero off-pattern).
The local claim is one concrete sextuple in that table: indices $(2,3,3,3,0,1)$. Sibling chunks cover the other cells; the assemble theorem quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the equality is a pure arithmetic decision with no lemmas beyond evaluation of m2Num and explicitZ.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over the six indices and discharge of each cell. Without the chunk equalities, the assemble proof has nothing to case on.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass term in 4D: the folded coupling numerator is forced to the explicit kernel, so later continuum or continuum-limit arguments can quote a closed integer factor rather than an opaque fold. It does not itself invoke the T0–T8 forcing chain, but it sits in the gravity-analysis layer that consumes discrete geometric identities once dimension and tick structure are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.