pith. machine review for the scientific record. sign in
theorem proved term proof

theta_zero_minimizes

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 133theorem theta_zero_minimizes :
 134    ∀ θ, thetaJCost 0 ≤ thetaJCost θ := by

proof body

Term-mode proof.

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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.