regge_mass_squared
regge_mass_squared supplies the explicit formula for squared hadron masses along Regge trajectories in the Recognition Science model. Particle physicists modeling meson and baryon spectra would cite this when fitting experimental data to phi-scaled ladders. The definition is a direct algebraic expression multiplying the principal quantum number n by the slope parameter and the squared phi-power of the composite rung index r.
claim$m^2(r,n) = n · α' · φ^{2r}$ where r and n are natural numbers indexing the rung and excitation level on the phi-ladder, and α' is the externally supplied Regge slope.
background
In the Physics.Hadrons module, hadron masses arise from composite rungs (quark1.rung + quark2.rung plus eight-beat binding) and relations such as ρ/ω degeneracy at equal Z. The phi-ladder denotes exponential spacing by powers of the golden ratio φ, the self-similar fixed point forced by the Recognition Composition Law. Constants is the abstract bundle of CPM constants that includes the positive real φ used for scaling.
proof idea
The definition is a one-line algebraic expression that casts n to real, multiplies by alpha_prime, and scales by Constants.phi raised to twice the rung r.
why it matters in Recognition Science
This definition is invoked by regge_linearity to prove additivity of squared masses and by regge_mass_squared_nonneg to establish non-negativity. It implements the Regge trajectory m² = n α' φ^{2r} inside the module's derivation of hadron masses from φ-tier spacing, linking to the phi fixed point (T6) and eight-tick octave in the forcing chain. The module marks the entire construction as Phase 6 scaffolding.
scope and limits
- Does not derive the numerical value of the Regge slope alpha_prime from first principles.
- Does not incorporate explicit quark masses or binding energies.
- Does not address spin, isospin, or full particle classification.
- Does not prove convergence of the trajectory for large n.
formal statement (Lean)
35noncomputable def regge_mass_squared (r n : ℕ) (alpha_prime : ℝ) : ℝ :=
proof body
Definition body.
36 (n : ℝ) * alpha_prime * (Constants.phi ^ (2 * (r : ℝ)))
37
38/-- External certificate seam for Regge slope reporting.
39This keeps hadron slope provenance explicit (analogous to RG transport seams). -/