Documentation

def Cslib.Kolmogorov.DescriptionMethod.universalTMRunFor (p : List Bool) (t : ℕ) :

Option (List Bool)

Clocked evaluation of a binary program p for t steps of the described multi-tape machine: parses p into the machine description decodeDesc (unframe p) and the input string dropFrame p, simulates the described machine for t steps, and maps the output symbol numbers to bits via (· != 0).

Instances For

theorem Cslib.Kolmogorov.DescriptionMethod.mem_universalTMRunFor_iff {p x : List Bool} {t : ℕ} :

x ∈ universalTMRunFor p t ↔ ∃ (out : List ℕ), Turing.MultiTapeTM.Universal.simulate (Turing.MultiTapeTM.Universal.decodeDesc (Turing.MultiTapeTM.unframe p)) (List.map (⇑Turing.MultiTapeTM.Universal.eBit) (Turing.MultiTapeTM.dropFrame p)) t = (out, true ) ∧ List.map (fun (x : ℕ) => x != 0) out = x

Membership in universalTMRunFor p t unpacked via the underlying simulate output list.

theorem Cslib.Kolmogorov.DescriptionMethod.mem_universalTMRunFor_iff_simulate {p x : List Bool} {t : ℕ} :

Membership in universalTMRunFor p t expressed directly as projections of simulate.

theorem Cslib.Kolmogorov.DescriptionMethod.universalTMRunFor_mono (p : List Bool) {t₁ t₂ : ℕ} (ht : t₁ ≤ t₂) {x : List Bool} (h : x ∈ universalTMRunFor p t₁) :

x ∈ universalTMRunFor p t₂

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.universalTMRunFor_zero (p : List Bool) :

universalTMRunFor p 0 = none

Running universalTMRunFor for 0 steps always returns none.

def Cslib.Kolmogorov.DescriptionMethod.universalTM :

DescriptionMethod (List Bool)

The universal multi-tape Turing machine description method for binary strings (Liu and Pass, Section 2.2). A binary program p encodes the machine description decodeDesc (unframe p) and the input string dropFrame p. The clock counts steps of the described multi-tape machine, and the output is the global output tape contents upon halting.

Instances For

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.universalTM_runFor (p : List Bool) (t : ℕ) :

(universalTM.run p).runFor t = universalTMRunFor p t

(universalTM.run p).runFor t is universalTMRunFor p t.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_universalTM_zero (x : List Bool) :

universalTM.etimeBoundedComplexity 0 x = ⊤

At 0 steps, universalTM.etimeBoundedComplexity 0 x = ⊤.

Polynomial-time and partial-recursive evaluation of `universalTM` #

theorem Cslib.Kolmogorov.DescriptionMethod.computableInPolyTime_universalTMRunFor :

Turing.MultiTapeTM.ComputableInPolyTime (fun (pt : List Bool × ℕ) => universalTMRunFor pt.1 pt.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

Evaluating universalTMRunFor on a program and a unary step budget is computable in polynomial time.

Computable₂ universalTMRunFor

theorem Cslib.Kolmogorov.DescriptionMethod.computable_universalTMRunFor :

universalTMRunFor is computable in Mathlib's sense (Computable₂).

theorem Cslib.Kolmogorov.DescriptionMethod.isPartrec_universalTM_map {dec : List Bool → ℕ} (hdec : Computable dec) :

(map dec universalTM).IsPartrec

Mapping any computable decoder dec : List Bool → ℕ over universalTM yields a partial recursive description method.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universal_le_universalTM {dec : List Bool → ℕ} (hdec : Computable dec) :

∃ (c : ℕ), ∀ (x : List Bool), universal.ecomplexity (dec x) ≤ universalTM.ecomplexity x + ↑c

Partrec's universal description method universal is at most an additive constant worse than universalTM under any computable decoder dec : List Bool → ℕ.

Clock-preserving simulation of every binary `MultiTapeTM` #

theorem Cslib.Kolmogorov.DescriptionMethod.exists_simulation_ofMultiTapeTM {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) :

∃ (c : ℕ), Nonempty ((ofMultiTapeTM tm).Simulation universalTM c fun (x t : ℕ) => t)

Every finite-state binary MultiTapeTM is simulated by universalTM with constant program overhead and zero time overhead.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_ecomplexity_universalTM_le_ofMultiTapeTM {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) :

∃ (c : ℕ), ∀ (x : List Bool), universalTM.ecomplexity x ≤ (ofMultiTapeTM tm).ecomplexity x + ↑c

Plain Kolmogorov complexity under universalTM is at most an additive constant worse than under any finite-state binary MultiTapeTM.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_etimeBoundedComplexity_universalTM_le_ofMultiTapeTM {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) :

∃ (c : ℕ), ∀ (t : ℕ) (x : List Bool), universalTM.etimeBoundedComplexity t x ≤ (ofMultiTapeTM tm).etimeBoundedComplexity t x + ↑c

Clock-preserving time-bounded optimality of universalTM over MultiTapeTM: for every finite-state binary MultiTapeTM, universalTM is at most an additive constant worse at the exact same step count t.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_etimeBoundedComplexity_universalTM_le_ofSingleTapeTM (tm : Turing.SingleTapeTM Bool) :

∃ (c : ℕ), ∀ {t k : ℕ} {x : List Bool}, (ofSingleTapeTM tm).etimeBoundedComplexity t x ≤ ↑k → universalTM.etimeBoundedComplexity (3 * k + 2 * t + 6) x ≤ ↑(k + c)

Time-bounded complexity transfer from a single-tape Turing machine SingleTapeTM Bool to universalTM.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_simulation_literal_universalTM :

∃ (c : ℕ), Nonempty (literal.Simulation universalTM c fun (x t : ℕ) => t + 1)

universalTM simulates the literal description method with constant program overhead and one extra step (t + 1).

Plain and time-bounded Kolmogorov complexity (`plain`, `timeBoundedAt`, `timeBounded`) #

noncomputable def Cslib.Kolmogorov.plain (x : List Bool) :

Plain Kolmogorov complexity $K(x)$ of a binary string $x$ under universalTM, in ℕ∞.

Instances For

noncomputable def Cslib.Kolmogorov.plainNat (x : List Bool) :

Plain Kolmogorov complexity $K(x)$ of a binary string $x$ under universalTM, as a natural number. Since every string has a finite description (plain_ne_top), (plainNat x : ℕ∞) = plain x (natCast_plainNat).

Instances For

noncomputable def Cslib.Kolmogorov.timeBoundedAt (t : ℕ) (x : List Bool) :

Step-indexed time-bounded Kolmogorov complexity $K^t(x)$ of a binary string $x$ at a concrete step budget $t : \mathbb{N}$ (Ko; Liu and Pass, Section 2.2): the length of a shortest binary program that outputs $x$ within $t$ steps of the described multi-tape machine under universalTM, in ℕ∞.

Instances For

noncomputable def Cslib.Kolmogorov.timeBounded (t : ℕ → ℕ) (x : List Bool) :

Time-bounded Kolmogorov complexity $K^t(x)$ of a binary string $x$ with respect to the time bound $t : \mathbb{N} \to \mathbb{N}$ (Ko; Liu and Pass, Section 2.2): the length of a shortest binary program that outputs $x$ within $t(|x|)$ steps of the described multi-tape machine, in ℕ∞.

Instances For

@[simp]

theorem Cslib.Kolmogorov.timeBounded_eq_timeBoundedAt (t : ℕ → ℕ) (x : List Bool) :

timeBounded t x = timeBoundedAt (t x.length) x

timeBounded t x is timeBoundedAt (t x.length) x.

noncomputable def Cslib.Kolmogorov.timeBoundedNat (t : ℕ → ℕ) (x : List Bool) :

Time-bounded Kolmogorov complexity $K^t(x)$ as a natural number. Whenever a program outputs $x$ within $t(|x|)$ steps (timeBounded t x ≠ ⊤), (timeBoundedNat t x : ℕ∞) = timeBounded t x (natCast_timeBoundedNat).

Instances For

Equivalence bridges between `ℕ∞` and finite (`ℕ`) formulations #

@[simp]

theorem Cslib.Kolmogorov.timeBoundedAt_zero (x : List Bool) :

timeBoundedAt 0 x = ⊤

At 0 steps, timeBoundedAt 0 x = ⊤.

theorem Cslib.Kolmogorov.timeBoundedAt_le_natCast_iff {t : ℕ} {x : List Bool} {k : ℕ} :

timeBoundedAt t x ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor t

timeBoundedAt t x ≤ k iff some program of length at most k outputs x within t steps.

theorem Cslib.Kolmogorov.timeBoundedAt_lt_natCast_iff {t : ℕ} {x : List Bool} {k : ℕ} :

timeBoundedAt t x < ↑k ↔ ∃ (p : List Bool), p.length < k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor t

timeBoundedAt t x < k iff some program of length strictly less than k outputs x within t steps.

theorem Cslib.Kolmogorov.timeBoundedAt_eq_top_iff {t : ℕ} {x : List Bool} :

timeBoundedAt t x = ⊤ ↔ ∀ (p : List Bool), x ∉ (DescriptionMethod.universalTM.run p).runFor t

timeBoundedAt t x = ⊤ iff no program outputs x within t steps.

theorem Cslib.Kolmogorov.timeBoundedAt_ne_top_iff {t : ℕ} {x : List Bool} :

timeBoundedAt t x ≠ ⊤ ↔ ∃ (p : List Bool), x ∈ (DescriptionMethod.universalTM.run p).runFor t

timeBoundedAt t x ≠ ⊤ iff some program outputs x within t steps.

theorem Cslib.Kolmogorov.timeBounded_le_natCast_iff {t : ℕ → ℕ} {x : List Bool} {k : ℕ} :

timeBounded t x ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length)

timeBounded t x ≤ k iff some program of length at most k outputs x within t |x| steps.

theorem Cslib.Kolmogorov.timeBounded_lt_natCast_iff {t : ℕ → ℕ} {x : List Bool} {k : ℕ} :

timeBounded t x < ↑k ↔ ∃ (p : List Bool), p.length < k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length)

timeBounded t x < k iff some program of length strictly less than k outputs x within t |x| steps.

theorem Cslib.Kolmogorov.timeBounded_eq_top_iff {t : ℕ → ℕ} {x : List Bool} :

timeBounded t x = ⊤ ↔ ∀ (p : List Bool), x ∉ (DescriptionMethod.universalTM.run p).runFor (t x.length)

timeBounded t x = ⊤ iff no program outputs x within t |x| steps.

theorem Cslib.Kolmogorov.timeBounded_ne_top_iff {t : ℕ → ℕ} {x : List Bool} :

timeBounded t x ≠ ⊤ ↔ ∃ (p : List Bool), x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length)

timeBounded t x ≠ ⊤ iff some program outputs x within t |x| steps.

theorem Cslib.Kolmogorov.natCast_timeBoundedNat {t : ℕ → ℕ} {x : List Bool} (h : timeBounded t x ≠ ⊤) :

↑(timeBoundedNat t x) = timeBounded t x

Whenever timeBounded t x ≠ ⊤, the natural-number wrapper timeBoundedNat t x casts back to timeBounded t x.

theorem Cslib.Kolmogorov.timeBoundedNat_le_iff {t : ℕ → ℕ} {x : List Bool} {k : ℕ} (h : timeBounded t x ≠ ⊤) :

timeBoundedNat t x ≤ k ↔ timeBounded t x ≤ ↑k

Whenever timeBounded t x ≠ ⊤, the ℕ-valued inequality timeBoundedNat t x ≤ k is equivalent to timeBounded t x ≤ k.

theorem Cslib.Kolmogorov.exists_length_eq_timeBoundedNat {t : ℕ → ℕ} {x : List Bool} (h : timeBounded t x ≠ ⊤) :

∃ (p : List Bool), x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length) ∧ p.length = timeBoundedNat t x

Whenever timeBounded t x ≠ ⊤, timeBoundedNat t x is the exact length of a shortest program outputting x within t |x| steps.

theorem Cslib.Kolmogorov.timeBoundedNat_eq_sInf {t : ℕ → ℕ} {x : List Bool} (h : timeBounded t x ≠ ⊤) :

timeBoundedNat t x = sInf {k : ℕ | ∃ (p : List Bool), p.length = k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length)}

Whenever a witness program exists (timeBounded t x ≠ ⊤), timeBoundedNat t x equals the ℕ-infimum sInf {p.length | x ∈ (universalTM.run p).runFor (t x.length)}, matching the source definition $K^t(x) = \min\{|\Pi| : U(\Pi, 1^{t(|x|)}) = x\}$ in Liu and Pass, Section 2.2.

Basic properties of `K^t`: monotonicity, upper bound, and relation to plain `K` #

theorem Cslib.Kolmogorov.timeBoundedAt_antitone (x : List Bool) :

Antitone fun (x_1 : ℕ) => timeBoundedAt x_1 x

Antitonicity in the step bound. Giving more steps cannot increase timeBoundedAt t x.

theorem Cslib.Kolmogorov.timeBoundedAt_anti {t₁ t₂ : ℕ} {x : List Bool} (h : t₁ ≤ t₂) :

timeBoundedAt t₂ x ≤ timeBoundedAt t₁ x

If t₁ ≤ t₂, then timeBoundedAt t₂ x ≤ timeBoundedAt t₁ x.

theorem Cslib.Kolmogorov.timeBounded_antitone (x : List Bool) :

Antitone fun (x_1 : ℕ → ℕ) => timeBounded x_1 x

Antitonicity in the time function. More time cannot increase K^t(x).

theorem Cslib.Kolmogorov.timeBounded_anti_of_le {t₁ t₂ : ℕ → ℕ} {x : List Bool} (h : t₁ x.length ≤ t₂ x.length) :

timeBounded t₂ x ≤ timeBounded t₁ x

Monotonicity in the time bound at |x|. Giving more time at input length |x| cannot increase K^t(x).

theorem Cslib.Kolmogorov.timeBounded_anti {t₁ t₂ : ℕ → ℕ} (h : t₁ ≤ t₂) (x : List Bool) :

timeBounded t₂ x ≤ timeBounded t₁ x

Monotonicity in the time function. If t₁ ≤ t₂ pointwise, then K^{t₂}(x) ≤ K^{t₁}(x).

noncomputable def Cslib.Kolmogorov.copyOverhead :

The fixed program overhead of the identity machine simulating literal in universalTM.

Instances For

theorem Cslib.Kolmogorov.timeBoundedAt_le_length_add {t : ℕ} {x : List Bool} (ht : x.length + 1 ≤ t) :

timeBoundedAt t x ≤ ↑(x.length + copyOverhead)

Under universalTM, every string x can be printed by a program of length at most |x| + copyOverhead within |x| + 1 steps.

theorem Cslib.Kolmogorov.timeBounded_le_length_add {t : ℕ → ℕ} {x : List Bool} (ht : x.length + 1 ≤ t x.length) :

timeBounded t x ≤ ↑(x.length + copyOverhead)

Trivial upper bound (Liu and Pass, Fact 2.1 under multi-tape global output): if $t(|x|) \ge |x| + 1$, then $K^t(x) \le |x| + \mathrm{copyOverhead}$.

theorem Cslib.Kolmogorov.timeBounded_le {t : ℕ → ℕ} (ht : ∀ (n : ℕ), n + 1 ≤ t n) (x : List Bool) :

timeBounded t x ≤ ↑(x.length + copyOverhead)

Trivial upper bound for all inputs (Liu and Pass, Fact 2.1): if $t(n) \ge n + 1$ for all $n$, then $K^t(x) \le |x| + \mathrm{copyOverhead}$ for all $x$.

theorem Cslib.Kolmogorov.exists_timeBounded_le :

∃ (c : ℕ), ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), n + 1 ≤ t n) → ∀ (x : List Bool), timeBounded t x ≤ ↑(x.length + c)

Existential form of the trivial upper bound $K^t(x) \le |x| + O(1)$ for $t(n) \ge n + 1$.

theorem Cslib.Kolmogorov.timeBounded_ne_top {t : ℕ → ℕ} {x : List Bool} (ht : x.length + 1 ≤ t x.length) :

timeBounded t x ≠ ⊤

If x.length + 1 ≤ t x.length, then timeBounded t x ≠ ⊤.

theorem Cslib.Kolmogorov.timeBoundedNat_le_length_add {t : ℕ → ℕ} {x : List Bool} (ht : x.length + 1 ≤ t x.length) :

timeBoundedNat t x ≤ x.length + copyOverhead

Natural-number upper bound timeBoundedNat t x ≤ x.length + copyOverhead when x.length + 1 ≤ t x.length.

theorem Cslib.Kolmogorov.plain_le_timeBoundedAt (t : ℕ) (x : List Bool) :

plain x ≤ timeBoundedAt t x

Relation to plain complexity (K(x) ≤ K^t(x) at step budget t). Dropping the step bound cannot increase Kolmogorov complexity under universalTM.

theorem Cslib.Kolmogorov.plain_le_timeBounded (t : ℕ → ℕ) (x : List Bool) :

plain x ≤ timeBounded t x

Relation to plain complexity (K(x) ≤ K^t(x)). Dropping the time bound cannot increase Kolmogorov complexity under universalTM.

theorem Cslib.Kolmogorov.plain_le_length_add (x : List Bool) :

plain x ≤ ↑(x.length + copyOverhead)

Trivial upper bound plain x ≤ x.length + copyOverhead for plain complexity.

theorem Cslib.Kolmogorov.plain_ne_top (x : List Bool) :

plain x ≠ ⊤

Plain Kolmogorov complexity plain x is always finite.

@[simp]

theorem Cslib.Kolmogorov.natCast_plainNat (x : List Bool) :

↑(plainNat x) = plain x

Casting plainNat x to ℕ∞ yields plain x.

theorem Cslib.Kolmogorov.plainNat_le_timeBoundedNat {t : ℕ → ℕ} {x : List Bool} (h : timeBounded t x ≠ ⊤) :

plainNat x ≤ timeBoundedNat t x

Whenever timeBounded t x ≠ ⊤, plainNat x ≤ timeBoundedNat t x.

theorem Cslib.Kolmogorov.iInf_timeBoundedAt (x : List Bool) :

⨅ (t : ℕ), timeBoundedAt t x = plain x

Plain complexity plain x is the infimum of timeBoundedAt t x over all step bounds t : ℕ.

theorem Cslib.Kolmogorov.exists_ecomplexity_universal_le_timeBounded {dec : List Bool → ℕ} (hdec : Computable dec) :

∃ (c : ℕ), ∀ (t : ℕ → ℕ) (x : List Bool), DescriptionMethod.universal.ecomplexity (dec x) ≤ timeBounded t x + ↑c

Relation to Partrec.universal (K_U(dec x) ≤ K^t(x) + O(1)). For any computable decoder dec : List Bool → ℕ, the plain complexity of dec x under DescriptionMethod.universal (Partrec.lean) is at most timeBounded t x + c.

theorem Cslib.Kolmogorov.exists_ecomplexity_universal_le_timeBounded_bits :

∃ (c : ℕ), ∀ (t : ℕ → ℕ) (n : ℕ), DescriptionMethod.universal.ecomplexity n ≤ timeBounded t n.bits + ↑c

Using Nat.bits and List.foldr Nat.bit 0, universal.ecomplexity n ≤ timeBounded t n.bits + c for all t and n.

Counting and incompressibility facts for `K^t` #

theorem Cslib.Kolmogorov.encard_setOf_timeBounded_lt (t : ℕ → ℕ) (n r : ℕ) :

{x : List Bool | x.length = n ∧ timeBounded t x < ↑r}.encard < 2 ^ r

Fewer than $2^r$ strings of length $n$ have $K^t(x) < r$.

theorem Cslib.Kolmogorov.exists_length_eq_forall_le_timeBounded (n : ℕ) :

∃ (x : List Bool), x.length = n ∧ ∀ (t : ℕ → ℕ), ↑n ≤ timeBounded t x

Existence of $K^t$-incompressible strings. For every $n$ and every time bound $t$, some string $x \in \{0, 1\}^n$ has $K^t(x) \ge n$ (in fact, a single string works for all $t$ simultaneously).

theorem Cslib.Kolmogorov.exists_length_eq_le_timeBounded (t : ℕ → ℕ) (n : ℕ) :

∃ (x : List Bool), x.length = n ∧ ↑n ≤ timeBounded t x

For every time bound t and length n, there exists a string x of length n with n ≤ timeBounded t x.

theorem Cslib.Kolmogorov.two_pow_lt_ncard_setOf_length_eq_le_timeBounded_add (t : ℕ → ℕ) (n c : ℕ) :

2 ^ n < {x : List Bool | x.length = n ∧ ↑(n - c) ≤ timeBounded t x}.ncard + 2 ^ (n - c)

Counting nearly $K^t$-incompressible strings. All but fewer than $2^{n - c}$ of the $2^n$ strings of length $n$ satisfy $K^t(x) \ge n - c$.

Levin's time-bounded Kolmogorov complexity (`Kt`) #

noncomputable def Cslib.Kolmogorov.levinKt (x : List Bool) :

Levin's time-bounded Kolmogorov complexity $\mathrm{Kt}(x)$ (Levin; Levin; Allender et al.; Liu and Pass, Section 2.2): $$\mathrm{Kt}(x) = \inf_{s \in \mathbb{N}} \bigl(K^s(x) + \lceil \log_2 s \rceil\bigr).$$ Because timeBoundedAt 0 x = ⊤ (timeBoundedAt_zero), the $s = 0$ term is $\top$ and the infimum over $s : \mathbb{N}$ coincides with the infimum over $s \ge 1$. Here $s$ counts steps of the described multi-tape machine (universalTM); relative to a fixed universal simulator with polynomial step overhead (Universal.universal), this changes the $\lceil \log_2 s \rceil$ term by a constant factor rather than an $O(1)$ additive term.

Instances For

noncomputable def Cslib.Kolmogorov.levinKtNat (x : List Bool) :

Levin's $\mathrm{Kt}(x)$ as a natural number.

Instances For

theorem Cslib.Kolmogorov.levinKt_eq_iInf_pos (x : List Bool) :

levinKt x = ⨅ (s : ℕ), ⨅ (_ : 0 < s), timeBoundedAt s x + ↑(Nat.clog 2 s)

Restricting the infimum in levinKt to positive step counts $s > 0$ gives the exact same value, since no program halts in $0$ steps (timeBoundedAt_zero).

theorem Cslib.Kolmogorov.levinKt_le_timeBoundedAt_add (s : ℕ) (x : List Bool) :

levinKt x ≤ timeBoundedAt s x + ↑(Nat.clog 2 s)

For every step count s, levinKt x ≤ timeBoundedAt s x + Nat.clog 2 s.

theorem Cslib.Kolmogorov.levinKt_le_timeBounded_add (t : ℕ → ℕ) (x : List Bool) :

levinKt x ≤ timeBounded t x + ↑(Nat.clog 2 (t x.length))

For every time bound t : ℕ → ℕ, levinKt x ≤ timeBounded t x + Nat.clog 2 (t x.length).

theorem Cslib.Kolmogorov.plain_le_levinKt (x : List Bool) :

plain x ≤ levinKt x

Plain complexity bounds Levin's Kt from below (K(x) ≤ Kt(x)).

theorem Cslib.Kolmogorov.levinKt_le_length_add (x : List Bool) :

levinKt x ≤ ↑(x.length + copyOverhead + Nat.clog 2 (x.length + 1))

Trivial upper bound for Levin's Kt: $\mathrm{Kt}(x) \le |x| + \mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil$.

theorem Cslib.Kolmogorov.levinKt_ne_top (x : List Bool) :

levinKt x ≠ ⊤

Levin's levinKt x is always finite.

@[simp]

theorem Cslib.Kolmogorov.natCast_levinKtNat (x : List Bool) :

↑(levinKtNat x) = levinKt x

Casting levinKtNat x to ℕ∞ yields levinKt x.

theorem Cslib.Kolmogorov.levinKt_le_natCast_iff {x : List Bool} {k : ℕ} :

levinKt x ≤ ↑k ↔ ∃ (p : List Bool) (s : ℕ), x ∈ (DescriptionMethod.universalTM.run p).runFor s ∧ p.length + Nat.clog 2 s ≤ k

Threshold characterization of levinKt. $\mathrm{Kt}(x) \le k$ iff some program $p$ outputs $x$ within $s$ steps with $|p| + \lceil \log_2 s \rceil \le k$.