axionDarkMatter

formal source

 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
 135  intro θ
 136  unfold thetaJCost
 137  simp only [Real.cos_zero]
 138  linarith [Real.cos_le_one θ]
 139
 140/-! ## Why Not θ = π? -/
 141