Hadron

formal source

  20namespace Physics
  21
  22/-- Simple hadrons as quark pairs (e.g., meson = up-bar down). -/
  23structure Hadron where
  24  q1 : RSBridge.Fermion
  25  q2 : RSBridge.Fermion
  26  binding : ℤ := 1
  27
  28noncomputable def composite_rung (h : Hadron) : ℤ :=
  29  RSBridge.rung h.1 + (- RSBridge.rung h.2) + h.3
  30
  31noncomputable def hadron_mass (h : Hadron) : ℝ :=
  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. -/