Is this solution to nonlinear first order ODE correct?

Question

Mathematica 11.3.

I am not sure if this solution given by Mathematica is correct. But I'd like to ask the experts.

eqn = 2*Sqrt[x] y'[x]==Sqrt[1-y[x]];
sol = DSolve[eqn,y,x]

(eqn/.sol)//Simplify

Now the above is supposed to give True if the solution satisfies the ODE. But it does not

I found the above is true only under the following condition

 Assuming[ (C[1] + Sqrt[x]) < 0, Simplify[(eqn /. sol)]]

Therefore, I think the solution given by Mathematica could not be considered valid in general. It is true only under specific condition.

Question is: Is Mathematica solution to the above ODE correct, and if so, why it does not give True then when substituting the solution back to the ODE?

http://reference.wolfram.com/language/tutorial/DSolveSolutionVerification.html

Appendix

The step by step solution to the above problem is below.

The ODE to solve is \begin{align*} 2\,\sqrt {x}{\frac {\rm d}{{\rm d}x}}y \left( x \right) =\sqrt {1-y \left( x \right) } \end{align*} Since the ODE is $y'=1/2\,{\frac {\sqrt {1-y}}{\sqrt {x}}}$, then this is separable. It can be written as $$ y' = f(x) g(y) $$ Where $f(x)={\frac {1}{\sqrt {x}}}$ and $g(y)=1/2\,\sqrt {1-y}$, therefore $$ y' = \left({\frac {1}{\sqrt {x}}}\right)\left(1/2\,\sqrt {1-y}\right) $$
Hence
\begin{align*} \left(2\,{\frac {1}{\sqrt {1-y}}}\right)\mathop{\mathrm{d}y} &= {\frac {1}{\sqrt {x}}}\mathop{\mathrm{d}x}\\ \int \left(2\,{\frac {1}{\sqrt {1-y}}}\right)\mathop{\mathrm{d}y} &= \int {\frac {1}{\sqrt {x}}}\mathop{\mathrm{d}x}\\ -4\,\sqrt {1-y}+{\it C}&=2\,\sqrt {x}\\ \end{align*}

The above is the final solution. I will leave it implicit.

Answer 1

The explicit solution given by DSolve is actually Solved from the implicit solution. This can be verified by:

Trace[DSolve[eqn, y, x], Solve[_, y[x]], TraceInternal -> True] // Flatten
(* {HoldForm[Solve[-2 Sqrt[1 - y[x]] == Sqrt[x] + C[1], y[x]]]} *)
% // ReleaseHold
(* {{{y[x] -> 1/4 (4 - x - 2 Sqrt[x] C[1] - C[1]^2)}}} *)

So the question boils down to "why doesn't Solve give the condition for the solution", and this has been explained in Possible Issues of document of Solve:

Solve gives generic solutions; solutions involving equations on parameters are not given… With MaxExtraConditions -> All, Solve also gives non-generic solutions.

Solve[-2 Sqrt[1 - y[x]] == Sqrt[x] + C[1], y[x], MaxExtraConditions -> All]
(* Alternatively: *)
Solve[-2 Sqrt[1 - y[x]] == Sqrt[x] + C[1], y[x], Method -> Reduce]
(* {{y[x] -> ConditionalExpression[1/4 (4 - x - 2 Sqrt[x] C[1] - C[1]^2), 
    Sqrt[x] + C[1] + Sqrt[(Sqrt[x] + C[1])^2] == 0]}} *)

Answer 2

Picking up from my earlier comment, note that you first have to define a branch for square-root(positive/negative). The conventional branch is positive. Once that is agreed upon, eyeball the implicit solution in the following form:

$$-4\sqrt{1-y}=2\sqrt{x}+2C_1$$

The LHS is non-positive, and so should be the RHS. This information gets lost when one squares both sides to get the explicit solution.

This means that $\sqrt{x}+C_1 \leq 0\; \forall C_1\; \forall (x,y)$ satisfying the above equation.

Note that here $C_1=-\frac{C}{2}$ as you mentioned in the implicit solution in the question.

Answer 3

What we learn here is, always try to verify solutions. You might get conditons for variables and parameters.

test = (eqn /. First@sol) // Simplify

red = test // Reduce[#, Reals] &

(*   (C[1] < 0 && 0 <= x <= C[1]^2) || (C[1] == 0 && x == 0)   *)

RegionPlot[red /. C[1] -> a, {x, -2, 5}, {a, -6, 6}, 
    FrameLabel -> {x, "C[1]"}]