Growth and uncomputability of plain Kolmogorov complexity

For every description method only finitely many objects have complexity below any given bound (eventually_natCast_le_ecomplexity), so the plain complexity K(x) of natural numbers under the universal description method tends to infinity (tendsto_complexity_universal). No computable unbounded function is a lower bound for K: such a function exceeds K at some argument (exists_complexity_universal_lt_of_computable), and hence at infinitely many (frequently_complexity_universal_lt_of_computable). In particular K is not computable (not_computable_complexity_universal). The proof is Berry's paradox: if f ≤ K were computable and unbounded, the program "the least x with f x ≥ 2 |q|", run on an input q, would describe a number of complexity at least 2 |q| by |q| + O(1) bits Li and Vitányi, Chapter 2.

The same invariance argument, applied to total computable decoders, shows that K(g p) ≤ |p| + O(1) for every computable g : List Bool → ℕ (exists_complexity_universal_le_length_add). Consequently K(x) ≤ log₂ x + O(1) (exists_complexity_universal_le_size_add), and computable maps increase K by at most a constant (exists_complexity_universal_comp_le).

The statements use the ℕ-valued complexity, which is the genuine plain complexity for the universal method (natCast_complexity_universal). The ℕ∞-valued complexity does not tend to ⊤ along the cofinite filter (not_tendsto_ecomplexity_universal), because it is never ⊤. Following the rest of the library, K denotes the plain complexity, which Li and Vitányi write C, reserving K for the prefix complexity.

Main results

• Cslib.Kolmogorov.DescriptionMethod.eventually_natCast_le_ecomplexity: all but finitely many objects have complexity at least k, for every description method.
• Cslib.Kolmogorov.DescriptionMethod.tendsto_complexity_universal: K(x) → ∞.
• Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_le_length_add: K(g p) ≤ |p| + O(1) for computable g.
• Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_le_size_add: K(x) ≤ log₂ x + O(1).
• Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_comp_le: K(f x) ≤ K(x) + O(1) for computable f.
• Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_lt_of_computable: no computable unbounded function is a lower bound for K.
• Cslib.Kolmogorov.DescriptionMethod.frequently_complexity_universal_lt_of_computable: a computable unbounded function exceeds K infinitely often.
• Cslib.Kolmogorov.DescriptionMethod.not_computable_complexity_universal: K is not computable.

References

• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications

Growth

theorem Cslib.Kolmogorov.DescriptionMethod.eventually_natCast_le_ecomplexity {α : Type u_1} (M : DescriptionMethod α) (k : ℕ) : ∀ᶠ (x : α) in Filter.cofinite, ↑k ≤ M.ecomplexity x

For every description method and every k, all but finitely many objects have complexity at least k: fewer than 2 ^ k objects have complexity below k.

theorem Cslib.Kolmogorov.DescriptionMethod.tendsto_complexity_universal : Filter.Tendsto universal.complexity Filter.atTop Filter.atTop

The plain complexity of natural numbers under the universal method tends to infinity.

theorem Cslib.Kolmogorov.DescriptionMethod.not_tendsto_ecomplexity_universal : ¬Filter.Tendsto universal.ecomplexity Filter.cofinite Filter.atTop

The ℕ∞-valued complexity under the universal method does not tend to ⊤, since it is never ⊤; this is why tendsto_complexity_universal is stated for the ℕ-valued complexity.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_le_complexity_universal (k : ℕ) : ∃ (x : ℕ), k ≤ universal.complexity x

Every bound is exceeded by the complexity of some natural number.

Upper bounds from computable decoders

theorem Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_le_length_add {g : List Bool → ℕ} (hg : Computable g) : ∃ (c : ℕ), ∀ (p : List Bool), universal.complexity (g p) ≤ p.length + c

Total computable decoders. If g is computable, the complexity of g p exceeds the length of p by at most a constant: the description method running g is partial recursive, and the universal method is at most a constant worse than it.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_le_size_add : ∃ (c : ℕ), ∀ (x : ℕ), universal.complexity x ≤ x.size + c

K(x) ≤ log₂ x + O(1): a number is described by its binary representation, of length Nat.size x.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_comp_le {f : ℕ → ℕ} (hf : Computable f) : ∃ (c : ℕ), ∀ (x : ℕ), universal.complexity (f x) ≤ universal.complexity x + c

Computable maps increase complexity by at most a constant: K(f x) ≤ K(x) + O(1) for every computable f. Composing f with the universal method is a partial recursive description method.

Uncomputability

theorem Cslib.Kolmogorov.DescriptionMethod.exists_complexity_universal_lt_of_computable {f : ℕ → ℕ} (hf : Computable f) (hunb : ∀ (k : ℕ), ∃ (x : ℕ), k ≤ f x) : ∃ (x : ℕ), universal.complexity x < f x

No computable unbounded lower bound. A computable unbounded function exceeds the plain complexity somewhere. Otherwise the search for the least x with f x ≥ 2 |q| would be a total computable decoder producing, from a program q of length c + 1, a number of complexity at least 2 (c + 1) but at most (c + 1) + c (Berry's paradox).

theorem Cslib.Kolmogorov.DescriptionMethod.frequently_complexity_universal_lt_of_computable {f : ℕ → ℕ} (hf : Computable f) (hunb : ∀ (k : ℕ), ∃ (x : ℕ), k ≤ f x) : ∃ᶠ (x : ℕ) in Filter.atTop, universal.complexity x < f x

A computable unbounded function exceeds the plain complexity at infinitely many arguments: beyond any N, apply exists_complexity_universal_lt_of_computable to the function that vanishes below N and agrees with f from N on.

theorem Cslib.Kolmogorov.DescriptionMethod.not_computable_complexity_universal : ¬Computable universal.complexity

The plain Kolmogorov complexity is not computable.