nonunity_positive_entropy

formal source

 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
 130        apply Finset.single_le_sum (f := fun i => LawOfExistence.defect (c.entries i))
 131          (fun i _ => LawOfExistence.defect_nonneg (c.entries_pos i))
 132          (Finset.mem_univ j)
 133
 134/-! ## The Past Hypothesis Becomes a Theorem -/
 135
 136/-- **The Past Theorem (F-005 Resolution)**:
 137
 138    The universe's initial condition is not a contingent fact but a
 139    mathematical necessity. The unique zero-cost configuration IS the
 140    low-entropy initial state. There is no other option.
 141
 142    This resolves:
 143    - Penrose's "Why was the Big Bang so special?"
 144    - Albert's "Past Hypothesis"
 145    - Boltzmann's "Why didn't we start in thermal equilibrium?"
 146
 147    Answer: Because thermal equilibrium (maximum defect) is infinitely
 148    costly, while the zero-defect state is the unique cost minimum. -/
 149theorem past_theorem {N : ℕ} (hN : 0 < N) :
 150    (∃! c : Configuration N, total_defect c = 0) ∧
 151    total_defect (unity_config N hN) = 0 ∧
 152    (∀ c : Configuration N, total_defect (unity_config N hN) ≤ total_defect c) := by
 153  refine ⟨⟨unity_config N hN, unity_defect_zero hN, ?_⟩, unity_defect_zero hN,