allowedTheta

formal source

 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
 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. -/