e_300033
plain-language theorem explainer
Kernel identity: the midpoint Regge mass-squared numerator at multi-index (3,0,0,0,3,3) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one cell of the 256-case certification that m2Num = 8·explicitZ on (Fin 4)^6. The proof is a single decide on the unfolded integer equality.
Claim. For indices $(a,b,c,d,i,j)=(3,0,0,0,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 table value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D midpoint Regge identity certification: every cell of the six-index kernel must satisfy $m_2^{\mathrm{num}}=8\cdot Z$. The local setting is pure integer arithmetic on $\mathrm{Fin},4$ indices (no continuum limit yet).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the given indices. The companion table $Z$ is an explicit pattern-matched integer function on six $\mathrm{Fin},4$ arguments (sample clauses return $4$, $-2$, etc.).
The identity $m_2^{\mathrm{num}}=8Z$ is the algebraic content being certified cell-by-cell before assembly over the full $4^6$ domain.
proof idea
One-line kernel decide. Lean unfolds $m_2^{\mathrm{num}}$ (the fold over the coupling list) and $Z$ (the pattern match) at the concrete indices $(3,0,0,0,3,3)$, reduces both sides to closed integers, and checks equality by the decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem $m_2^{\mathrm{num}}=8Z$ for all $a,b,c,d,i,j:\mathrm{Fin},4$, which exhausts the six-index domain by finitary case split and consumes this cell among the 256 kernel decides. That global identity is the algebraic backbone of the exact midpoint mass-squared / TT identity in the 4D Regge analysis stack under Gravity.
Within Recognition Science this sits in the discrete-geometry layer that supports continuum gravity limits; it does not itself touch the forcing chain (T5 J-uniqueness, T6 $\phi$, T7 eight-tick, T8 $D=3$), but it hardens the combinatorial side of the Regge sector those continuum claims rest on. Closing all chunks removes scaffolding from the midpoint identity path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.