regge_mass_squared

formal source

  32  Constants.E_coh * (Constants.phi ^ (composite_rung h : ℝ))
  33
  34-- Regge trajectory: excited states n=0,1,2,... m_n^2 = n α' φ^{2 r} (r=base rung)
  35noncomputable def regge_mass_squared (r n : ℕ) (alpha_prime : ℝ) : ℝ :=
  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). -/
  40structure ReggeSlopeCertificate where
  41  source : String
  42  alphaPrime_GeV_inv2 : ℝ
  43  uncertainty_GeV_inv2 : ℝ
  44  uncertainty_nonneg : 0 ≤ uncertainty_GeV_inv2
  45
  46/-- Current external Regge slope placeholder (PDG-facing convention). -/
  47def pdg_regge_slope_cert : ReggeSlopeCertificate where
  48  source := "PDG display placeholder"
  49  alphaPrime_GeV_inv2 := 0.9
  50  uncertainty_GeV_inv2 := 0.1
  51  uncertainty_nonneg := by norm_num
  52
  53/-- Regge slope value consumed by the structural trajectory formulas. -/
  54@[simp] def pdg_regge_slope : ℝ := pdg_regge_slope_cert.alphaPrime_GeV_inv2
  55
  56/-- Equal-Z hadrons are degenerate at leading order. -/
  57theorem hadron_equal_z_degenerate (h1 h2 : Hadron)
  58  (h_same_rung : composite_rung h1 = composite_rung h2) :
  59  hadron_mass h1 = hadron_mass h2 := by
  60  simp [hadron_mass, h_same_rung]
  61
  62/-- Regge mass squared is non-negative. -/
  63theorem regge_mass_squared_nonneg (r n : ℕ) : regge_mass_squared r n pdg_regge_slope ≥ 0 := by
  64  have hphi_pow_nonneg : 0 ≤ Constants.phi ^ (2 * (r : ℝ)) :=
  65    le_of_lt (Real.rpow_pos_of_pos Constants.phi_pos _)