pdg_regge_slope
plain-language theorem explainer
The definition supplies the numerical Regge slope α' = 0.9 GeV^{-2} taken from external PDG data for insertion into the Recognition Science hadron mass formulas. Researchers modeling meson and baryon trajectories within the φ-ladder framework would reference this constant when verifying linearity or non-negativity of m²(n). It is realized as a one-line extraction from the certified placeholder record.
Claim. The Regge slope parameter is given by $α' = 0.9$ GeV$^{-2}$.
background
This module develops hadron mass relations using composite rungs on the φ-ladder and Regge trajectories of the form m² = n α' φ^{2r}. The anchor Z maps sectors to integers via quadratic and quartic terms in the charge fraction Q6. The upstream certificate supplies the placeholder value 0.9 with uncertainty 0.1, sourced as a PDG display placeholder. Local setting is Phase 6 scaffolding for hadron phenomenology, out of scope for Level A completion.
proof idea
The definition is a one-line wrapper that projects the alphaPrime_GeV_inv2 field from the ReggeSlopeCertificate record.
why it matters
This constant feeds the theorems regge_linearity and regge_mass_squared_nonneg, which establish linearity in the excitation number n and non-negativity of the mass squared. It implements the universal slope in the Regge trajectory formula m² = n α' φ^{2r} described in the module documentation. The declaration touches the open question of deriving α' from the Recognition Composition Law or the eight-tick octave rather than external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.