On some inequality (upper bound) on a function of two variables There is a problem (of physical origin) which needs an analytical solution or a hint.  Let us consider the following real-valued function of two variables
$y (t,a) = 4 \left(1 + \frac{t}{x(t,a)}\right)^{ - a - 1/2}  
  \left(1 - \frac{2}{x(t,a)}\right)^{ 1/2} (x(t,a))^{-3/2} (z(t,a))^{1/4} \left(1 + \frac{t}{2}\right)^{ a},$
where  $t  > 0$,  $0 < a < 1$ and
$x(t,a)   =   \frac{a-1}{2} t + \frac{3}{2}+\frac{1}{2}\sqrt{z(t,a)}$,
$z(t,a)   =   (1-a)^2 t^2+ 2(3-a)t +9.$
It is necessary to prove  that
$$y(t,a) < 1$$
for all $t  > 0$ and $0 < a < 1$. The numerical analysis supports this bound.
P.S. I apologize for too ``technical'' question. It looks that the inequality is valid also for $a = 1$
but it fails for $a > 1$.
 A: Here is a human verifiable proof.
The quadratic equation for $x$ in terms of $a,t$ is
$$
x^2-[(a-1)t+3]x+(2a-3)t=0
$$
Substituting $x=y+2$, we get
$$
y^2+[1+(1-a)t]y=2+t=1+\frac{T-a}{1-a}\tag{*}
$$
where $T=1+(1-a)t$ (I'm trying to mimic Mathematica explanation of proofs style). Thus $\frac{t}{2}+1=\frac{y(y+T)}{2}$.
Next, from the equation (*),
$$
t=\frac{(y-1)(y+2)}{1-(1-a)y}\,,
$$
so
$$
1+\frac tx=\frac{ay}{1-(1-a)y}
$$
Finally, from the OP equation for $x$, we get
$$
\sqrt z=2x-(a-1)t-3=2y+T\,.
$$
Plugging all that nonsense in, we see that we need to bound from above (by $1$ or better) the expression
$$
4\left[\frac{(y+T)(1-(1-a)y)}{2a}\right]^a
\left[\frac{(1-(1-a)y)}{ay}\right]^{1/2}\times
\\
\left[\frac{y}{y+2}\right]^{1/2}
\frac 1{(y+2)^{3/2}}(2y+T)^{1/2}
$$
Now, from $(*)$,
$$
(1-a)y(y+T)=1+T-2a\,,
$$
so the first bracket simplifies to
$$
\left[\frac{y-1+2a}{2a}\right]^a=\left[1+\frac{y-1}{2a}\right]^a\le 1+\frac{y-1}2=\frac{y+1}2
$$
(Here I use Bernoulli in the same way as Iosif did).
We can cancel $y^{1/2}$ and combine $y+2$'s, which leaves us with the factor
$$
F(T)=\frac{1-(1-a)y}a(2y+T)
$$
Here I'm going to use the symbolic differentiation tool:
$$
\frac d{dT}\log F(T)=-\frac{(1-a)\dot y}{1-(1-a)y}+\frac{2\dot y+1}{2y+T}\,.
$$
From $(*)$, we have $(1-a)(2y+T)\dot y=1-(1-a)y$, so the logarithmic derivative evaluates to $\frac{2\dot y}{2y+T}\le \frac{2\dot y}{2y+1}=\frac d{dT}\log(2y+1)$ (using $\dot y>0$ and equality for $T=y=1$, of course).
Thus $F(T)\le 2y+1$ and we end up with proving that
$$
2(y+1)\sqrt{2y+1}\le(y+2)^2
$$
However $(y+2)^2-2(y+1)\sqrt{2y+1}=\sqrt 2^2+(y+1-\sqrt{2y+1})^2$, which, according to the principle we discussed is trustworthy.
I leave the improvement of the last inequality to $2(y+1)\sqrt{2y+1}\le \gamma(y+2)^2$ with explicit $\gamma<1$ to Mathematica. Let me see if it is capable of that. But, of course, I want to see the full output, not just the declaration that the statement is true.
What I did doesn't go beyond the AI capabilities (just some bunch of random substitutions and symbolic manipulations). However, until I see a printout like this, I'll remain utterly skeptical. The fact that one of the most useful Mathematica commands for a friend of mine who is a big fan of it is "Quit kernel" doesn't add to my trust.
A: $\newcommand{\ty}{\tilde y}$With $x:=x(t,a)$, $y:=y(t,a)$, and $z:=z(t,a)$, we have
\begin{align*}
    y &= 4(1+t/x)^{-a-1/2}(1-2/x)^{1/2} x^{-3/2} z^{1/4}(1+t/2)^a \\ 
    &=4\Big(\frac{1+t/2}{1+t/x}\Big)^a(1+t/x)^{-1/2}(1-2/x)^{1/2} x^{-3/2} z^{1/4} \\ 
    &\le\ty:=4\Big(1-a+a\frac{1+t/2}{1+t/x}\Big)(1+t/x)^{-1/2}(1-2/x)^{1/2} x^{-3/2} z^{1/4}, 
\end{align*}
by the convexity of $u^a$ in $a$ for each real $u>0$.
Since $\ty$ is an algebraic function of $(t,a)$, it can be proved purely algorithmically that for all $(t,a)\in(0,\infty)\times(0,1)$ we have $\ty<1$ and hence $y<1$. Mathematica takes about 6 sec for this proof, which is a very long time for a computer program. In about 17 sec, Mathematica can also prove that $\ty<9/10$ and hence $y<9/10$. Below is the image of the corresponding Mathematica notebook; click on the image below to enlarge it.

A: a human verifiable proof:
Let us prove that the sharp bound of $y$ is $\frac{\sqrt{3+2\sqrt 3}}{3}$.
Letting $x := x(t, a), z := z(t, a), y := y(t, a)$, we have
$$y = 4 \left(\frac{1 + t/2}{1 + t/x}\right)^a\cdot \left(\frac{z}{(1 + t/x)^2}\right)^{1/4} (1 - 2/x)^{1/2} x^{-3/2}. \tag{1}$$
Using Bernoulli inequality $(1 + u)^r \le 1 + ru$ for all $r \in (0, 1]$ and all $u > -1$, we have
$$y \le 4 \left(1 + \left(\frac{1 + t/2}{1 + t/x}  - 1\right)a\right)\cdot \left(\frac{z}{(1 + t/x)^2}\right)^{1/4} (1 - 2/x)^{1/2} x^{-3/2} \tag{2}$$
and
$$y^2 \le 16 \left(1 + \left(\frac{1 + t/2}{1 + t/x}  - 1\right)a\right)^2\cdot \left(\frac{z}{(1 + t/x)^2}\right)^{1/2} (1 - 2/x) x^{-3}. \tag{3}$$
We first simplify the expression. We have
$$a \in (0, 1) \quad \iff \quad a = \frac{1}{1 + s}, \quad s > 0. $$
Then, we have (the so-called Euler substitution)
$$t > 0 \quad \iff \quad t = \frac{2(1+s)(3s+2 - 3u))}{u^2 - s^2}, \quad s < u < s + \frac23. $$
With these substitutions, we have
$$z = \left(\frac{-3u^2 + (6s + 4)u - 3s^2}{u^2 - s^2}\right)^2$$
and
$$x = \frac{6s + 2}{u + s}.$$
Then, (3) is written as
$$y^2 \le {\frac { \left(-3u^2 + 6su + 4u - 3s^2 \right)
        \left( 5\,s+2 - u \right) ^{2}}{4 \left( 3\,s+1 \right) ^{3}}}.
$$
The constraints are: $s > 0$ and $s < u < s + \frac23$.
We have
$$\sup_{s> 0, ~ s < u < s + \frac23} {\frac { \left(-3u^2 + 6su + 4u - 3s^2 \right)
        \left( 5\,s+2 - u \right) ^{2}}{4 \left( 3\,s+1 \right) ^{3}}} = \frac{3 + 2\sqrt 3}{9}. \tag{4}$$
(The proof is given at the end.)
Thus, we have
$$y \le \frac{\sqrt{3 + 2\sqrt 3}}{3}.$$
On the other hand, in (1), letting
$t = 3 + 3\sqrt 3, ~ a = 1$,
we have $y = \frac{\sqrt{3 + 2\sqrt 3}}{3}$.
Thus, $\frac{\sqrt{3 + 2\sqrt 3}}{3}$ is a sharp bound.
We are done.

Proof of (4):
Fixed $s > 0$, let
$$f(u) := {\frac { \left(-3u^2 + 6su + 4u - 3s^2 \right)
        \left( 5\,s+2 - u \right) ^{2}}{4 \left( 3\,s+1 \right) ^{3}}}.$$
The maximum of $f(u)$ is attained
at $u_0 = 2\,s+1- \frac13\,\sqrt {9\,{s}^{2}+12\,s+3}$. Let
$g(s) := f(u_0)$.
It is easy to prove that $g'(s) < 0$ for all $s \ge 0$.
Thus, $g(s) \le g(0) =  \frac{3 + 2\sqrt 3}{9}$.
We are done.
