What is known about constructively irrational numbers? Intuitively, a constructively irrational number is one for which we can effectively separate it from any rational number in terms of the latter's denominator. More formally, a constructively irrational number is a number $x$ such that there is a known primitive recursive function $f : \mathbb{Z}^+ \rightarrow \mathbb{Z}^+$ such that $|x - \frac{p}{q}| > \frac{1}{f(q)}$ for all $p, q \in \mathbb{Z}$ such that $q \neq 0$. This corresponds closely to what is meant by "irrational" in constructive mathematics, where "irrational" is interpreted as stronger than "not rational" (indeed, strictly stronger).
For example, $\sqrt{2}$ is constructively irrational, given that $|\sqrt{2} - \frac{p}{q}| > \frac{1}{3q^2}$.
Which theorems of irrational number theory are known to also hold for constructively irrational numbers? In particular, are all algebraic irrational numbers constructively irrational? Are $\pi$ and $e$ constructively irrational? What about $e^n$ for $n \in \mathbb{Z}$ and $n \neq 0$? Or $\ln{n}$ for $n \in \mathbb{Z}^+$ and $n \geq 2$? And finally, is $\log_p{n}$ constructively irrational for $p$ a prime, $n \in \mathbb{Z}^+$, and $n$ not an integer power of $p$?
Answers to any of these questions would be greatly appreciated.
 A: All algebraic numbers are by this definition constructively irrational. You can adopt Liouville's proof that Liouville numbers are transcendental and turn it in the other direction to get a function of the sort you want given an algebraic number and its corresponding polynomial. Explicit versions of Baker's theorem also can be thought of as a similar statement. Baker's sort of methods also give you your desired result for a lot of logarithms.
What you are interested in is also closely connected to the idea of irrationality measure. In particular, Mahler's theorem on the irrationality measure of $\pi$ may be enough to show that $\pi$ is constructively irrational. For the best bounds currently on that, see this paper by Doron Zeilberger and Wadim Zudilin. I say "may" here because there are epsilons floating around there and I haven't checked to see if they can be made explicit.
A quick aside about a number you didn't ask about but I'm now wondering about: I don't know if Apery's proof that $\zeta(3)$ is irrational can be turned into a proof of constructive irrationality. My guess is that things there are much too delicate.
