The Minimum Kt Problem (MKtP) and GapMKtP

This module develops the decision and promise problems associated with Levin's time-bounded Kolmogorov complexity Cslib.Kolmogorov.levinKt ($\mathrm{Kt}$):

• Exponential-step witness characterization (levinKt_le_natCast_iff_exists_runFor_two_pow): $\mathrm{Kt}(x) \le k$ if and only if some binary program $p$ of length at most $k$ outputs $x$ within $2^{k - |p|}$ steps under universalTM.
• Optimal Kt-witnesses and running-time bound for random strings (exists_length_add_clog_eq_levinKtNat, encard_setOf_forall_optimal_levinKt_two_pow_lt, two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow): Every string $x$ admits an optimal $\mathrm{Kt}$-witness $(p, s)$ with $s > 0$ and $|p| + \lceil \log_2 s \rceil = \mathrm{Kt}(x)$. Following Liu and Pass, Section 3.1, Fact 3.1, p. 10, if any witness $(p, s)$ satisfying $|p| + \lceil \log_2 s \rceil \le \mathrm{Kt}(x)$ runs for more than $2^{\mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil + m}$ steps, then $K(x) < |x| - m$; consequently, all but fewer than $2^{n - m}$ strings of length $n$ have an optimal $\mathrm{Kt}$-witness running in at most $2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps. Here the extra $\lceil \log_2(n + 1) \rceil$ term in the exponent (relative to Liu–Pass's $2^c / \varepsilon$ bound from Fact 2.1, $\mathrm{Kt}(x) \le |x| + c$) comes from our multi-tape bound levinKt_le_length_add ($\mathrm{Kt}(x) \le |x| + \mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil$).
• MKtP ∈ E ⊆ EXP (MKtP.mem_E, MKtP.mem_EXP, MKtPAt.mem_EXP): Cslib.Kolmogorov.MKtP is the set of pairs (x, k) : List Bool × ℕ with levinKt x ≤ k, and Cslib.Kolmogorov.MKtPAt s is the fixed-threshold language {x | levinKt x ≤ s x.length} (Liu and Pass, Section 2.2; Oliveira and Santhanam, Appendix A, Definition 44, p. 34; compare R_Kt ∈ E in Allender et al., Definitions 1 and 6). While Liu and Pass, Section 2.2 encode the threshold $k$ in binary as a $\lceil \log_2 n \rceil$-bit integer (in their model Fact 2.1 gives $\mathrm{Kt}(x) \le |x| + c$, and in ours levinKt_le_length_add gives $\mathrm{Kt}(x) \le |x| + \mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil$), here MKtP is paired with the unary threshold encoding encPair encBits encUnary so that $k + 1 \le |(x, 1^k)|$ holds unconditionally for arbitrary $k \in \mathbb{N}$ without a syntactic $k < 2 |x|$ side condition; for nontrivial thresholds $k \le O(|x|)$ and for every polynomial-time unary threshold $s$ in MKtPAt s, the unary encoding has polynomial length and EXP membership transfers via PolyTimeReducible.mem_EXP. Enumerating candidate programs Ladner.word j of length at most k and running universalTMRunFor for $2^{k - |p|}$ steps places MKtP in E (encPair encBits encUnary) and EXP (encPair encBits encUnary), and places MKtPAt s in EXP encBits whenever s is computable in polynomial time in unary.
• Promise problem GapMKtP (Cslib.Kolmogorov.GapMKtP): The promise problem separating $\mathrm{Kt}(x) \le s_1(|x|)$ from $\mathrm{Kt}(x) > s_2(|x|)$ for $s_1 \le s_2$ (Oliveira and Santhanam, Appendix A, Definition 44, p. 34).

Main definitions

• Cslib.Kolmogorov.MKtP: the language $\{(x, k) \mid \mathrm{Kt}(x) \le k\}$.
• Cslib.Kolmogorov.MKtP.boundedSearch: polynomial-time bounded search for a Kt-witness up to word-index and step cap N.
• Cslib.Kolmogorov.MKtPAt: the fixed-threshold language $\{x \mid \mathrm{Kt}(x) \le s(|x|)\}$.
• Cslib.Kolmogorov.GapMKtP, Cslib.Kolmogorov.GapMKtP.yesSet, Cslib.Kolmogorov.GapMKtP.noSet: the promise problem GapMKtP[s₁, s₂].

Main results

• Cslib.Kolmogorov.levinKt_le_natCast_iff_exists_runFor_two_pow, Cslib.Kolmogorov.levinKtNat_le_iff_exists_runFor_two_pow: exponential-step witness characterization of $\mathrm{Kt}(x) \le k$.
• Cslib.Kolmogorov.exists_length_add_clog_eq_levinKt, Cslib.Kolmogorov.exists_length_add_clog_eq_levinKtNat: existence of an optimal Kt-witness.
• Cslib.Kolmogorov.plain_lt_of_levinKtNat_witness_two_pow_lt, Cslib.Kolmogorov.encard_setOf_forall_optimal_levinKt_two_pow_lt, Cslib.Kolmogorov.two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow: running-time bound for optimal Kt-witnesses (Liu and Pass, Section 3.1, Fact 3.1, p. 10).
• Cslib.Kolmogorov.MKtP.computableInPolyTime_boundedSearch, Cslib.Kolmogorov.MKtP.boundedSearch_eq_true_iff_of_two_pow_le: polynomial-time certificate and exactness of MKtP.boundedSearch.
• Cslib.Kolmogorov.MKtP.mem_E, Cslib.Kolmogorov.MKtP.mem_EXP: MKtP is in E and EXP.
• Cslib.Kolmogorov.MKtPAt.polyTimeReducible_MKtP, Cslib.Kolmogorov.MKtPAt.mem_EXP, Cslib.Kolmogorov.MKtPAt.mem_EXP_polynomial: MKtPAt s ∈ EXP encBits for polynomial-time unary thresholds s.
• Cslib.Kolmogorov.GapMKtP.disjoint_yesSet_noSet, Cslib.Kolmogorov.GapMKtP.id_eq: consistency and zero-gap specialization of GapMKtP.

References

• E. Allender, H. Buhrman, M. Koucký, D. van Melkebeek, D. Ronneburger, Power from Random Strings
• L. A. Levin, Universal Sequential Search Problems
• L. A. Levin, Randomness Conservation Inequalities; Information and Independence in Mathematical Theories
• Y. Liu, R. Pass, On the Possibility of Basing Cryptography on EXP ≠ BPP
• I. C. Oliveira, R. Santhanam, Hardness Magnification for Natural Problems

Exponential-step witness characterization and optimal witnesses for levinKt

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

Exponential-step characterization of levinKt. $\mathrm{Kt}(x) \le k$ iff some binary program $p$ of length at most $k$ outputs $x$ within $2^{k - |p|}$ steps under universalTM.

theorem Cslib.Kolmogorov.levinKtNat_le_iff_exists_runFor_two_pow {x : List Bool} {k : ℕ} : levinKtNat x ≤ k ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (2 ^ (k - p.length))

ℕ-valued exponential-step characterization of levinKtNat.

theorem Cslib.Kolmogorov.exists_length_add_clog_eq_levinKtNat (x : List Bool) : ∃ (p : List Bool) (s : ℕ), 0 < s ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor s ∧ p.length + Nat.clog 2 s = levinKtNat x

Every string x admits an optimal Kt-witness (p, s) with 0 < s, x ∈ (universalTM.run p).runFor s, and p.length + Nat.clog 2 s = levinKtNat x.

theorem Cslib.Kolmogorov.exists_length_add_clog_eq_levinKt (x : List Bool) : ∃ (p : List Bool) (s : ℕ), 0 < s ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor s ∧ ↑(p.length + Nat.clog 2 s) = levinKt x

Every string x admits an optimal Kt-witness (p, s) in ℕ∞ with 0 < s, x ∈ (universalTM.run p).runFor s, and (p.length + Nat.clog 2 s : ℕ) = levinKt x.

theorem Cslib.Kolmogorov.plain_lt_of_levinKtNat_witness_two_pow_lt {x p : List Bool} {s m : ℕ} (hm : m ≤ x.length) (hp : x ∈ (DescriptionMethod.universalTM.run p).runFor s) (hopt : p.length + Nat.clog 2 s ≤ levinKtNat x) (hs : 2 ^ (copyOverhead + Nat.clog 2 (x.length + 1) + m) < s) : plain x < ↑(x.length - m)

Liu and Pass, Section 3.1, Fact 3.1, p. 10: If $(p, s)$ outputs $x$ within $s$ steps with $|p| + \lceil \log_2 s \rceil \le \mathrm{Kt}(x)$, and $s > 2^{\mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil + m}$ (with $m \le |x|$), then the plain Kolmogorov complexity of $x$ satisfies $K(x) < |x| - m$. The extra $\lceil \log_2(|x| + 1) \rceil$ term in the exponent (relative to Liu–Pass's $2^c / \varepsilon$ from Fact 2.1, $\mathrm{Kt}(x) \le |x| + c$) comes from levinKt_le_length_add ($\mathrm{Kt}(x) \le |x| + \mathrm{copyOverhead} + \lceil \log_2(|x| + 1) \rceil$).

theorem Cslib.Kolmogorov.encard_setOf_forall_optimal_levinKt_two_pow_lt {n m : ℕ} (hm : m ≤ n) : {x : List Bool | x.length = n ∧ ∀ (p : List Bool) (s : ℕ), x ∈ (DescriptionMethod.universalTM.run p).runFor s → p.length + Nat.clog 2 s ≤ levinKtNat x → 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m) < s}.encard < 2 ^ (n - m)

Liu and Pass, Section 3.1, Fact 3.1, p. 10: For $m \le n$, fewer than $2^{n - m}$ strings $x \in \{0, 1\}^n$ have the property that every optimal $\mathrm{Kt}$-witness $(p, s)$ for $x$ runs for more than $2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps (with the extra $\lceil \log_2(n + 1) \rceil$ term coming from levinKt_le_length_add).

theorem Cslib.Kolmogorov.two_pow_lt_ncard_setOf_exists_optimal_levinKt_le_two_pow {n m : ℕ} (hm : m ≤ n) : 2 ^ n < {x : List Bool | x.length = n ∧ ∃ (p : List Bool) (s : ℕ), x ∈ (DescriptionMethod.universalTM.run p).runFor s ∧ p.length + Nat.clog 2 s ≤ levinKtNat x ∧ s ≤ 2 ^ (copyOverhead + Nat.clog 2 (n + 1) + m)}.ncard + 2 ^ (n - m)

Liu and Pass, Section 3.1, Fact 3.1, p. 10: For $m \le n$, all but fewer than $2^{n - m}$ of the $2^n$ strings of length $n$ admit an optimal $\mathrm{Kt}$-witness $(p, s)$ running in at most $2^{\mathrm{copyOverhead} + \lceil \log_2(n + 1) \rceil + m}$ steps (with the extra $\lceil \log_2(n + 1) \rceil$ term coming from levinKt_le_length_add).

The Minimum Kt Problem (MKtP) and MKtP ∈ E ⊆ EXP

def Cslib.Kolmogorov.MKtP : Set (List Bool × ℕ)

The Minimum Kt Problem (MKtP) (Liu and Pass, Section 2.2; Oliveira and Santhanam, Appendix A, Definition 44, p. 34): the set of pairs (x, k) : List Bool × ℕ such that levinKt x ≤ k. In Complexitylib's complexity-class statements below (MKtP.mem_E, MKtP.mem_EXP), MKtP is encoded by encPair encBits encUnary (with the threshold k in unary rather than the $\lceil \log_2 n \rceil$-bit binary representation of Liu and Pass, Section 2.2) so that $k + 1 \le |(x, 1^k)|$ holds for all $k \in \mathbb{N}$ without a side condition bounding $k$.

theorem Cslib.Kolmogorov.MKtP.mem_iff {xk : List Bool × ℕ} : xk ∈ MKtP ↔ levinKt xk.1 ≤ ↑xk.2

A pair xk belongs to MKtP iff levinKt xk.1 ≤ xk.2.

@[simp]

theorem Cslib.Kolmogorov.MKtP.pair_mem_iff {x : List Bool} {k : ℕ} : (x, k) ∈ MKtP ↔ levinKt x ≤ ↑k

(x, k) ∈ MKtP iff levinKt x ≤ k.

theorem Cslib.Kolmogorov.MKtP.pair_mem_iff_levinKtNat_le {x : List Bool} {k : ℕ} : (x, k) ∈ MKtP ↔ levinKtNat x ≤ k

(x, k) ∈ MKtP iff levinKtNat x ≤ k.

theorem Cslib.Kolmogorov.MKtP.pair_mem_iff_exists_runFor_two_pow {x : List Bool} {k : ℕ} : (x, k) ∈ MKtP ↔ ∃ (p : List Bool), p.length ≤ k ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (2 ^ (k - p.length))

(x, k) ∈ MKtP iff some program p of length at most k outputs x within 2 ^ (k - |p|) steps under universalTM.

theorem Cslib.Kolmogorov.MKtP.mem_of_le {x : List Bool} {k₁ k₂ : ℕ} (h : (x, k₁) ∈ MKtP) (hk : k₁ ≤ k₂) : (x, k₂) ∈ MKtP

Monotonicity of MKtP in the threshold k.

def Cslib.Kolmogorov.MKtP.boundedSearch (x : List Bool) (k N : ℕ) : Bool

Bounded brute-force search for a Kt-witness of (x, k) up to word-index and step cap N: checks whether some word p = Ladner.word j with j < N has p.length ≤ k and outputs x within min (2 ^ (k - p.length)) N steps.

theorem Cslib.Kolmogorov.MKtP.boundedSearch_eq_true_iff_of_two_pow_le {x : List Bool} {k N : ℕ} (hN : 2 ^ (k + 1) ≤ N) : boundedSearch x k N = true ↔ (x, k) ∈ MKtP

Whenever $2^{k + 1} \le N$, boundedSearch x k N = true iff (x, k) ∈ MKtP.

theorem Cslib.Kolmogorov.MKtP.computableInPolyTime_boundedSearch : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : List Bool × ℕ × ℕ) => boundedSearch q.1 q.2.1 q.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool

boundedSearch is computable in polynomial time when k and N are encoded in unary.

theorem Cslib.Kolmogorov.MKtP.mem_E : MKtP ∈ Complexity.E (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary)

MKtP is in linear exponential time E with respect to encPair encBits encUnary.

theorem Cslib.Kolmogorov.MKtP.mem_EXP : MKtP ∈ Complexity.EXP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary)

MKtP is in EXP with respect to encPair encBits encUnary (Liu and Pass, Section 2.2; compare R_Kt ∈ E in Allender et al., Definition 6).

Fixed-threshold formulation (MKtPAt)

def Cslib.Kolmogorov.MKtPAt (s : ℕ → ℕ) : Set (List Bool)

Fixed-threshold MKtP (MKtPAt s, Oliveira and Santhanam, Appendix A, Definition 44, p. 34; Liu and Pass, Section 2.2): the language of binary strings x with levinKt x ≤ s x.length.

theorem Cslib.Kolmogorov.mem_MKtPAt_iff {s : ℕ → ℕ} {x : List Bool} : x ∈ MKtPAt s ↔ levinKt x ≤ ↑(s x.length)

x ∈ MKtPAt s iff levinKt x ≤ s x.length.

@[simp]

theorem Cslib.Kolmogorov.mem_MKtPAt_iff_mem_MKtP {s : ℕ → ℕ} {x : List Bool} : x ∈ MKtPAt s ↔ (x, s x.length) ∈ MKtP

x ∈ MKtPAt s iff (x, s x.length) ∈ MKtP.

theorem Cslib.Kolmogorov.mem_MKtPAt_iff_levinKtNat_le {s : ℕ → ℕ} {x : List Bool} : x ∈ MKtPAt s ↔ levinKtNat x ≤ s x.length

x ∈ MKtPAt s iff levinKtNat x ≤ s x.length.

theorem Cslib.Kolmogorov.MKtPAt.polyTimeReducible_MKtP {s : ℕ → ℕ} (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Complexity.PolyTimeReducible Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) (MKtPAt s) MKtP

Whenever s is computable in polynomial time in unary, MKtPAt s is polynomial-time many-one reducible to MKtP.

theorem Cslib.Kolmogorov.MKtPAt.mem_EXP {s : ℕ → ℕ} (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : MKtPAt s ∈ Complexity.EXP Turing.MultiTapeTM.encBits

Fixed-threshold MKtPAt s is in EXP whenever s is computable in polynomial time in unary.

theorem Cslib.Kolmogorov.MKtPAt.mem_EXP_polynomial (q : Polynomial ℕ) : (MKtPAt fun (x : ℕ) => Polynomial.eval x q) ∈ Complexity.EXP Turing.MultiTapeTM.encBits

For any polynomial threshold q : Polynomial ℕ, MKtPAt q.eval ∈ EXP encBits.

The promise problem GapMKtP

def Cslib.Kolmogorov.GapMKtP.yesSet (s₁ : ℕ → ℕ) : Set (List Bool)

The yes-instances of GapMKtP[s₁, s₂]: strings x with levinKt x ≤ s₁ x.length (Oliveira and Santhanam, Appendix A, Definition 44, p. 34).

def Cslib.Kolmogorov.GapMKtP.noSet (s₂ : ℕ → ℕ) : Set (List Bool)

The no-instances of GapMKtP[s₁, s₂]: strings x with s₂ x.length < levinKt x (Oliveira and Santhanam, Appendix A, Definition 44, p. 34).

theorem Cslib.Kolmogorov.GapMKtP.mem_yesSet_iff {s₁ : ℕ → ℕ} {x : List Bool} : x ∈ yesSet s₁ ↔ x ∈ MKtPAt s₁

x ∈ GapMKtP.yesSet s₁ iff x ∈ MKtPAt s₁.

theorem Cslib.Kolmogorov.GapMKtP.mem_noSet_iff {s₂ : ℕ → ℕ} {x : List Bool} : x ∈ noSet s₂ ↔ ↑(s₂ x.length) < levinKt x

x ∈ GapMKtP.noSet s₂ iff (s₂ x.length : ℕ∞) < levinKt x.

theorem Cslib.Kolmogorov.GapMKtP.mem_noSet_iff_lt_levinKtNat {s₂ : ℕ → ℕ} {x : List Bool} : x ∈ noSet s₂ ↔ s₂ x.length < levinKtNat x

x ∈ GapMKtP.noSet s₂ iff s₂ x.length < levinKtNat x.

theorem Cslib.Kolmogorov.GapMKtP.disjoint_yesSet_noSet {s₁ s₂ : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) : Disjoint (yesSet s₁) (noSet s₂)

When s₁ n ≤ s₂ n for all n, GapMKtP.yesSet s₁ and GapMKtP.noSet s₂ are disjoint.

theorem Cslib.Kolmogorov.GapMKtP.noSet_eq_compl (s : ℕ → ℕ) : noSet s = (MKtPAt s)ᶜ

When s₁ = s₂, GapMKtP.noSet s is the complement of MKtPAt s.

def Cslib.Kolmogorov.GapMKtP (s₁ s₂ : ℕ → ℕ) (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) : Complexity.PromiseProblem (List Bool)

The GapMKtP promise problem (Oliveira and Santhanam, Appendix A, Definition 44, p. 34): separates MKtPAt s₁ (levinKt x ≤ s₁ |x|) from GapMKtP.noSet s₂ (levinKt x > s₂ |x|) whenever s₁ n ≤ s₂ n.

@[simp]

theorem Cslib.Kolmogorov.GapMKtP.yes_eq {s₁ s₂ : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) : (GapMKtP s₁ s₂ hs).yes = MKtPAt s₁

The yes-instances of GapMKtP s₁ s₂ hs are MKtPAt s₁.

@[simp]

theorem Cslib.Kolmogorov.GapMKtP.no_eq {s₁ s₂ : ℕ → ℕ} (hs : ∀ (n : ℕ), s₁ n ≤ s₂ n) : (GapMKtP s₁ s₂ hs).no = noSet s₂

The no-instances of GapMKtP s₁ s₂ hs are GapMKtP.noSet s₂.

@[simp]

theorem Cslib.Kolmogorov.GapMKtP.id_eq (s : ℕ → ℕ) : GapMKtP s s ⋯ = Complexity.PromiseProblem.ofSet (MKtPAt s)

With zero gap (s₁ = s₂ = s), GapMKtP is the decision problem MKtPAt s viewed as a promise problem (PromiseProblem.ofSet (MKtPAt s)).