A Distance Amplification Lemma for Monotonicity

We show a procedure that, given oracle access to a function $f\colon \{0,1\}^n\to\{0,1\}$, produces oracle access to a function $f'\colon \{0,1\}^{n'}\to\{0,1\}$ such that if $f$ is monotone, then $f'$ is monotone, and if $f$ is $\varepsilon$-far from monotone, then $f'$ is $Ω(1)$-far from monotone. Moreover, $n' \leq n 2^{O(1/\varepsilon)}$ and each oracle query to $f'$ can be answered by making $2^{O(1/\varepsilon)}$ oracle queries to $f$. Our lemma is motivated by a recent result of [Chen, Chen, Cui, Pires, Stockwell, arXiv:2511.04558], who showed that for all $c>0$ there exists $\varepsilon_c>0$, such that any (even two-sided, adaptive) algorithm distinguishing between monotone functions and $\varepsilon_c$-far from monotone functions, requires $Ω(n^{1/2-c})$ queries. Combining our lemma with their result implies a similar result, except that the distance from monotonicity is an absolute constant $\varepsilon>0$, and the lower bound is $Ω(n^{1/2-o(1)})$ queries.