regge_mass_squared_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the squared mass on Regge trajectories for hadrons, expressed as m² = n α' φ^{2r} where α' is the PDG slope and φ the golden ratio. Hadron spectroscopists would cite it when checking consistency of the φ-ladder mass formula against experimental trajectories. The proof proceeds by separate non-negativity arguments on n, α', and φ^{2r} followed by two applications of multiplication preservation and algebraic simplification.
Claim. For all natural numbers $r$ and $n$, the expression $n · α' · φ^{2r} ≥ 0$, where $α'$ denotes the PDG Regge slope and $φ$ the golden ratio.
background
The module derives hadron masses from composite rungs (quark1.rung + quark2.rung + binding from eight-beat) and Regge trajectories of the form m² = n α' φ^{2r} with universal slope. Constants is the abstract bundle containing Knet, Cproj, Ceng, Cdisp and the golden ratio φ. The upstream zero_le supplies non-negativity for natural numbers in the underlying arithmetic. The local setting is Phase 6 scaffolding for hadron spectroscopy, explicitly outside Level A completion.
proof idea
The tactic proof first obtains 0 ≤ φ^{2r} from Real.rpow_pos_of_pos applied to Constants.phi_pos. It obtains 0 ≤ α' by norm_num on pdg_regge_slope and its certificate. It obtains 0 ≤ n by casting Nat.zero_le. Two successive mul_nonneg steps combine the factors, after which simpa rewrites using the definition of regge_mass_squared together with commutativity and associativity of multiplication.
why it matters
The result supplies a basic positivity check for the Regge trajectory formula inside the φ-tier spacing relations for hadrons. It supports the module's claim that the slope is universal and the mass formula remains non-negative on the ladder. No downstream theorems yet reference it; the declaration closes a scaffolding gap in the hadron mass relations before further linearity or degeneracy statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.