thetaContributions

formal source

  80    θ is the sum of:
  81    - Bare QCD θ
  82    - Contribution from quark masses (arg det M) -/
  83def thetaContributions : List String := [
  84  "Bare QCD theta",
  85  "Quark mass phase: arg det M_q",
  86  "Total: θ_eff = θ_QCD + arg det M_q"
  87]
  88
  89/-! ## The Axion Solution -/
  90
  91/-- The Peccei-Quinn (PQ) solution:
  92
  93    Introduce a new U(1)_PQ symmetry.
  94    When broken, a Goldstone boson (axion) appears.
  95    The axion field dynamically relaxes θ → 0.
  96
  97    Axion mass: m_a ~ f_π m_π / f_a
  98    where f_a is the PQ breaking scale. -/
  99structure AxionSolution where
 100  pq_scale : ℝ  -- f_a, typically 10⁹-10¹² GeV
 101  axion_mass : ℝ  -- Typically 10⁻⁶-10⁻³ eV
 102  couples_to : List String
 103
 104def axionProperties : AxionSolution := {
 105  pq_scale := 1e10,  -- GeV
 106  axion_mass := 1e-5,  -- eV
 107  couples_to := ["photons", "nucleons", "electrons"]
 108}
 109
 110/-- Axions are also a dark matter candidate! -/
 111def axionDarkMatter : String :=
 112  "If f_a ~ 10¹² GeV, axions can be all of dark matter"
 113