regge_linearity
plain-language theorem explainer
The theorem establishes that squared masses on Regge trajectories add linearly with total excitation number n. Hadron modelers in the Recognition Science setting cite it when composing states from separate excitation quanta on the phi-ladder. The proof is a direct algebraic reduction: simplification unfolds the definition of the mass-squared function and ring confirms additivity over the reals.
Claim. For natural numbers $r, n_1, n_2$, the squared mass at rung $r$ and excitation $n_1 + n_2$ equals the sum of the squared masses at excitations $n_1$ and $n_2$, where the squared-mass function is $m^2(r,n,α') = n · α' · φ^{2r}$ and $α'$ is the PDG Regge slope.
background
The Hadrons module derives masses from composite rungs (quark rungs plus eight-beat binding) and encodes Regge trajectories as $m^2 = n α' φ^{2r}$ with universal slope. The definition regge_mass_squared(r, n, alpha_prime) returns exactly $n · alpha_prime · φ^{2r}$, while pdg_regge_slope supplies the numerical slope taken from the external PDG certificate. This construction sits inside Phase 6 scaffolding for hadron relations and remains outside Level A completion.
proof idea
The term proof first applies simp to unfold regge_mass_squared, exposing the explicit factor of n, then invokes ring to verify that the linear term distributes over addition of the two excitation indices.
why it matters
The result confirms the additive structure of Regge trajectories required by the phi-tier spacing model. It supplies the algebraic step that lets composite excitations be summed without extra terms, directly supporting the mass formulas in the same module. As Phase 6 scaffolding it touches the open question of how the universal slope emerges from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.