TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A strict local minimum of the potential gives a Lyapunov stable equilibrium of the mechanical system, by energy conservation

Statement

Let $n \geq 1$ , let $Ω \subseteq R^{n}$ be open, let $M : Ω \to M_{n} (R)$ be a $C^{2}$ field of symmetric positive definite matrices, let $U : Ω \to R$ be $C^{2}$ , let $q_{0} \in Ω$ with $\nabla U (q_{0}) = 0$ , and suppose $q_{0}$ is a strict local minimum of $U$ : there is $r_{0} > 0$ with $\overline{B} (q_{0}, r_{0}) \subseteq Ω$ and

$U (q) > U (q_{0}) (0 < ∥ q - q_{0} ∥_{2} < r_{0}) .$

Let $G$ be the mechanical vector field of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart on $Ω \times R^{n}$ , with energy $E (q, v) = \frac{1}{2} v^{T} M (q) v + U (q)$ . Then $(q_{0}, 0)$ is a Lyapunov stable equilibrium of $(q^{'}, v^{'}) = G (q, v)$ in the sense of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system: for every $ε > 0$ with $\overline{B} ((q_{0}, 0), ε) \subseteq Ω \times R^{n}$ there is $δ > 0$ such that every maximal solution $(q, v)$ with $∥ (q (0), v (0)) - (q_{0}, 0) ∥_{2} < δ$ is defined for all $t \geq 0$ and satisfies

$∥ (q (t), v (t)) - (q_{0}, 0) ∥_{2} < ε (t \geq 0) .$

No asymptotic stability is asserted.

Facts & Assumptions

Given: The $C^{2}$ positive definite kinetic metric field $M$ , the $C^{2}$ potential $U$ , the strict local minimum $q_{0}$ and the mechanical vector field $G$ .

[F1]

$G$ is $C^{1}$ on $Ω \times R^{n}$ : the formula involves $M$ , its first derivatives, $\nabla U$ and $M^{- 1}$ , with $M^{- 1}$ having entries polynomial in the entries of $M$ divided by the nonvanishing continuous function $\det M$ ; hence $G$ is $C^{1}$ (The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart, If $\det (A)$ is a unit, then $A^{- 1} = \det (A)^{- 1} adj (A)$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative). A $C^{1}$ map is locally Lipschitz on compact coordinate subsets (A $C^{1}$ map is locally Lipschitz on compact coordinate subsets, Local Lipschitz continuity in the state variable, locally uniform in time and parameters), so every initial value problem has a unique maximal solution (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions).

[F2]

Energy conservation: for every $C^{2}$ solution $(q, v)$ of the mechanical system, $t \mapsto E (q (t), v (t))$ is constant (Energy is conserved along solutions of the mechanical system with a configuration-dependent kinetic metric).

[F3]

Compact continuation: an autonomous solution trapped in a compact subset of the open state domain near a finite endpoint extends past that endpoint (Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it).

[F4]

Compactness and extrema: closed bounded subsets of $R^{2 n}$ are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line) and a continuous real function on a nonempty compact set attains a minimum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value); the Euclidean norm is a norm, so the triangle inequality and the reverse triangle inequality hold (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation); the reverse inequality follows by applying the triangle inequality in both orders.

Proof

technique · direct; use the energy as a Lyapunov function on the boundary of a ball and extend the trapped solution by compact continuation

1.1givenF4algebra

Fix an admissible test radius $ε_{t e s t} > 0$ and choose $0 < ε \leq ε_{t e s t}$ with $ε < r_{0}$ and $\overline{B} ((q_{0}, 0), ε) \subseteq Ω \times R^{n}$ ; then the projection of the ball to the first factor lies in $\overline{B} (q_{0}, ε) \subseteq \overline{B} (q_{0}, r_{0})$ . Write $E_{0} : = E (q_{0}, 0) = U (q_{0})$ . On the sphere $S_{ε} : = {(q, v) : ∥ (q, v) - (q_{0}, 0) ∥_{2} = ε}$ the continuous function $E - E_{0}$ is strictly positive: if $v \neq 0$ then $\frac{1}{2} v^{T} M (q) v > 0$ , and if $v = 0$ then $0 < ∥ q - q_{0} ∥_{2} = ε < r_{0}$ and $U (q) > U (q_{0})$ . As $S_{ε}$ is nonempty and compact by [F4], there is $δ_{0} : = \min_{S_{ε}} (E - E_{0}) > 0$ .

2.1step 1.1F4algebra

Continuity of $E$ at $(q_{0}, 0)$ gives $δ > 0$ such that $∥ (q, v) - (q_{0}, 0) ∥_{2} < δ$ implies $E (q, v) - E_{0} < δ_{0}$ . Shrinking $δ$ further, assume $δ \leq ε$ .

3.1step 1.12.1F1F2F4algebra

Let $(q, v) : [0, b) \to Ω \times R^{n}$ be the maximal forward solution with $∥ (q (0), v (0)) - (q_{0}, 0) ∥_{2} < δ$ . Then $∥ (q (t), v (t)) - (q_{0}, 0) ∥_{2} < ε$ for all $t \in [0, b)$ . Indeed, suppose not and let $t_{1} : = \inf {t \in (0, b) : ∥ (q (t), v (t)) - (q_{0}, 0) ∥_{2} \geq ε}$ ; since the radius function is continuous with value $< ε$ at $t = 0$ and $\geq ε$ at some time, the intermediate value theorem (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ) shows that the infimum is attained with $∥ (q (t_{1}), v (t_{1})) - (q_{0}, 0) ∥_{2} = ε$ and $t_{1} > 0$ . By [F2], $E (q (t_{1}), v (t_{1})) = E (q (0), v (0))$ , so $E - E_{0}$ at time $t_{1}$ is $< δ_{0}$ by step 2.1, contradicting the definition of $δ_{0}$ on $S_{ε}$ .

4.1step 3.1F3

The solution is defined for all $t \geq 0$ : if $b < \infty$ , then the values $(q (t), v (t))$ for $t \in [0, b)$ lie in the compact set $\overline{B} ((q_{0}, 0), ε) \subseteq Ω \times R^{n}$ by step 3.1, so [F3] extends the solution past $b$ , contradicting maximality of the maximal solution (Extensions, maximal solutions, maximal intervals, and global solutions).

5.1step 2.13.14.1∎

Therefore every maximal solution starting at distance $< δ$ from $(q_{0}, 0)$ is defined for all $t \geq 0$ and stays at distance $< ε$ ; the resulting bound is also $< ε_{t e s t}$ , and since $ε_{t e s t}$ was arbitrary, $(q_{0}, 0)$ is Lyapunov stable. This is exactly the defining condition of Equilibria, Lyapunov stability and asymptotic stability of an autonomous first-order system: the $δ$ produced in step 2.1 depends only on $ε$ , not on the solution.

Remarks

The proof uses exact energy conservation to establish stability, but it does not prove attraction. In this strict-minimum setting, nearby non-equilibrium initial data have energy greater than $E (q_{0}, 0)$ ; conservation therefore prevents their solutions from converging to $(q_{0}, 0)$ . The theorem makes no asymptotic-stability claim, in contrast with An equilibrium whose linearisation has all eigenvalues in the open left half-plane is locally exponentially stable, which uses a strict Lyapunov decrease.
Neither strict positivity of the Hessian nor a Taylor expansion is used: a degenerate strict minimum such as $U (q) = ∥ q ∥_{2}^{4}$ is covered. The strictness hypothesis on the ball is essential for the positivity of $E - E_{0}$ on the sphere; a non-strict minimum with a flat direction, such as $U \equiv c o n s t$ near $q_{0}$ , would give $E - E_{0} = 0$ at points of the sphere with $v = 0$ and the argument would not apply.

A strict local minimum of the potential gives a Lyapunov stable equilibrium of the mechanical system, by energy conservation

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources