`entropy`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.InitialCondition
domain: Foundation
line: 115 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.InitialCondition on GitHub at line 115.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 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?"

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.