axionProperties

formal source

 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
 114/-! ## RS Solution: 8-Tick Quantization -/
 115
 116/-- In RS, θ is quantized by 8-tick symmetry:
 117
 118    The allowed values are: θ = 2πk/8 = πk/4 for k ∈ {0,1,...,7}
 119
 120    This gives only 8 allowed values:
 121    0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4 -/
 122noncomputable def allowedTheta : List ℝ := [0, π/4, π/2, 3*π/4, π, 5*π/4, 3*π/2, 7*π/4]
 123
 124/-- J-cost of each θ value:
 125
 126    θ = 0 and θ = π have lowest J-cost (CP-conserving).
 127    Other values have higher J-cost.
 128
 129    J-cost selection: θ = 0 is preferred. -/
 130noncomputable def thetaJCost (θ : ℝ) : ℝ :=
 131  (1 - Real.cos θ)  -- Minimum at θ = 0
 132
 133theorem theta_zero_minimizes :
 134    ∀ θ, thetaJCost 0 ≤ thetaJCost θ := by