PropositionStatement: 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.

The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0

Statement

Let $m > 0$ , $c \geq 0$ , let $k \leq 0$ , and consider the model $m x^{''} + c x^{'} + k x = 0$ of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with time domain $I = R$ and forcing $f : R \to R$ identically zero. In the three cases below, $x : J \to R$ runs over solutions on intervals $J \subseteq R$ with nonempty interior.

A local solution here may have any interval $J \subseteq R$ with nonempty interior, with domain-relative derivatives at included endpoints. It has a unique extension to the global family below. A maximal solution means one that has no solution extension to a strictly larger interval; the maximal solutions of this global autonomous equation are precisely the family members on $R$ . For a homogeneous model restricted to a time domain $I$ , its solutions have $J \subseteq I$ and are restrictions of these same global members; their extensions solve the all- $R$ equation.

Double zero root ( $k = 0$ , $c = 0$ ). Then on every such interval $J$ , $x$ solves the model if and only if $x (t) = A + B t$ for some $A, B \in R$ ; each such local solution is the restriction of a unique global member of this family. For every datum $(x_{0}, v_{0})$ there is a unique global solution on $R$ with $x (0) = x_{0}$ , $x^{'} (0) = v_{0}$ , namely $x (t) = x_{0} + v_{0} t$ .
Simple zero root ( $k = 0$ , $c > 0$ ). Then on every such interval $J$ , $x$ solves the model if and only if $x (t) = A + B e^{- c t / m}$ for some $A, B \in R$ ; each such local solution is the restriction of a unique global member of this family. For every datum $(x_{0}, v_{0})$ there is a unique global solution on $R$ with $x (0) = x_{0}$ , $x^{'} (0) = v_{0}$ , namely the member with $A = x_{0} + \frac{m v_{0}}{c}$ and $B = - \frac{m v_{0}}{c}$ . This global solution has limit $A$ as $t \to + \infty$ ; any local solution on an interval unbounded above has the same limit along that interval.
One positive and one negative root ( $k < 0$ ). Put $λ_{\pm} : = \frac{- c \pm \sqrt{c^{2} - 4 m k}}{2 m} .$ Then $λ_{-} < 0 < λ_{+}$ , both are real roots of the characteristic polynomial, and on every such interval $J$ , $x$ solves the model if and only if $x (t) = A e^{λ_{+} t} + B e^{λ_{-} t}$ for some $A, B \in R$ ; each such local solution is the restriction of a global member of this family. In particular the global solution $t \mapsto e^{λ_{+} t}$ has data $x (0) = 1$ , $x^{'} (0) = λ_{+}$ and satisfies $e^{λ_{+} t} \to + \infty$ as $t \to + \infty$ : the model has an unbounded solution growing exponentially on $[0, \infty)$ .

Facts & Assumptions

Given: The parameters $m > 0$ , $c \geq 0$ , $k \leq 0$ , the model of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $I = R$ , $f \equiv 0$ and phase field $G_{0} (x, v) = (v, - (c v + k x) / m)$ , and the constants $λ_{\pm}$ of case 3.

[F1]

The model, its solutions and the phase-plane system are those of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $I = R$ and $f \equiv 0$ ; $x$ is a solution on $J$ exactly when $t \mapsto (x (t), x^{'} (t))$ solves $z^{'} = G_{0} (z)$ on $J$ , and for $k \leq 0$ the field $G_{0} (x, v) = (v, - (c v + k x) / m)$ is linear, hence continuous and globally Lipschitz in the state variable. [given]

[F2]

Local uniqueness: Continuous and Lipschitz dependence on the initial condition on a Picard-Lindelof cylinder in the form used before: for the Lipschitz field $G_{0}$ , any two solutions of $z^{'} = G_{0} (z)$ defined on a common interval and taking the same value at one point agree on that interval (this is its "exactly one solution through given data with graph in a Picard-Lindelof cylinder" clause together with the cylinder-local uniqueness, applied along the interval). [given]

[F3]

Derivative rules: $(e^{μ t})^{'} = μ e^{μ t}$ for real $μ$ ; sums and products are differentiated by the algebra of derivatives and the chain rule. [thm-derivative-of-exponential, thm-algebra-of-derivatives, thm-chain-rule]

[F4]

A differentiable function on an interval with identically zero derivative is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant). [def-interval]

[F5]

Fundamental theorem of calculus for continuous integrands: if $G$ is a primitive of a continuous $u$ on an interval containing $a$ and $t$ , then for $a < t$ the evaluation clause of Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ gives $\int_{a}^{t} u = G (t) - G (a)$ . For $t < a$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ gives $\int_{a}^{t} u = - \int_{t}^{a} u = - (G (a) - G (t))$ by the same clause on $[t, a]$ ; for $t = a$ both sides vanish. Thus the formula holds for every ordering of $a, t$ .

[F6]

The real exponential is strictly increasing, and its image is $(0, \infty)$ . [thm-exponential-is-strictly-increasing, cor-exponential-is-a-bijection-onto-positive-reals]

Proof

technique · cases; identify the solution families in the three degenerate/repulsive cases, then obtain uniqueness from the local uniqueness lemma

1.1F1F3F4

Case $k = 0$ , $c = 0$ . [assume-case 1] The model is $m x^{''} = 0$ . By [F4], $x^{'}$ is a constant $B$ on $J$ , and $x (t) - B t$ has zero derivative, hence is a constant $A$ on $J$ . Thus every solution on an arbitrary interval is $A + B t$ , and conversely each such function solves by [F3]. For a global solution the data at zero give $A = x_{0}$ , $B = v_{0}$ .

1.2F1F3F4F5F6algebra

Case $k = 0$ , $c > 0$ . [assume-case 2] Put $u = x^{'}$ . By [F3], $(e^{c t / m} u)^{'} = e^{c t / m} (u^{'} + (c / m) u) = 0$ , so [F4] gives $u (t) = D e^{- c t / m}$ for a constant $D$ on $J$ . Fix $a \in J^{\circ}$ . Applying [F5] to the primitives $x$ and $- (m D / c) e^{- c t / m}$ of $u$ gives $x (t) - x (a) = - (m D / c) (e^{- c t / m} - e^{- c a / m})$ for every $t \in J$ . Hence $(x (t) + (m D / c) e^{- c t / m})^{'} = 0$ and $x (t) = A + B e^{- c t / m}$ for constants $A, B$ with $B = - m D / c$ , without requiring $0 \in J$ . Conversely this family solves by [F3] and extends globally. Its extension is unique: if two such global members agree on $J$ , their difference $A_{1} - A_{2} + (B_{1} - B_{2}) e^{- c t / m}$ vanishes on the nonempty open interval $J^{\circ}$ ; differentiating there and using $c > 0$ and $e^{- c t / m} > 0$ gives $B_{1} = B_{2}$ , then $A_{1} = A_{2}$ . On the global member, data at zero give $B = - m v_{0} / c$ and $A = x_{0} + m v_{0} / c$ . The exponential term tends to zero at $+ \infty$ by monotonicity and surjectivity of the exponential in [F6]: for any $η > 0$ , choose $r \in R$ with $e^{r} = η$ ; whenever $t > \max {0, - m r / c}$ , $- c t / m < r$ and $0 < e^{- c t / m} < η$ . Thus the global extension has limit $A$ ; when $J$ is unbounded above, the original solution agrees with this extension on its positive-time tail and has the same limit.

1.3givenF3F6algebra

Case $k < 0$ . [assume-case 3] Here $c^{2} - 4 m k > c^{2} \geq 0$ , so $\sqrt{c^{2} - 4 m k} > c$ and $λ_{+} > 0 > λ_{-}$ ; the completing-square identity $m λ^{2} + c λ + k = m [(λ + \frac{c}{2 m})^{2} - \frac{c^{2} - 4 m k}{4 m^{2}}]$ shows that $λ_{\pm}$ are exactly the two real roots of the characteristic polynomial. For a real root $μ$ , $t \mapsto e^{μ t}$ solves the model because $m μ^{2} + c μ + k = 0$ and $(e^{μ t})^{''} = μ^{2} e^{μ t}$ by [F3]; by linearity every $A e^{λ_{+} t} + B e^{λ_{-} t}$ solves it. Finally $e^{λ_{+} t} \to + \infty$ as $t \to + \infty$ : given $R > 0$ , surjectivity in [F6] gives $u$ with $e^{u} > R$ , and monotonicity gives $e^{λ_{+} t} \geq e^{u} > R$ for all $t \geq u / λ_{+}$ .

2.1step 1.1step 1.2step 1.3F1F2F3algebra∎

Uniqueness and exhaustiveness. [cases-exhaustive: $k = 0, c = 0$ ; $k = 0, c > 0$ ; $k < 0$ ] Cases 1 and 2 exhaust the arbitrary-interval solution sets by steps 1.1 and 1.2. In case 3 choose any $t_{0} \in J^{\circ}$ . The value/derivative matrix of $e^{λ_{+} t}$ and $e^{λ_{-} t}$ at $t_{0}$ has determinant $(λ_{-} - λ_{+}) e^{(λ_{+} + λ_{-}) t_{0}} \neq 0$ , so a unique global family member $y$ matches $(x (t_{0}), x^{'} (t_{0}))$ . By [F1] the full phase curves solve the same system, and [F2] gives equality on $J$ : cylinder-local uniqueness propagates on the connected interior using the closed-and-open set where both phase components agree, then extends to included endpoints by continuity. Thus $x = y ∣_{J}$ . Each explicit family is defined on $R$ , its coefficient/data map at zero is invertible, and these exhaust all solutions, proving global existence and uniqueness for prescribed data. The repulsive member with data $(1, λ_{+})$ grows without bound by step 1.3. Because every interval solution has a unique all- $R$ extension and $R$ has no larger real time interval, these global family members are exactly the maximal solutions. Restricting them to $J \subseteq I$ gives the solutions of a restricted homogeneous model on $I$ .

The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources