Conditional Time-Bounded Kolmogorov Complexity (K(x | y), K^t(x | y), and Kt(x | y))

This module defines the conditional universal multi-tape Turing machine description method Cslib.Kolmogorov.DescriptionMethod.condUniversalTM (a conditional description method List Bool → DescriptionMethod (List Bool) in the sense of Complexity.Computability.Kolmogorov.ChainRule) and the associated conditional plain, time-bounded, and Levin Kolmogorov complexities:

• Cslib.Kolmogorov.condPlain ($K(x \mid y)$) and Cslib.Kolmogorov.condPlainNat,
• Cslib.Kolmogorov.condTimeBoundedAt ($K^t(x \mid y)$, the conditional analogue of Hirahara, Definition 7), Cslib.Kolmogorov.condTimeBounded, and Cslib.Kolmogorov.condTimeBoundedNat, and
• Cslib.Kolmogorov.condLevinKt ($\mathrm{Kt}(x \mid y)$, the conditional analogue of Allender et al., Definition 1) and Cslib.Kolmogorov.condLevinKtNat.

Modeling conventions

• Conditioning via universalTM on paired inputs: Given an auxiliary (condition) string y : List Bool, a binary program p : List Bool is parsed into its machine description unframe p and program argument dropFrame p, and executed under universalTM on the re-framed program frame (unframe p) ++ encPair encBits encBits (dropFrame p, y). By unframe_frame_append and dropFrame_frame_append, at step budget t this runs the described multi-tape machine decodeDesc (unframe p) on the paired input encPair encBits encBits (dropFrame p, y) for t steps of the described machine (the conditional analogue of the unconditional universalTM clock convention in Complexity.Computability.Kolmogorov.TimeBounded).
• Reuse of universalTM and DescriptionMethod: Because condUniversalTM y is a DescriptionMethod (List Bool) defined directly from universalTM.run, it is a conditional description method in the sense of Complexity.Computability.Kolmogorov.ChainRule and inherits step monotonicity from universalTM, polynomial-time evaluation from computableInPolyTime_universalTMRunFor, and counting / incompressibility bounds for every fixed condition y from Cslib.Kolmogorov.DescriptionMethod (Complexity.Computability.Kolmogorov.Incompressibility).

Main definitions

• Cslib.Kolmogorov.DescriptionMethod.condUniversalTMProgram, Cslib.Kolmogorov.DescriptionMethod.condUniversalTMRunFor, Cslib.Kolmogorov.DescriptionMethod.condUniversalTM: the conditional universal multi-tape description method for condition string y.
• Cslib.Kolmogorov.condPlain, Cslib.Kolmogorov.condPlainNat: conditional plain Kolmogorov complexity $K(x \mid y)$ in ℕ∞ and ℕ.
• Cslib.Kolmogorov.condTimeBoundedAt, Cslib.Kolmogorov.condTimeBounded, Cslib.Kolmogorov.condTimeBoundedNat: step-indexed and function-indexed conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ in ℕ∞ and ℕ.
• Cslib.Kolmogorov.condLevinKt, Cslib.Kolmogorov.condLevinKtNat: conditional Levin complexity $\mathrm{Kt}(x \mid y)$ in ℕ∞ and ℕ.

Main results

• Cslib.Kolmogorov.DescriptionMethod.computableInPolyTime_condUniversalTMRunFor: polynomial-time evaluation of condUniversalTMRunFor.
• DescriptionMethod.exists_etimeBoundedComplexity_condUniversalTM_le_ofMultiTapeTM: clock-preserving conditional simulation of every finite-state binary MultiTapeTM operating on encPair encBits encBits (w, y).
• Cslib.Kolmogorov.exists_condTimeBoundedAt_le_of_computableInPolyTime: for any polynomial-time F : List Bool × List Bool → List Bool, $K^t(F(w, y) \mid y) \le |w| + O(1)$ at polynomial time.
• Cslib.Kolmogorov.exists_condTimeBoundedAt_apply_le, Cslib.Kolmogorov.exists_condTimeBoundedAt_self_le: $K^t(f(y) \mid y) \le O(1)$ and $K^t(y \mid y) \le O(1)$ for polynomial-time $f$.
• Cslib.Kolmogorov.exists_condTimeBoundedAt_le_length_add, Cslib.Kolmogorov.condPlain_ne_top, Cslib.Kolmogorov.condLevinKt_ne_top: $K^t(x \mid y) \le |x| + O(1)$ and finiteness of condPlain and condLevinKt.
• Cslib.Kolmogorov.encard_setOf_condTimeBoundedAt_lt, Cslib.Kolmogorov.exists_length_eq_forall_le_condTimeBoundedAt, Cslib.Kolmogorov.two_pow_lt_ncard_setOf_length_eq_le_condTimeBounded_add: counting and incompressibility for $K^t(\cdot \mid y)$ at any fixed condition $y$.

References

• E. Allender, H. Buhrman, M. Koucký, D. van Melkebeek, D. Ronneburger, Power from Random Strings
• S. Hirahara, Non-Black-Box Worst-Case to Average-Case Reductions within NP
• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications

The conditional universal multi-tape description method (condUniversalTM)

def Cslib.Kolmogorov.DescriptionMethod.condUniversalTMProgram (p y : List Bool) : List Bool

Re-frames a conditional program p with the auxiliary condition string y into a program for universalTM whose machine description is unframe p and whose input is encPair encBits encBits (dropFrame p, y).

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.unframe_condUniversalTMProgram (p y : List Bool) : Turing.MultiTapeTM.unframe (condUniversalTMProgram p y) = Turing.MultiTapeTM.unframe p

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.dropFrame_condUniversalTMProgram (p y : List Bool) : Turing.MultiTapeTM.dropFrame (condUniversalTMProgram p y) = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.dropFrame p, y)

def Cslib.Kolmogorov.DescriptionMethod.condUniversalTMRunFor (p y : List Bool) (t : ℕ) : Option (List Bool)

Clocked evaluation of a binary program p given condition string y for t steps of the described multi-tape machine.

def Cslib.Kolmogorov.DescriptionMethod.condUniversalTM (y : List Bool) : DescriptionMethod (List Bool)

The conditional universal multi-tape Turing machine description method for binary strings, conditioned on y : List Bool (a conditional description method in the sense of Complexity.Computability.Kolmogorov.ChainRule, and the conditional analogue of universalTM in Complexity.Computability.Kolmogorov.TimeBounded / Hirahara, Definition 7).

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.condUniversalTM_runFor (y p : List Bool) (t : ℕ) : ((condUniversalTM y).run p).runFor t = condUniversalTMRunFor p y t

((condUniversalTM y).run p).runFor t is condUniversalTMRunFor p y t.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.condUniversalTMRunFor_zero (p y : List Bool) : condUniversalTMRunFor p y 0 = none

Running condUniversalTMRunFor for 0 steps always returns none.

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

Step monotonicity of condUniversalTMRunFor.

@[simp]

theorem Cslib.Kolmogorov.DescriptionMethod.etimeBoundedComplexity_condUniversalTM_zero (y x : List Bool) : (condUniversalTM y).etimeBoundedComplexity 0 x = ⊤

At 0 steps, (condUniversalTM y).etimeBoundedComplexity 0 x = ⊤.

theorem Cslib.Kolmogorov.DescriptionMethod.computableInPolyTime_condUniversalTMProgram : Turing.MultiTapeTM.ComputableInPolyTime (fun (py : List Bool × List Bool) => condUniversalTMProgram py.1 py.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

condUniversalTMProgram is computable in polynomial time.

theorem Cslib.Kolmogorov.DescriptionMethod.computableInPolyTime_condUniversalTMRunFor : Turing.MultiTapeTM.ComputableInPolyTime (fun (pyt : List Bool × List Bool × ℕ) => condUniversalTMRunFor pyt.1 pyt.2.1 pyt.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary)) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBits)

Evaluating condUniversalTMRunFor on (p, (y, t)) is computable in polynomial time when t is given in unary.

Clock-preserving conditional simulation of every binary MultiTapeTM

theorem Cslib.Kolmogorov.DescriptionMethod.exists_etimeBoundedComplexity_condUniversalTM_le_ofMultiTapeTM {k : ℕ} {State : Type} [Finite State] (tm : Turing.MultiTapeTM k Bool State) : ∃ (c : ℕ), ∀ (t : ℕ) (w y x : List Bool), tm.RunsInTime ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (w, y)) t → tm.Computes ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (w, y)) x → (condUniversalTM y).etimeBoundedComplexity t x ≤ ↑(w.length + c)

Clock-preserving conditional simulation of MultiTapeTM: for every finite-state binary MultiTapeTM, there is a constant c such that whenever tm on input encPair encBits encBits (w, y) halts within t steps and outputs x, condUniversalTM y outputs x within t steps from a program of length at most w.length + c.

Conditional Kolmogorov complexity measures (condPlain, condTimeBoundedAt,

condTimeBounded, condLevinKt)

noncomputable def Cslib.Kolmogorov.condPlain (x y : List Bool) : ℕ∞

Conditional plain Kolmogorov complexity $K(x \mid y)$ under condUniversalTM y, in ℕ∞ Li and Vitányi, Chapter 2.

noncomputable def Cslib.Kolmogorov.condPlainNat (x y : List Bool) : ℕ

Conditional plain Kolmogorov complexity $K(x \mid y)$ as a natural number.

noncomputable def Cslib.Kolmogorov.condTimeBoundedAt (t : ℕ) (x y : List Bool) : ℕ∞

Step-indexed conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ at step budget t : ℕ (the conditional analogue of Hirahara, Definition 7), in ℕ∞.

noncomputable def Cslib.Kolmogorov.condTimeBounded (t : ℕ → ℕ) (x y : List Bool) : ℕ∞

Function-indexed conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ at step budget t x.length, in ℕ∞.

@[simp]

theorem Cslib.Kolmogorov.condTimeBounded_eq_condTimeBoundedAt (t : ℕ → ℕ) (x y : List Bool) : condTimeBounded t x y = condTimeBoundedAt (t x.length) x y

condTimeBounded t x y is condTimeBoundedAt (t x.length) x y.

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

Conditional time-bounded Kolmogorov complexity $K^t(x \mid y)$ as a natural number.

noncomputable def Cslib.Kolmogorov.condLevinKt (x y : List Bool) : ℕ∞

Conditional Levin time-bounded Kolmogorov complexity $\mathrm{Kt}(x \mid y) = \inf_{s \in \mathbb{N}} \bigl(K^s(x \mid y) + \lceil \log_2 s \rceil\bigr)$ (the conditional analogue of levinKt in Allender et al., Definition 1), in ℕ∞.

noncomputable def Cslib.Kolmogorov.condLevinKtNat (x y : List Bool) : ℕ

Conditional Levin complexity $\mathrm{Kt}(x \mid y)$ as a natural number.

Basic properties and equivalence bridges

@[simp]

theorem Cslib.Kolmogorov.condTimeBoundedAt_zero (x y : List Bool) : condTimeBoundedAt 0 x y = ⊤

At 0 steps, condTimeBoundedAt 0 x y = ⊤.

theorem Cslib.Kolmogorov.condTimeBoundedAt_le_natCast_iff {t : ℕ} {x y : List Bool} {k : ℕ} : condTimeBoundedAt t x y ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ ((DescriptionMethod.condUniversalTM y).run p).runFor t

condTimeBoundedAt t x y ≤ k iff some program of length at most k outputs x given y within t steps.

theorem Cslib.Kolmogorov.condTimeBoundedAt_lt_natCast_iff {t : ℕ} {x y : List Bool} {k : ℕ} : condTimeBoundedAt t x y < ↑k ↔ ∃ (p : List Bool), p.length < k ∧ x ∈ ((DescriptionMethod.condUniversalTM y).run p).runFor t

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

theorem Cslib.Kolmogorov.condTimeBounded_le_natCast_iff {t : ℕ → ℕ} {x y : List Bool} {k : ℕ} : condTimeBounded t x y ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ ((DescriptionMethod.condUniversalTM y).run p).runFor (t x.length)

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

theorem Cslib.Kolmogorov.natCast_condTimeBoundedNat {t : ℕ → ℕ} {x y : List Bool} (h : condTimeBounded t x y ≠ ⊤) : ↑(condTimeBoundedNat t x y) = condTimeBounded t x y

Whenever condTimeBounded t x y ≠ ⊤, condTimeBoundedNat t x y casts back to condTimeBounded t x y.

theorem Cslib.Kolmogorov.condTimeBoundedAt_antitone (x y : List Bool) : Antitone fun (x_1 : ℕ) => condTimeBoundedAt x_1 x y

Antitonicity of condTimeBoundedAt in the step bound t.

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

If t₁ ≤ t₂, then condTimeBoundedAt t₂ x y ≤ condTimeBoundedAt t₁ x y.

theorem Cslib.Kolmogorov.condTimeBounded_antitone (x y : List Bool) : Antitone fun (x_1 : ℕ → ℕ) => condTimeBounded x_1 x y

Antitonicity of condTimeBounded in the time function t.

theorem Cslib.Kolmogorov.condPlain_le_condTimeBoundedAt (t : ℕ) (x y : List Bool) : condPlain x y ≤ condTimeBoundedAt t x y

Dropping the step bound cannot increase conditional complexity (K(x | y) ≤ K^t(x | y)).

theorem Cslib.Kolmogorov.condPlain_le_condTimeBounded (t : ℕ → ℕ) (x y : List Bool) : condPlain x y ≤ condTimeBounded t x y

Dropping the time function cannot increase conditional complexity (K(x | y) ≤ K^t(x | y)).

theorem Cslib.Kolmogorov.iInf_condTimeBoundedAt (x y : List Bool) : ⨅ (t : ℕ), condTimeBoundedAt t x y = condPlain x y

condPlain x y is the infimum of condTimeBoundedAt t x y over t : ℕ.

theorem Cslib.Kolmogorov.condLevinKt_le_condTimeBoundedAt_add (s : ℕ) (x y : List Bool) : condLevinKt x y ≤ condTimeBoundedAt s x y + ↑(Nat.clog 2 s)

For every step count s, condLevinKt x y ≤ condTimeBoundedAt s x y + Nat.clog 2 s.

theorem Cslib.Kolmogorov.condPlain_le_condLevinKt (x y : List Bool) : condPlain x y ≤ condLevinKt x y

Conditional plain complexity bounds conditional Levin complexity from below (K(x | y) ≤ Kt(x | y)).

theorem Cslib.Kolmogorov.condLevinKt_le_natCast_iff {x y : List Bool} {k : ℕ} : condLevinKt x y ≤ ↑k ↔ ∃ (p : List Bool) (s : ℕ), x ∈ ((DescriptionMethod.condUniversalTM y).run p).runFor s ∧ p.length + Nat.clog 2 s ≤ k

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

theorem Cslib.Kolmogorov.condLevinKt_le_natCast_iff_exists_runFor_two_pow {x y : List Bool} {k : ℕ} : condLevinKt x y ≤ ↑k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ ((DescriptionMethod.condUniversalTM y).run p).runFor (2 ^ (k - p.length))

Exponential-step characterization of condLevinKt: $\mathrm{Kt}(x \mid y) \le k$ iff some program $p$ of length at most $k$ outputs $x$ given $y$ within $2^{k - |p|}$ steps.

Polynomial-time conditional upper bounds ($K^t(F(w, y) \mid y) \le |w| + O(1)$)

theorem Cslib.Kolmogorov.exists_condTimeBoundedAt_le_of_computableInPolyTime {F : List Bool × List Bool → List Bool} (hF : Turing.MultiTapeTM.ComputableInPolyTime F (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : ∃ (pF : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pF) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x pF) ∧ ∀ {t : ℕ} (w y : List Bool), Polynomial.eval ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (w, y)).length pF ≤ t → condTimeBoundedAt t (F (w, y)) y ≤ ↑(w.length + c)

Polynomial-time conditional evaluation bound: for any polynomial-time function F : List Bool × List Bool → List Bool, there exist a monotone polynomial pF (with n + 1 ≤ pF.eval n) and a constant c such that for all w y : List Bool and step budgets t ≥ pF.eval (encPair encBits encBits (w, y)).length, $$K^t(F(w, y) \mid y) \le |w| + c.$$

theorem Cslib.Kolmogorov.exists_condTimeBoundedAt_apply_le {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : ∃ (q : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n q) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x q) ∧ (∀ {t : ℕ} (y : List Bool), Polynomial.eval (y.length + 1) q ≤ t → condTimeBoundedAt t (f y) y ≤ ↑c) ∧ ∀ (y : List Bool), condPlain (f y) y ≤ ↑c

Conditional complexity of a polynomial-time function of the condition ($K^t(f(y) \mid y) \le O(1)$): for any f : List Bool → List Bool computable in polynomial time, there exist a monotone polynomial q (with n + 1 ≤ q.eval n) and a constant c such that for all y : List Bool and t ≥ q.eval (y.length + 1), condTimeBoundedAt t (f y) y ≤ c and condPlain (f y) y ≤ c.

theorem Cslib.Kolmogorov.exists_condTimeBoundedAt_self_le : ∃ (q : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n q) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x q) ∧ (∀ {t : ℕ} (y : List Bool), Polynomial.eval (y.length + 1) q ≤ t → condTimeBoundedAt t y y ≤ ↑c) ∧ ∀ (y : List Bool), condPlain y y ≤ ↑c

Self-conditioning ($K^t(y \mid y) \le O(1)$): there exist a monotone polynomial q and a constant c such that condTimeBoundedAt t y y ≤ c whenever q.eval (y.length + 1) ≤ t, and condPlain y y ≤ c for all y.

theorem Cslib.Kolmogorov.exists_condTimeBoundedAt_le_length_add : ∃ (q : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n q) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x q) ∧ (∀ {t : ℕ} (x y : List Bool), Polynomial.eval (2 * x.length + 1 + y.length) q ≤ t → condTimeBoundedAt t x y ≤ ↑(x.length + c)) ∧ ∀ (x y : List Bool), condPlain x y ≤ ↑(x.length + c)

Trivial conditional upper bound ($K^t(x \mid y) \le |x| + O(1)$): there exist a monotone polynomial q (with n + 1 ≤ q.eval n) and a constant c such that for all x y : List Bool and t ≥ q.eval (2 * x.length + 1 + y.length), condTimeBoundedAt t x y ≤ (x.length + c : ℕ) and condPlain x y ≤ (x.length + c : ℕ).

theorem Cslib.Kolmogorov.condPlain_ne_top (x y : List Bool) : condPlain x y ≠ ⊤

Conditional plain complexity condPlain x y is always finite.

@[simp]

theorem Cslib.Kolmogorov.natCast_condPlainNat (x y : List Bool) : ↑(condPlainNat x y) = condPlain x y

Casting condPlainNat x y to ℕ∞ yields condPlain x y.

theorem Cslib.Kolmogorov.condLevinKt_ne_top (x y : List Bool) : condLevinKt x y ≠ ⊤

Conditional Levin complexity condLevinKt x y is always finite.

@[simp]

theorem Cslib.Kolmogorov.natCast_condLevinKtNat (x y : List Bool) : ↑(condLevinKtNat x y) = condLevinKt x y

Casting condLevinKtNat x y to ℕ∞ yields condLevinKt x y.

theorem Cslib.Kolmogorov.condLevinKtNat_le_iff {x y : List Bool} {k : ℕ} : condLevinKtNat x y ≤ k ↔ condLevinKt x y ≤ ↑k

ℕ-valued threshold characterization of condLevinKtNat.

Counting and incompressibility for conditional complexity

theorem Cslib.Kolmogorov.encard_setOf_condTimeBoundedAt_lt (y : List Bool) (t n r : ℕ) : {x : List Bool | x.length = n ∧ condTimeBoundedAt t x y < ↑r}.encard < 2 ^ r

For every condition string y, step bound t, length n, and threshold r, fewer than 2 ^ r strings x of length n have condTimeBoundedAt t x y < r.

theorem Cslib.Kolmogorov.exists_length_eq_forall_le_condTimeBoundedAt (y : List Bool) (n : ℕ) : ∃ (x : List Bool), x.length = n ∧ ∀ (t : ℕ), ↑n ≤ condTimeBoundedAt t x y

Existence of conditionally incompressible strings: for every condition string y and length n, some string x of length n satisfies n ≤ condPlain x y (and hence n ≤ condTimeBoundedAt t x y for all t).

theorem Cslib.Kolmogorov.two_pow_lt_ncard_setOf_length_eq_le_condTimeBounded_add (t : ℕ → ℕ) (y : List Bool) (n c : ℕ) : 2 ^ n < {x : List Bool | x.length = n ∧ ↑(n - c) ≤ condTimeBounded t x y}.ncard + 2 ^ (n - c)

For every condition string y, time function t, and n c : ℕ, all but fewer than 2 ^ (n - c) of the 2 ^ n strings x of length n satisfy (n - c : ℕ) ≤ condTimeBounded t x y.