ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

Motion under linear drag and a constant applied force: explicit global solution and approach to the terminal velocity

Physical scope

A worked computation inside the linear drag model of The linear drag model: a phenomenological velocity-proportional resistance with a declared coefficient with a constant applied force: for a stated initial position and velocity the explicit motion is verified, it is the unique maximal motion and exists for all real times, and its velocity converges to the terminal velocity $(m / c) g$ with an explicit exponential bound. The item is a conditional computation inside the model; the coefficient and field parameters are declared model data, no measured value is asserted, and the phenomenological and regime qualifications of the drag postulate are preserved.

Example

Work in the linear drag model of The linear drag model: a phenomenological velocity-proportional resistance with a declared coefficient with one label of mass $m > 0$ , coefficient $c > 0$ , time window $R$ , configuration domain $Q = R^{3}$ , and a declared constant vector $g \in R^{3}$ of dimension $ℓ τ^{- 2}$ , so that the force map is $F (t, x, v) = m g - c v$ and the equation of motion is

$m \ddot{x} (t) = m g - c \dot{x} (t) .$

Define the terminal velocity

$v_{\infty} : = \frac{m}{c} g, [v_{\infty}] = ℓ τ^{- 1},$

and fix the initial datum $x (0) = x_{0}$ , $\dot{x} (0) = v_{0}$ . Verify:

the explicit curve

$x (t) = x_{0} + v_{\infty} t + \frac{m}{c} (v_{0} - v_{\infty}) (1 - e^{- c t / m})$

is a motion of the model on $R$ with the stated datum, and by uniqueness it is the maximal motion;
its velocity satisfies $\dot{x} (t) = v_{\infty} + (v_{0} - v_{\infty}) e^{- c t / m}$ for all $t$ , so that $∣ \dot{x} (t) - v_{\infty} ∣_{2} \leq ∣ v_{0} - v_{\infty} ∣_{2} e^{- c t / m}$ and $\dot{x} (t) \to v_{\infty}$ as $t \to + \infty$ : the velocity approaches the terminal velocity exponentially in time.

Facts & Assumptions

Given: The drag model with its parameters $m, c > 0$ and $g$ , the datum $(0, x_{0}, v_{0})$ , and the terminal velocity $v_{\infty} = (m / c) g$ .

[L1]

The model is a force map of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance clause (iii) by The linear drag model: a phenomenological velocity-proportional resistance with a declared coefficient clause (iii); motions, maximal motions and their uniqueness are The associated first-order system, motions, maximal motions and the Newtonian flow of a force model and Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder clauses 1, 2 and 4.

[L2]

Scalar model and its solvability: for $m > 0$ , $c \geq 0$ , $k = 0$ and constant forcing $f \equiv f_{0}$ the equation $m ξ^{''} + c ξ^{'} = f_{0}$ is the damped driven oscillator model The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $k = 0$ ; by The forced oscillator with $k \geq 0$ : unique global solution and the convolution (Green's function) formula clause 1 there is exactly one solution on $R$ through any datum $(ξ (0), ξ^{'} (0))$ , and by The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0 clause 2, for $c > 0$ the homogeneous solutions are $ξ_{h} (t) = A + B e^{- c t / m}$ with $A = ξ_{h} (0) + \frac{m}{c} ξ_{h}^{'} (0)$ and $B = - \frac{m}{c} ξ_{h}^{'} (0)$ .

[L3]

Differentiation and limits: $\frac{d}{d t} e^{μ t} = μ e^{μ t}$ (The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral for componentwise differentiation); $\exp (s) \geq 1 + s$ for every real $s$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ); $e^{- c t / m} = 1 / e^{c t / m} > 0$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ); and $0 < a < b$ implies $0 < 1 / b < 1 / a$ (Inverses of positives are positive, and reciprocation reverses order); limits at infinity are read through Limits at $+ \infty$ and $- \infty$ , and infinite limits at a point.

[L4]

The Euclidean norm satisfies the triangle inequality and absolute homogeneity (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 Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Verification

technique · direct; decompose the vector equation into scalar coordinate equations of the solved scalar model, verify the explicit formula by differentiation, and estimate the velocity difference

1.1givenL1L2algebra

The vector equation $m \ddot{x} = m g - c \dot{x}$ is, in the frame's coordinates, the three scalar equations $m {\ddot{x}}_{j} = m g_{j} - c {\dot{x}}_{j}$ for $j = 1, 2, 3$ , each the scalar model of [L2] with $k = 0$ , $c > 0$ and constant forcing $f_{0} = m g_{j}$ ; in particular each scalar initial value problem has exactly one solution on $R$ by [L2].

2.1step 1.1L2L3algebra

Candidate and its derivatives: set $v_{\infty} = (m / c) g$ and $ξ_{j} (t) : = x_{0, j} + v_{\infty, j} t + \frac{m}{c} (v_{0, j} - v_{\infty, j}) (1 - e^{- c t / m});$ then by [L3] $ξ_{j}^{'} (t) = v_{\infty, j} + (v_{0, j} - v_{\infty, j}) e^{- c t / m}$ and $ξ_{j}^{''} (t) = - \frac{c}{m} (v_{0, j} - v_{\infty, j}) e^{- c t / m}$ , so $m ξ_{j}^{''} + c ξ_{j}^{'} = - c (v_{0, j} - v_{\infty, j}) e^{- c t / m} + c v_{\infty, j} + c (v_{0, j} - v_{\infty, j}) e^{- c t / m} = c v_{\infty, j} = m g_{j},$ the scalar equation of step 1.1; moreover $ξ_{j} (0) = x_{0, j}$ and $ξ_{j}^{'} (0) = v_{\infty, j} + (v_{0, j} - v_{\infty, j}) = v_{0, j}$ .

3.1step 2.1L1L2algebra

By uniqueness in [L2] each $ξ_{j}$ is the unique scalar solution on $R$ with the datum, so the vector curve $x (t) : = (ξ_{1} (t), ξ_{2} (t), ξ_{3} (t))$ displayed in the Example satisfies the vector equation for all $t \in R$ with values in $Q = R^{3}$ and the stated datum; by The associated first-order system, motions, maximal motions and the Newtonian flow of a force model clause (c) it is a motion of the model, and it is defined on all of the time window. By Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder clauses 2 and 4 every motion with the same datum is the restriction of this one, so it is the unique maximal motion, with maximal interval $R$ ; this proves claim 1.

4.1step 2.1L3L4algebra∎

Velocity and approach to the terminal velocity: from step 2.1, $\dot{x} (t) - v_{\infty} = (v_{0} - v_{\infty}) e^{- c t / m}$ , so by [L4] $∣ \dot{x} (t) - v_{\infty} ∣_{2} = ∣ v_{0} - v_{\infty} ∣_{2} e^{- c t / m}$ for every $t$ . The factor decays to $0$ : given $ε > 0$ , for $t > \frac{m}{c} \cdot \frac{1}{ε}$ one has $\frac{c t}{m} > \frac{1}{ε}$ and hence, using $\exp (s) \geq 1 + s$ at $s = \frac{c t}{m} > 0$ , the reciprocal comparison of [L3] and $\frac{m}{c t} < ε$ , $0 < e^{- c t / m} = \frac{1}{e^{c t / m}} \leq \frac{1}{1 + c t / m} < \frac{m}{c t} < ε .$ Therefore $∣ \dot{x} (t) - v_{\infty} ∣_{2} \leq ∣ v_{0} - v_{\infty} ∣_{2} e^{- c t / m} \to 0$ as $t \to + \infty$ , i.e. $\dot{x} (t) \to v_{\infty}$ (Limits at $+ \infty$ and $- \infty$ , and infinite limits at a point); this proves claim 2.

Remarks

Terminal velocity is a model quantity. $v_{\infty} = (m / c) g$ is the velocity at which the drag force balances the applied force in this model; it is not asserted as a measured value, and both $c$ and $g$ are declared model parameters subject to the regime qualifications of The linear drag model: a phenomenological velocity-proportional resistance with a declared coefficient.
Position and compact trapping. If $g \neq 0$ , then $v_{\infty} \neq 0$ and $x (t) = v_{\infty} t + O (1)$ as $t \to + \infty$ , so the state is unbounded and the forward compact-trapping hypothesis of Maximal Newtonian motions and the compact-continuation criterion: finite-time breakdown requires escape from every compact subset of the time-state domain clause 3 is unavailable. If $g = 0$ , then $x (t) \to x_{0} + (m / c) v_{0}$ and $\dot{x} (t) \to 0$ ; the forward state is bounded and lies in a compact subset of the full state space. For $g = 0$ and $v_{0} = 0$ , the motion is stationary. In every case the explicit all-time formula establishes global existence.
Strict positivity of $c$ . The formula for $v_{\infty}$ and the computation above require $c > 0$ . For $c = 0$ the equation instead gives $\dot{x} (t) = v_{0} + g t$ : there is no finite limiting velocity when $g \neq 0$ , while for $g = 0$ the velocity is constant.

Motion under linear drag and a constant applied force: explicit global solution and approach to the terminal velocity

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources