I have written some code to solve for the roots of a 4th order polynomial, and in the process, I noticed that the resolvent cubic always has at least one positive real root.
I can't find anywhere that states that this is proven to be true, is it?
Edit: When I posted this, I didn't know there were several possible resolvent cubics. The one I am using is from Nonweiler's paper, Roots of Low Order Polynomial Equations, TOMS Algorithm 326.
The answer is No. The cubic resolvent need not have a positive real root. To recall, given,
$$x^4+ax^3+bx^2+cx+d=0$$
then the four solutions are,
$$x_{1,2} = -\frac{a}{4}+\frac{\color{red}\pm\sqrt{u}}{2}\color{blue}+\frac{1}{4}\sqrt{3a^2-8b-4u+\frac{-a^3+4ab-8c}{\color{red}\pm\sqrt{u}}}\tag1$$
$$x_{3,4} = -\frac{a}{4}+\frac{\color{red}\pm\sqrt{u}}{2}\color{blue}-\frac{1}{4}\sqrt{3a^2-8b-4u+\frac{-a^3+4ab-8c}{\color{red}\pm\sqrt{u}}}\tag2$$
where $u$ is any non-zero root of the cubic resolvent,
$u^3-\tfrac{1}{4}(3 a^2 - 8 b)u^2+\tfrac{1}{48}\big((3 a^2 - 8 b)^2 - 16 (b^2 - 3 a c + 12 d)\big)u-\tfrac{1}{64}(\color{brown}{a^3 - 4 a b + 8 c})^2=0\tag3$
This is the solution used by Mathematica but I've simplified it. To answer your question, we can "cheat" and set $\color{brown}{a^3 - 4 a b + 8 c}= 0$ so $u_1=0$, and either of the non-zero roots must be employed. A quick search then reveals that using $a,b,c,d = 1,\;2,\;\frac{7}{8},\;\frac{1}{2}$ and the solutions of the resolvent are,
$$u_1,\,u_2,\,u_3 = 0,\;\tfrac{-13-\sqrt{101}}{8},\;\tfrac{-13+\sqrt{101}}{8}$$
none of which is a positive real.
However, we can modify your question by asking, "For real $a,b,c,d$, if the cubic resolvent has all non-zero roots, then is one root always positive?" That one remains to be settled.
