One-Way Functions and Average-Case Hardness of Time-Bounded Kolmogorov Complexity

This module proves the M2a polynomial-threshold form of the forward direction of the main theorem of Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity and combines it with the Section 4 converse (Complexity.Crypto.Computational.OneWay.LiuPassConverse) to establish the headline equivalences of Theorem 3.1:

• Forward direction: if one-way functions exist, then for every constant $d \in \mathbb{N}$ there exists a polynomial $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, $t$-time-bounded Kolmogorov complexity $K^t$ is mildly hard on average against uniform strict PPT heuristics, and mildly hard on average to approximate within the symmetric error windows $d (\lfloor \log_2 n \rfloor + 1)$, $d \lceil \log_2 n \rceil$, $d \lfloor \log_2 n \rfloor$, and the real-valued window $d \log_2 n$.
• Headline equivalences (Theorem 3.1 (a) $\Leftrightarrow$ (b) $\Leftrightarrow$ (c)): one-way functions exist if and only if there exists a polynomial $p(n) \ge n + 1$ such that $K^p$ is mildly hard on average (exists_oneWay_iff_exists_mildlyHardOnAverage_timeBoundedNat), and equivalently in the polynomial-threshold and symmetric approximation forms.

All section, theorem, definition, lemma, and page locators follow the full version arXiv:2009.11514v1 (and ECCC TR20-052).

Time-bound scope note (M2a polynomial-threshold form and $n + 1$-step sufficient clock): In Liu and Pass, Theorem 3.1 (b)–(c), §3, p. 9 of arXiv:2009.11514v1, item (b) quantifies over a polynomial $t(n) > 0$, while item (c) and the post-Theorem 3.1 remark give hardness for every polynomial $t(n) \ge (1 + \varepsilon) n$. The source obtains that near-linear range from a rate-$1$ efficient condEP-PRG, one whose running time on $n$-bit inputs is $n + O(n^{c})$ for a constant $c < 1$ (Liu and Pass, §5.1 and Theorem 5.2, §5.2, p. 11, and Theorem 5.6, §5.3, p. 17 of arXiv:2009.11514v1), built by a padding construction. This module proves only the polynomial-threshold form $\exists p,\ \forall t \ge p$ of (c) and of the threshold consequence; the near-linear range is not formalized.

The threshold comes from the generator's own running-time certificate. The proof of CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat_log_succ (Theorem 5.2) applies Kolmogorov.exists_timeBounded_of_computableInPolyTime to the truncated generator, which reads a truncation count in unary and a seed and drops that many trailing output bits. That theorem extracts constants $c', d'$ bounding the running time by $c' (n + 1)^{d'}$ from the ComputableInPolyTime certificate and takes $p_0(n) = (c' + 1)(n + 1)^{d' + 1}$, where $n$ is the length of the encoded input. An output of length $m$ comes from an encoded input of length at most $m + 2 \gamma + 3$, so the threshold is $p_G(m) = p_0(m + 2 \gamma + 3)$, and every $t \ge p_G$ gives the generator's multi-tape machine enough steps to print each output from its seed. In the native model DescriptionMethod.universalTM, $K^t$ counts steps of the described machine, so DescriptionMethod.exists_etimeBoundedComplexity_universalTM_le_ofMultiTapeTM is clock-preserving: it compares universalTM with the generator's machine at the same step bound and contributes only an additive constant to the description length. The threshold is polynomial because the certificate bounds the generator's running time only by some polynomial; the near-linear range would need a rate-$1$ step bound for the generator's machine.

Separately, the literal/copy program bound supplies a program that prints each $n$-bit string within $n + 1$ steps (Kolmogorov.timeBoundedNat_le_length_add). Our statements therefore assume $p(n) \ge n + 1$ as a sufficient clock hypothesis ensuring finite $K^t$ in the native model (rather than a lower bound on every program or an equivalence with the source's $t(n) > 0$ convention).

Symmetric approximation and logarithm rounding: Liu and Pass, Definition 2.5, §2.3, p. 8 of arXiv:2009.11514v1 defines $g$-approximation via the symmetric error bound $|v - f(x)| \le g(|x|)$, formalized on $\mathbb{N}$ by Cslib.Complexity.MildlyHardOnAverageToApprox (Nat.dist v (f x) ≤ g n). The threshold distinguisher of Theorem 5.2 directly establishes one-sided underestimation hardness (Cslib.Complexity.MildlyHardOnAverageToOneSidedApprox) for the upper-rounded integer log window $g(n) = d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)). Applying the PPT shift and gap-scaling bridge MildlyHardOnAverageToOneSidedApprox.mildlyHardOnAverageToApprox (shifting a heuristic's output down by $g(|x|)$ and doubling the PRG stretch parameter from $2 d + 3$ to $4 d + 3$) yields symmetric MildlyHardOnAverageToApprox for d * (Nat.log 2 n + 1). Since $\lfloor \log_2 n \rfloor \le \log_2 n \le \lceil \log_2 n \rceil \le \lfloor \log_2 n \rfloor + 1$ for all $n \ge 1$, monotonicity immediately yields symmetric approximation hardness for d * Nat.clog 2 n, d * Nat.log 2 n, and the real-valued $|(v : \mathbb{R}) - K^t(x)| \le d \log_2 |x|$ window (OneWay.exists_eventually_real_abs_sub_le_timeBoundedNat).

Main results

• Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat_log_succ: a $(1 / n^2, \gamma)$-condEP-PRG with $\gamma \ge 2 d + 3$ implies one-sided $d (\lfloor \log_2 n \rfloor + 1)$-approximation hardness of $K^t$ for all $t \ge p_G$ (Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1, M2a polynomial-threshold one-sided helper).
• Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ, Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_clog, Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat: a $(1 / n^2, \gamma)$-condEP-PRG with $\gamma \ge 4 d + 3$ implies symmetric PPT approximation hardness of $K^t$ for all $t \ge p_G$ under $d (\lfloor \log_2 n \rfloor + 1)$, $d \lceil \log_2 n \rceil$, and $d \lfloor \log_2 n \rfloor$ (Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1, M2a polynomial-threshold form).
• Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverage_timeBoundedNat: exact average-case PPT hardness specialization of Theorem 5.2 ($\gamma \ge 3$, M2a polynomial-threshold form).
• Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ, Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat_clog, Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat, Cslib.Crypto.OneWay.exists_eventually_real_abs_sub_le_timeBoundedNat: every one-way function implies the existence of a polynomial $p$ such that for all $t \ge p$, $K^t$ is mildly hard on average to approximate within $d (\lfloor \log_2 n \rfloor + 1)$, $d \lceil \log_2 n \rceil$, $d \lfloor \log_2 n \rfloor$, and real $d \log_2 n$ against uniform strict PPT heuristics (Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1, M2a polynomial-threshold form).
• Cslib.Crypto.OneWay.exists_mildlyHardOnAverage_timeBoundedNat: every one-way function implies the existence of a polynomial $p$ such that for all $t \ge p$, $K^t$ is mildly hard on average against uniform strict PPT heuristics (Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (b), §3, p. 9 of arXiv:2009.11514v1, M2a polynomial-threshold form).
• Cslib.Crypto.exists_mildlyHardOnAverageToApprox_of_exists_oneWay, Cslib.Crypto.exists_mildlyHardOnAverage_of_exists_oneWay: existential M2a polynomial-threshold forms of Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c) and (a) $\Rightarrow$ (b), §3, p. 9 of arXiv:2009.11514v1.
• Cslib.Crypto.exists_oneWay_iff_exists_mildlyHardOnAverage_timeBoundedNat, Cslib.Crypto.exists_oneWay_iff_exists_mildlyHardOnAverageENat_timeBounded, Cslib.Crypto.exists_oneWay_iff_exists_forall_mildlyHardOnAverage_timeBoundedNat: headline characterizations of one-way functions via average-case hardness of $K^t$ (Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (b) and post-Theorem 3.1 threshold consequence, §3, p. 9 of arXiv:2009.11514v1).
• Cslib.Crypto.exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_clog_timeBoundedNat, Cslib.Crypto.exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_timeBoundedNat: approximation-hardness characterizations of one-way functions (Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1), together with the upper-rounded log-window variant exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_log_succ_timeBoundedNat.

References

• Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Sections 3, 4, and 5).

Stretch schedule helpers

Truncated generator and threshold distinguisher for Theorem 5.2

Theorem 5.2: Conditional EP-PRGs imply $K^t$ is mildly hard on average

(M2a polynomial-threshold form)

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat_log_succ {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 2 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToOneSidedApprox (fun (n : ℕ) => d * (Nat.log 2 n + 1)) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1 (M2a polynomial-threshold one-sided helper): If $G$ is a $(1 / n^2, \gamma)$-condEP-PRG with entropy-loss constant $\alpha$ and stretch factor $\gamma \ge 2 d + 3$, then there exists a polynomial $p_G$ (with $n + 1 \le p_G(n)$ for all $n$) such that for every time bound $t : \mathbb{N} \to \mathbb{N}$ dominating $p_G$, Kolmogorov.timeBoundedNat t is mildly hard on average to one-sidedly approximate within the upper-rounded log window $d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)) against uniform strict PPT heuristics.

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 2 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToOneSidedApprox (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

One-sided $(d \lfloor \log_2 n \rfloor)$-approximation corollary of CondEPPRG.exists_mildlyHardOnAverageToOneSidedApprox_timeBoundedNat_log_succ ($\gamma \ge 2 d + 3$).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 4 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * (Nat.log 2 n + 1)) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1 (M2a polynomial-threshold form, upper-rounded log window): If $G$ is a $(1 / n^2, \gamma)$-condEP-PRG with entropy-loss constant $\alpha$ and stretch factor $\gamma \ge 4 d + 3$, then there exists a polynomial $p_G$ (with $n + 1 \le p_G(n)$ for all $n$) such that for every time bound $t : \mathbb{N} \to \mathbb{N}$ dominating $p_G$, Kolmogorov.timeBoundedNat t is mildly hard on average to symmetrically approximate within the upper-rounded log window $d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)) against uniform strict PPT heuristics.

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_clog {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 4 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.clog 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1 (M2a polynomial-threshold form, ceiling log window d * Nat.clog 2 n): Symmetric $(d \lceil \log_2 n \rceil)$-approximation corollary of CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ ($\gamma \ge 4 d + 3$).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 4 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1 (M2a polynomial-threshold form, floor log window d * Nat.log 2 n): Symmetric $(d \lfloor \log_2 n \rfloor)$-approximation corollary of CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ ($\gamma \ge 4 d + 3$).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverage_timeBoundedNat {G : List Bool → List Bool} {γ α : ℕ} (hγ : 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)

Exact average-case PPT hardness specialization of Theorem 5.2 at $d = 0$ ($\gamma \ge 3$, M2a polynomial-threshold form) (Liu and Pass, Theorem 5.2, §5.2, p. 11 of arXiv:2009.11514v1).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageToApproxDet_timeBoundedNat {G : List Bool → List Bool} {γ α : ℕ} (d : ℕ) (hγ : 4 * d + 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageToApproxDet (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Library corollary: deterministic polynomial-time heuristic specialization of CondEPPRG.exists_mildlyHardOnAverageToApprox_timeBoundedNat ($\gamma \ge 4 d + 3$).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageDet_timeBoundedNat {G : List Bool → List Bool} {γ α : ℕ} (hγ : 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageDet (Kolmogorov.timeBoundedNat t)

Library corollary: deterministic polynomial-time heuristic specialization of CondEPPRG.exists_mildlyHardOnAverage_timeBoundedNat ($\gamma \ge 3$).

theorem Cslib.Crypto.CondEPPRG.exists_mildlyHardOnAverageENat_timeBounded {G : List Bool → List Bool} {γ α : ℕ} (hγ : 3 ≤ γ) (hG : CondEPPRG G (fun (n : ℕ) => 1 / ↑n ^ 2) γ α) : ∃ (pG : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n pG) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n pG ≤ t n) → Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded t)

Library corollary: ℕ∞-valued Kolmogorov.timeBounded version of CondEPPRG.exists_mildlyHardOnAverage_timeBoundedNat.

Theorem 3.1 (a) $\Rightarrow$ (c) and (a) $\Rightarrow$ (b): One-way functions imply

average-case hardness of $K^t$ (M2a polynomial-threshold form)

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat_log_succ {f : List Bool → List Bool} (hf : OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * (Nat.log 2 n + 1)) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, upper-rounded log window): If $f$ is a one-way function, then for every approximation constant $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t : \mathbb{N} \to \mathbb{N}$ satisfying $t(n) \ge p(n)$ for all $n$, timeBoundedNat t is mildly hard on average to symmetrically approximate within the upper-rounded integer log window $d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)) against uniform strict PPT heuristics.

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat_clog {f : List Bool → List Bool} (hf : OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.clog 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, ceiling log window): If $f$ is a one-way function, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lceil \log_2 n \rceil$ (d * Nat.clog 2 n) against uniform strict PPT heuristics.

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat {f : List Bool → List Bool} (hf : OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, floor log window): If $f$ is a one-way function, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lfloor \log_2 n \rfloor$ (d * Nat.log 2 n) against uniform strict PPT heuristics.

theorem Cslib.Crypto.OneWay.exists_eventually_real_abs_sub_le_timeBoundedNat {f : List Bool → List Bool} (hf : OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → ∃ (q : Polynomial ℕ), (∀ (n : ℕ), 0 < Polynomial.eval n q) ∧ ∀ (H : List Bool → ProbComp ℕ), Probability.IsPPTOn Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat H → ∀ᶠ (n : ℕ) in Filter.atTop, (((BitString.uniformList n).bind fun (x : List Bool) => PMF.map (fun (v : ℕ) => decide (|↑v - ↑(Kolmogorov.timeBoundedNat t x)| ≤ ↑d * Real.logb 2 ↑n)) (H x).eval) true).toReal ≤ 1 - 1 / ↑(Polynomial.eval n q)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, real-valued $d \log_2 n$ window): If $f$ is a one-way function, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, there exists a positive polynomial $q$ such that for every uniform strict PPT heuristic $\mathcal{H} : \{0, 1\}^* \to \mathrm{ProbComp}\ \mathbb{N}$ and all sufficiently large $n$, $$\Pr_{x \leftarrow \{0, 1\}^n, v \leftarrow \mathcal{H}(x)}[|(v : \mathbb{R}) - K^t(x)| \le d \log_2 n] \le 1 - \frac{1}{q(n)}.$$

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverage_timeBoundedNat {f : List Bool → List Bool} (hf : OneWay f) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (b), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form): If $f$ is a one-way function, then there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics.

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageToApproxDet_timeBoundedNat {f : List Bool → List Bool} (hf : OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApproxDet (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Library corollary: deterministic polynomial-time heuristic specialization of OneWay.exists_mildlyHardOnAverageToApprox_timeBoundedNat.

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageDet_timeBoundedNat {f : List Bool → List Bool} (hf : OneWay f) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageDet (Kolmogorov.timeBoundedNat t)

Library corollary: deterministic polynomial-time heuristic specialization of OneWay.exists_mildlyHardOnAverage_timeBoundedNat.

theorem Cslib.Crypto.OneWay.exists_mildlyHardOnAverageENat_timeBounded {f : List Bool → List Bool} (hf : OneWay f) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded t)

Library corollary: ℕ∞-valued Kolmogorov.timeBounded version of OneWay.exists_mildlyHardOnAverage_timeBoundedNat.

theorem Cslib.Crypto.exists_mildlyHardOnAverageToApprox_log_succ_of_exists_oneWay (h : ∃ (f : List Bool → List Bool), OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * (Nat.log 2 n + 1)) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (existential M2a polynomial-threshold form, upper-rounded log window): If one-way functions exist, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)) against uniform strict PPT heuristics.

theorem Cslib.Crypto.exists_mildlyHardOnAverageToApprox_clog_of_exists_oneWay (h : ∃ (f : List Bool → List Bool), OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.clog 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (existential M2a polynomial-threshold form, ceiling log window): If one-way functions exist, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lceil \log_2 n \rceil$ (d * Nat.clog 2 n) against uniform strict PPT heuristics.

theorem Cslib.Crypto.exists_mildlyHardOnAverageToApprox_of_exists_oneWay (h : ∃ (f : List Bool → List Bool), OneWay f) (d : ℕ) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (existential M2a polynomial-threshold form, floor log window): If one-way functions exist, then for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lfloor \log_2 n \rfloor$ (d * Nat.log 2 n) against uniform strict PPT heuristics.

theorem Cslib.Crypto.exists_mildlyHardOnAverage_of_exists_oneWay (h : ∃ (f : List Bool → List Bool), OneWay f) : ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Rightarrow$ (b), §3, p. 9 of arXiv:2009.11514v1 (existential M2a polynomial-threshold form): If one-way functions exist, then there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics.

Headline equivalences (Liu and Pass, Theorem 3.1, §3, p. 9)

theorem Cslib.Crypto.exists_oneWay_iff_exists_mildlyHardOnAverage_timeBoundedNat : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat fun (n : ℕ) => Polynomial.eval n p)

Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (b), §3, p. 9 of arXiv:2009.11514v1: One-way functions exist if and only if there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ (a sufficient clock hypothesis in the native model ensuring finite $K^t$ via timeBoundedNat_le_length_add, where the source writes $t(n) > 0$) such that timeBoundedNat (fun n => p.eval n) is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverage).

theorem Cslib.Crypto.exists_oneWay_iff_exists_mildlyHardOnAverageENat_timeBounded : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ Complexity.MildlyHardOnAverageENat (Kolmogorov.timeBounded fun (n : ℕ) => Polynomial.eval n p)

ℕ∞-valued Kolmogorov.timeBounded corollary of Theorem 3.1 (a) $\Leftrightarrow$ (b): One-way functions exist if and only if there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ such that timeBounded (fun n => p.eval n) is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverageENat).

theorem Cslib.Crypto.exists_oneWay_iff_exists_forall_mildlyHardOnAverage_timeBoundedNat : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverage (Kolmogorov.timeBoundedNat t)

Liu and Pass, §3, p. 9 of arXiv:2009.11514v1 (post-Theorem 3.1 threshold consequence, M2a polynomial-threshold form): One-way functions exist if and only if there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average against uniform strict PPT heuristics (MildlyHardOnAverage).

theorem Cslib.Crypto.exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_log_succ_timeBoundedNat : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∀ (d : ℕ), ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * (Nat.log 2 n + 1)) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, upper-rounded log window): One-way functions exist if and only if for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d (\lfloor \log_2 n \rfloor + 1)$ (d * (Nat.log 2 n + 1)) against uniform strict PPT heuristics (MildlyHardOnAverageToApprox).

theorem Cslib.Crypto.exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_clog_timeBoundedNat : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∀ (d : ℕ), ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.clog 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, ceiling log window): One-way functions exist if and only if for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lceil \log_2 n \rceil$ (d * Nat.clog 2 n) against uniform strict PPT heuristics (MildlyHardOnAverageToApprox).

theorem Cslib.Crypto.exists_oneWay_iff_forall_exists_mildlyHardOnAverageToApprox_timeBoundedNat : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∀ (d : ℕ), ∃ (p : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n p) ∧ ∀ {t : ℕ → ℕ}, (∀ (n : ℕ), Polynomial.eval n p ≤ t n) → Complexity.MildlyHardOnAverageToApprox (fun (n : ℕ) => d * Nat.log 2 n) (Kolmogorov.timeBoundedNat t)

Liu and Pass, Theorem 3.1 (a) $\Leftrightarrow$ (c), §3, p. 9 of arXiv:2009.11514v1 (M2a polynomial-threshold form, floor log window): One-way functions exist if and only if for every $d \in \mathbb{N}$ there exists a polynomial $p \in \mathbb{N}[X]$ with $p(n) \ge n + 1$ for all $n$ such that for every time bound $t(n) \ge p(n)$, timeBoundedNat t is mildly hard on average to symmetrically approximate within $d \lfloor \log_2 n \rfloor$ (d * Nat.log 2 n) against uniform strict PPT heuristics (MildlyHardOnAverageToApprox).