ReggeSlopeCertificate
plain-language theorem explainer
ReggeSlopeCertificate bundles a source string, Regge slope value α' in GeV^{-2}, its uncertainty, and a non-negativity constraint for explicit data provenance in hadron calculations. Physicists referencing external PDG inputs inside the Recognition Science hadron module cite this structure to anchor trajectory fits. The definition is a plain record type whose only content is the four fields with the embedded inequality.
Claim. A Regge slope certificate consists of a source string, a real number α' (in GeV^{-2}), an uncertainty Δα' (in GeV^{-2}), and the assertion 0 ≤ Δα'.
background
The Physics.Hadrons module derives hadron masses from composite rungs on the φ-ladder and states Regge trajectories as m² = n α' φ^{2r} with universal slope α' taken from residue. This structure supplies the external certificate seam that keeps slope provenance explicit, analogous to RG transport seams. The module marks the entire construction as Phase 6 scaffolding outside Level A completion.
proof idea
Structure definition that directly declares the four fields source, alphaPrime_GeV_inv2, uncertainty_GeV_inv2 and the field uncertainty_nonneg carrying the inequality 0 ≤ uncertainty_GeV_inv2.
why it matters
Supplies the type instantiated by pdg_regge_slope_cert, which hard-codes the placeholder α' = 0.9 GeV^{-2} with uncertainty 0.1. It supports the Regge linearity and regge_mass_squared relations inside the hadron module while preserving the universal slope required by φ-tier spacing. As Phase 6 scaffolding it leaves open the first-principles derivation of α' from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.