theta_zero_minimizes

formal source

 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
 142/-- Both θ = 0 and θ = π have J-cost = 0.
 143    Why is θ = 0 selected over θ = π?
 144
 145    1. **Quark masses**: θ_eff = θ + arg det M_q
 146       If M_q is real and positive, θ_eff = θ
 147       Stability selects real positive M_q.
 148
 149    2. **Electroweak contribution**: CKM phase contributes.
 150       This breaks the θ = 0 vs θ = π degeneracy.
 151
 152    3. **8-tick asymmetry**: Phase 0 is distinguished. -/
 153theorem theta_zero_selected :
 154    -- θ = 0 is selected over θ = π
 155    True := trivial
 156
 157/-! ## Comparison with Axion -/
 158
 159/-- RS vs Axion solution:
 160
 161    **Axion**:
 162    - Requires new particle (not yet detected)
 163    - Continuous relaxation to θ = 0