Since the OP was kind enough to reference an older answer of mine, and also to alert me to the fact, I will provide some input here, of naive flavor, I guess, since mathoverflow is definitely over and out of my league. I will use $\Phi()$ for the standard normal CDF and $\phi()$ for the standard normal PDF.
In my answer in math.se I had proved that
$${\rm Var}(Y) = {\rm Var}(X)\cdot \left[1+\sigma^2\frac{\partial^2 \ln H(\mu)}{\partial \mu^2}\right],\;\; -1 <\sigma^2\frac{\partial^2 \ln H(\mu)}{\partial \mu^2} \leq 0 $$
where:
$$\ln H(\mu)=\ln \big(\Phi(\beta(\mu))-\Phi(\alpha(\mu))\big)$$
$$\alpha=(a-\mu)/\sigma, \;\beta=(b-\mu)/\sigma$$.
The weak inequality comes from the fact that $H$ is log-concave (see the original post).
Calculating the second derivative, in order to prove strict inequality, we have to show that
$$\frac{\partial^2 \ln H(\mu)}{\partial \mu^2} < 0 \implies D \equiv [-\phi'(\alpha)+\phi'(\beta)][\Phi(\beta)-\Phi(\alpha)]-[\phi(\alpha)-\phi(\beta)]^2 < 0 $$
We note that $\Phi(\beta)-\Phi(\alpha) >0 $ always.
CASE A : $a \leq \mu \leq b$ (including one-sided trunctaions).
Here, by the unimodality of $\phi()$, with $\mu$ being the mode, we have that
$$\phi'(\alpha) \geq 0, \phi'(\beta) \leq 0 \implies -\phi'(\alpha)+\phi'(\beta) < 0$$
since the two derivatives cannot be both equal to zero.
Then $D < 0$ always (including truncation symmetric around the mean, where, due to the fact that $\phi()$ is an even function, we have that $\phi(\alpha)=\phi(\beta)$, and the second element of $D$ will be zero. But the first element is always strictly negative).
So for this case we have proved that $\partial^2 \ln H(\mu)/\partial \mu^2 < 0$ as we wanted.
The cases left out are all the cases where $\mu$ does not belong to the (two-sided or one-sided) truncated support.
CASE B : Truncated support $S_B\equiv (-\infty , b], \mu \notin S_B$
Here the inequality to prove is
$$D_B \equiv \phi'(\beta)\Phi(\beta)-\phi(\beta)^2 < 0$$
Since $\phi'(\beta) = -\beta \phi(\beta)$ we wan to show
$$-\beta \phi(\beta)\Phi(\beta)-\phi(\beta)^2 < 0 \implies -\beta \Phi(\beta)-\phi(\beta) < 0 \implies \beta \Phi(\beta)+\phi(\beta) > 0$$
But this holds because
$$\beta \Phi(\beta)+\phi(\beta) = \int_{-\infty}^{\beta}\Phi(t){\rm d}t$$
and the integral is necessarily strictly greater than zero since $\Phi()$ is non-negative and non-constantly zero. So we have proved here too what we needed to prove.
CASE C : Truncated support $S_C\equiv [a, \infty ), \mu \notin S_C$
Here the inequality to prove is
$$-\phi'(\alpha)[1-\Phi(\alpha)]-\phi(\alpha)^2 < 0 \implies \alpha \phi(\alpha)[1-\Phi(\alpha)]-\phi(\alpha)^2 < 0 $$
and simplifying and using the symmetry properties of the two functions we have
$$ \implies (-\alpha)\Phi(-\alpha) + \phi(-\alpha) >0$$
and we are at the same situation as in Case B. So QED here too.
I am not treating the two-sided truncation cases $a < b < \mu$ and $\mu < a < b$. As with the cases I treated, I am certain there exists some more advanced and elegant way to prove what we want.
Best Answer
Here's a sketch and a link for how I prove it. Let $$ f(x) = - \left( \frac{1}{x} - \frac{1}{x^3} + \frac{3}{x^5}\right) \phi(x) .$$
Now show (lemma): $\frac{df}{dx} = \left(1 + \frac{15}{x^6}\right)\phi(x)$.
(To prove this, use that $\frac{d\phi}{dx} = - x \phi(x)$, the product rule, and some cancellation.)
Now suppose $x > 0$:
\begin{align*} 1 - \Phi(x) &= \int_{t=x}^{\infty} \phi(x) dx \\ &\leq \int_{t=x}^{\infty} \left(1 + \frac{15}{x^6}\right) \phi(x) dx \\ &= \lim_{t\to\infty} f(t) - f(x) \\ &= - f(x) \\ &= \left(\frac{1}{x} - \frac{1}{x^3} + \frac{3}{x^5} \right) \phi(x) . \end{align*}
Using the next term in the series gives $f(x) = -\left(\frac{1}{x} - \frac{1}{x^3} + \frac{3}{x^5} - \frac{15}{x^7}\right)\phi(x)$ and $\frac{df}{dx} = \left(1 - \frac{105}{x^8}\right)\phi(x)$. Notice because of the alternating positive/negative terms, $\frac{df}{dx}$ is now $\phi$ times something less than one, so plugging it into the same proof gives a lower bound on $1 - \Phi(x)$. I have a blog post on the general form of this (sorry to not point you to a more formal reference).