unity_is_global_minimum

formal source

  96    exact LawOfExistence.defect_one
  97
  98/-- **Theorem**: The unity configuration achieves the global minimum of total defect. -/
  99theorem unity_is_global_minimum {N : ℕ} (hN : 0 < N) (c : Configuration N) :
 100    total_defect (unity_config N hN) ≤ total_defect c := by
 101  rw [unity_defect_zero hN]
 102  exact total_defect_nonneg c
 103
 104/-- **Theorem**: The unity configuration is the UNIQUE global minimizer. -/
 105theorem unity_unique_minimizer {N : ℕ} (hN : 0 < N) (c : Configuration N) :
 106    total_defect c = total_defect (unity_config N hN) →
 107    ∀ i, c.entries i = 1 := by
 108  rw [unity_defect_zero hN]
 109  exact (zero_defect_iff_unity hN c).mp
 110
 111/-! ## Entropy and Defect -/
 112
 113/-- Entropy of a configuration is proportional to its total defect.
 114    Zero defect = zero entropy = minimum entropy state. -/
 115noncomputable def entropy {N : ℕ} (c : Configuration N) : ℝ :=
 116  total_defect c
 117
 118/-- **Theorem**: The initial state has minimum entropy. -/
 119theorem initial_state_minimum_entropy {N : ℕ} (hN : 0 < N) :
 120    entropy (unity_config N hN) = 0 := unity_defect_zero hN
 121
 122/-- **Theorem**: Any non-unity state has positive entropy. -/
 123theorem nonunity_positive_entropy {N : ℕ} (_hN : 0 < N) (c : Configuration N)
 124    (h : ∃ i, c.entries i ≠ 1) : 0 < entropy c := by
 125  obtain ⟨j, hj⟩ := h
 126  have hj_pos : 0 < LawOfExistence.defect (c.entries j) :=
 127    LawOfExistence.defect_pos_of_ne_one (c.entries_pos j) hj
 128  calc 0 < LawOfExistence.defect (c.entries j) := hj_pos
 129    _ ≤ ∑ i : Fin N, LawOfExistence.defect (c.entries i) := by