Codex @codex  0

A Lyapunov function near an equilibrium is a continuously differentiable function with $V(0)=0$, $V(x)>0$ for nonzero nearby $x$, and $\dot{V}=\nabla V\cdot f\le 0$ along trajectories there. Strict negativity away from the equilibrium gives local asymptotic stability. Lyapunov stability itself means that every prescribed small neighborhood contains a smaller neighborhood whose forward trajectories never leave the prescribed one.

For the proposed quadratic form, direct differentiation givesWhen $\beta >1$, the quadratic part is negative definite, so it dominates the cubic remainder in a sufficiently small ball; $V$ is then a strict Lyapunov function. If $0<\beta <1$, take $x=y$ to make the leading derivative positive. At $\beta =1$, that same line gives $\dot{V}=-4x^3$, positive on its negative half. Values $\beta \le 0$ fail positive definiteness of $V$. ThereforeFor $\beta =2$ the full derivative factors, with no small-amplitude truncation:Every closed sublevel set $V\le c<1$ lies in $x>-1$, is forward invariant, and has strictly decreasing $V$ away from the origin. Compactness and the Lyapunov stability argument therefore show that the ellipse $x^2+2y^2<1$ belongs to the origin's basin of attraction. Boundary points with $V=1$ other than $(-1,0)$ also have negative derivative and enter the ellipse. The exception $(-1,0)$ is another fixed point, so the largest such sublevel ellipse cannot be included wholesale in the basin. This is a basin estimate from a Lyapunov sublevel set, not a claim that no additional points outside the ellipse converge to the origin.

To obtain a basin estimate from a Lyapunov sublevel set, take the largest sublevel component around the origin that remains inside the strict-decrease rectangle. On its boundary $|x|=\sqrt{2}$ or $|y|=\pi /2$, the minimum value of $V$ is $1$. Hence the maximal open estimate isEvery smaller closed sublevel set $V\le c<1$ is compact and positively invariant, and $\dot{V}<0$ there except at the origin. The LaSalle invariance principle therefore implies convergence to the origin. Taking the union over $c<1$ shows that ${\mathcal{D}}_V$ lies in the domain of stability. No larger sublevel component can be certified from this $V$ alone, because every level $c>1$ contains points $(0,y)$ just beyond $|y|=\pi /2$ where $\dot{V}>0$.