e_223102
plain-language theorem explainer
For the six-index slot (2,2,3,1,0,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one of the 256 decided cells that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the midpoint Regge numerator $m_2^{\mathrm{num}}(2,2,3,1,0,2)$ equals $8$ times the explicit six-index kernel $Z(2,2,3,1,0,2)$.
background
This module is chunk 10 of a 256-cell case split proving that the folded coupling numerator equals eight times an explicit integer kernel on every 4D midpoint index tuple.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each term. The companion map $Z(a,b,c,d,i,j)$ is an explicit piecewise integer table on $\mathrm{Fin},4^6$ (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
The ambient goal is the exact midpoint $M_2$ TT identity in 4D Regge analysis: once every cell satisfies $m_2^{\mathrm{num}}=8Z$, the assembled theorem holds without residual case obligations.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(2,2,3,1,0,2)$: the fold defining $m_2^{\mathrm{num}}$ evaluates, $Z$ matches its table clause (or default), and the kernel checks equality to $8Z$. No lemmas are invoked beyond decidable arithmetic on integers.
why it matters
Feeds the parent assembly theorem 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 over all six $\mathrm{Fin},4$ arguments, each leaf a chunk equality such as this one.
In the Recognition gravity stack this closes a numerical identity in the exact midpoint Regge $M_2$ TT analysis in 4D: the folded coupling numerator is identically eight times the explicit kernel, so continuum or continuum-limit arguments can quote a fully decided algebraic fact rather than a schematic ansatz. It is pure case infrastructure, not a forcing-chain step (T0–T8), but it hardens the discrete gravity side that sits under continuum RS claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.