Average-case hardness building blocks for time-bounded Kolmogorov complexity (K^t)

This module formalizes the $K^t$-specific counting, generator upper-bound, and threshold distinguisher lemmas from Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity. Generic mild average-case hardness definitions and bridges live in Complexity.Computability.Complexity.AverageCase, and reusable BitString Shannon-entropy bounds live in Complexity.Probability.Entropy.BitString. All section, theorem, lemma, and page locators follow the full version arXiv:2009.11514v1 (and ECCC TR20-052).

Main results

• Cslib.Kolmogorov.mildlyHardOnAverageENat_timeBounded_iff, Cslib.Kolmogorov.mildlyHardOnAverageIOENat_timeBounded_iff: equivalence between ℕ∞-valued timeBounded t hardness and ℕ-valued timeBoundedNat t hardness whenever ∀ n, n + 1 ≤ t n.
• Cslib.Kolmogorov.exists_timeBounded_generator_le: for any length-nondecreasing polynomial-time generator $G : \{0, 1\}^* \to \{0, 1\}^*$, there exist a polynomial $p_G$ and a constant $c$ such that for all $t \ge p_G$ and all $z$, $K^t(G(z)) \le |z| + c$ (Liu and Pass, Proof of Theorem 5.2, Equation (3), §5.2, pp. 11–12 of arXiv:2009.11514v1).
• Cslib.Kolmogorov.sum_uniform_timeBoundedNat_lt_le: counting bound on the fraction of $n$-bit strings with $K^t(x) < n - k$ (Liu and Pass, Proof of Theorem 5.2, Equation (2), §5.2, p. 11 of arXiv:2009.11514v1).
• Cslib.Kolmogorov.uniformList_threshold_accept_ge, Cslib.Kolmogorov.generator_threshold_accept_le: acceptance bounds for the Theorem 5.2 threshold distinguisher on $U_m$ and on an entropy-preserving generator distribution $p_G$ (Liu and Pass, Proof of Theorem 5.2, Claims 1–2, §5.2, p. 12 of arXiv:2009.11514v1).

References

• Y. Liu, R. Pass, On One-way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Section 5.2).

Equivalence between timeBounded (ℕ∞) and timeBoundedNat (ℕ) hardness

theorem Cslib.Kolmogorov.mildlyHardOnAverageENat_timeBounded_iff {t : ℕ → ℕ} (ht : ∀ (n : ℕ), n + 1 ≤ t n) : Complexity.MildlyHardOnAverageENat (timeBounded t) ↔ Complexity.MildlyHardOnAverage (timeBoundedNat t)

Whenever ∀ n, n + 1 ≤ t n, MildlyHardOnAverageENat (timeBounded t) is equivalent to MildlyHardOnAverage (timeBoundedNat t).

theorem Cslib.Kolmogorov.mildlyHardOnAverageIOENat_timeBounded_iff {t : ℕ → ℕ} (ht : ∀ (n : ℕ), n + 1 ≤ t n) : Complexity.MildlyHardOnAverageIOENat (timeBounded t) ↔ Complexity.MildlyHardOnAverageIO (timeBoundedNat t)

Whenever ∀ n, n + 1 ≤ t n, MildlyHardOnAverageIOENat (timeBounded t) is equivalent to MildlyHardOnAverageIO (timeBoundedNat t).

Generator $K^t$ upper bound

(Liu and Pass, Proof of Theorem 5.2, Eq. (3), §5.2, pp. 11–12 of arXiv:2009.11514v1)

theorem Cslib.Kolmogorov.exists_timeBounded_generator_le {G : List Bool → List Bool} (hG : Turing.MultiTapeTM.ComputableInPolyTime G Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hstretch : ∀ (z : List Bool), z.length ≤ (G z).length) : ∃ (pG : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (m : ℕ), Polynomial.eval m pG ≤ t m) → ∀ (z : List Bool), timeBounded t (G z) ≤ ↑(z.length + c)

Liu and Pass, Proof of Theorem 5.2, Equation (3), §5.2, pp. 11–12 of arXiv:2009.11514v1: Outputs of a polynomial-time generator have $K^t(G(z)) \le |z| + O(1)$. For any polynomial-time generator $G : \{0, 1\}^* \to \{0, 1\}^*$ that does not shrink its input ($|z| \le |G(z)|$), there exist a polynomial $p_G$ (with $n + 1 \le p_G(n)$) and a constant $c$ such that for every time bound $t$ dominating $p_G$ and every seed $z \in \{0, 1\}^*$, $K^t(G(z)) \le |z| + c$.

theorem Cslib.Kolmogorov.timeBoundedNat_generator_le {G : List Bool → List Bool} {pG : Polynomial ℕ} {c : ℕ} (hpG : ∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) (hbound : ∀ {t : ℕ → ℕ}, (∀ (m : ℕ), Polynomial.eval m pG ≤ t m) → ∀ (z : List Bool), timeBounded t (G z) ≤ ↑(z.length + c)) {t : ℕ → ℕ} (ht : ∀ (m : ℕ), Polynomial.eval m pG ≤ t m) (z : List Bool) : timeBoundedNat t (G z) ≤ z.length + c

Natural-number version of exists_timeBounded_generator_le for timeBoundedNat.

theorem Cslib.Kolmogorov.exists_timeBounded_of_computableInPolyTime {α : Type u_1} {enc : α ↪ List Bool} {G : α → List Bool} (hG : Turing.MultiTapeTM.ComputableInPolyTime G enc Turing.MultiTapeTM.encBits) : ∃ (pG : Polynomial ℕ) (c : ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x pG) ∧ ∀ {t : ℕ → ℕ} (a : α), Polynomial.eval (enc a).length pG ≤ t (G a).length → timeBounded t (G a) ≤ ↑((enc a).length + c)

General polynomial-time $K^t$ upper bound for any encoded input type $\alpha$: if G : α → List Bool is computable in polynomial time with respect to enc : α ↪ List Bool and encBits, there exist a monotone polynomial pG (with n + 1 ≤ pG.eval n) and a constant c such that whenever pG.eval (enc a).length ≤ t (G a).length, we have timeBounded t (G a) ≤ ((enc a).length + c : ℕ).

theorem Cslib.Kolmogorov.card_filter_timeBoundedNat_lt {t : ℕ → ℕ} {n : ℕ} (ht : n + 1 ≤ t n) (r : ℕ) : {x : Fin n → Bool | timeBoundedNat t (List.ofFn x) < r}.card < 2 ^ r

Fewer than 2 ^ r bitstrings of length n have timeBoundedNat t (List.ofFn x) < r whenever n + 1 ≤ t n.

theorem Cslib.Kolmogorov.sum_uniform_timeBoundedNat_lt_le {t : ℕ → ℕ} {n : ℕ} (ht : n + 1 ≤ t n) (k : ℕ) : (∑ x : BitString n, ((Probability.PMF.uniformOfFintype (BitString n)) x).toReal * if timeBoundedNat t (List.ofFn x) < n - k then 1 else 0) ≤ 2 ^ (-↑k)

Liu and Pass, Proof of Theorem 5.2, Equation (2), §5.2, p. 11 of arXiv:2009.11514v1: Probability that a random $n$-bit string has $K^t(x) < n - k$ is at most $2^{-k}$.

theorem Cslib.Kolmogorov.uniformList_threshold_accept_ge {t : ℕ → ℕ} {m : ℕ} (ht : m + 1 ≤ t m) (k g_err : ℕ) (q : List Bool → PMF ℕ) : (((BitString.uniformList m).bind fun (y : List Bool) => PMF.map (fun (v : ℕ) => decide (timeBoundedNat t y - g_err ≤ v ∧ v ≤ timeBoundedNat t y)) (q y)) true).toReal - 2 ^ (-↑k) ≤ (((BitString.uniformList m).bind fun (y : List Bool) => PMF.map (fun (v : ℕ) => decide (m - k - g_err ≤ v)) (q y)) true).toReal

Liu and Pass, Proof of Theorem 5.2, Claim 1, §5.2, p. 12 of arXiv:2009.11514v1: Acceptance probability of the threshold distinguisher on the uniform distribution $U_m$.

theorem Cslib.Kolmogorov.generator_threshold_accept_le {t : ℕ → ℕ} {m : ℕ} (hm : 1 ≤ m) {pG : PMF (BitString m)} {B : ℝ} (hB3 : 3 ≤ B) (hent : B ≤ Probability.PMF.entropy pG) (k g_err : ℕ) (hlow : ∀ x ∈ pG.support, timeBoundedNat t (List.ofFn x) < m - k - g_err) (q : List Bool → PMF ℕ) : (((PMF.map List.ofFn pG).bind fun (y : List Bool) => PMF.map (fun (v : ℕ) => decide (m - k - g_err ≤ v)) (q y)) true).toReal ≤ 1 - 1 / ↑m + 2 ^ (↑m - (B - 3)) * (1 - (((BitString.uniformList m).bind fun (y : List Bool) => PMF.map (fun (v : ℕ) => decide (timeBoundedNat t y - g_err ≤ v ∧ v ≤ timeBoundedNat t y)) (q y)) true).toReal)

Liu and Pass, Proof of Theorem 5.2, Claim 2, §5.2, p. 12 of arXiv:2009.11514v1: Acceptance probability of the threshold distinguisher on an entropy-preserving generator distribution $p_G$.