pdg_regge_slope_cert
plain-language theorem explainer
pdg_regge_slope_cert supplies a placeholder certificate for the Regge slope in hadron physics calculations. Researchers computing Regge trajectories within the Recognition Science framework cite this value when extracting the slope for mass formulas. The definition builds the certificate by assigning the source string, slope of 0.9 GeV inverse squared, uncertainty of 0.1, and verifies non-negativity of the uncertainty using the norm_num tactic.
Claim. The external Regge slope certificate consists of the source string ``PDG display placeholder'', the slope parameter $0.9$ in units of GeV$^{-2}$, the uncertainty $0.1$ GeV$^{-2}$, and the assertion that the uncertainty is nonnegative.
background
The Physics.Hadrons module derives hadron masses from composite rungs on the phi-ladder and Regge trajectories of the form $m^2 = n α' φ^{2r}$, with the slope $α'$ taken from residue. The ReggeSlopeCertificate structure serves as an external seam for reporting the slope value, keeping its provenance explicit in a manner analogous to RG transport seams. This setup belongs to Phase 6 scaffolding and lies outside the scope of Level A completion for the framework. Upstream, the ReggeSlopeCertificate is defined with fields for source, alphaPrime_GeV_inv2, uncertainty_GeV_inv2, and the nonnegativity condition on uncertainty.
proof idea
The definition constructs an instance of the ReggeSlopeCertificate structure through direct field initialization. It populates the source with the PDG placeholder, sets the slope to 0.9 and uncertainty to 0.1, then applies the norm_num tactic to establish that the uncertainty satisfies the nonnegativity requirement.
why it matters
This certificate is consumed by the pdg_regge_slope definition to extract the numerical slope for structural trajectory formulas and by the regge_mass_squared_nonneg theorem to prove nonnegativity of the resulting mass squared. It provides the external data input for Regge slopes in the hadron mass relations based on φ-tier spacing. As part of Phase 6 scaffolding, it leaves open the integration of precise PDG values with the Recognition Science constants such as the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.