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 amplitude of the sinusoidally forced damped oscillator: location and value of its maximum

Statement

Let $m > 0$ , $k > 0$ , $c > 0$ and $f_{0} \neq 0$ . For $Ω \geq 0$ let

$A (Ω) : = \frac{∣ f_{0} ∣}{\sqrt{(k - m Ω^{2})^{2} + c^{2} Ω^{2}}}$

be the amplitude about zero of the steady response of Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ clause 1, and put

$u_{*} : = \frac{k}{m} - \frac{c^{2}}{2 m^{2}}, Ω_{*} : = \sqrt{u_{*}} when u_{*} > 0.$

Then:

If $u_{*} > 0$ (equivalently $c^{2} < 2 m k$ ), $A$ is strictly increasing on $[0, Ω_{*}]$ , strictly decreasing on $[Ω_{*}, \infty)$ , and its maximum on $[0, \infty)$ is attained at $Ω_{*}$ and at no other point, with $A (Ω_{*}) = \frac{2 m ∣ f_{0} ∣}{c \sqrt{4 m k - c^{2}}} .$
If $u_{*} \leq 0$ then $A$ is strictly decreasing on $[0, \infty)$ and its maximum on $[0, \infty)$ is attained at $Ω = 0$ and at no other point.

Facts & Assumptions

Given: The parameters $m > 0$ , $k > 0$ , $c > 0$ , $f_{0} \neq 0$ , the amplitude function $A$ of the statement and the number $u_{*}$ .

[F1]

For every $Ω \geq 0$ the denominator $(k - m Ω^{2})^{2} + c^{2} Ω^{2}$ is strictly positive, and $A (Ω) = ∣ f_{0} ∣ / \sqrt{q (Ω^{2})}$ with $q (u) : = (k - m u)^{2} + c^{2} u$ ; this is the amplitude computed in Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ clause 1. [given]

[F2]

Derivatives: for a differentiable $F$ with $F^{'} > 0$ on an interval, $F$ is strictly increasing there, and with $F^{'} < 0$ strictly decreasing, by the mean value theorem (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ); polynomials are differentiated by the algebra of derivatives and the power rule, and composites by the chain rule. [thm-algebra-of-derivatives, lem-derivative-of-a-power, thm-chain-rule, def-interval]

[F3]

For $0 < a < b$ one has $0 < b^{- 1} < a^{- 1}$ and $0 < \sqrt{a} < \sqrt{b}$ , and $x \mapsto \sqrt{x}$ is strictly increasing on $[0, \infty)$ (Inverses of positives are positive, and reciprocation reverses order, Squaring is monotone on the nonnegatives, with nonnegative roots supplied by Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). [def-interval]

Proof

technique · cases on the sign of the minimiser; compute the quadratic exactly, locate its vertex, and convert the monotonicity through the strictly increasing square-root map followed by the strictly decreasing reciprocal map on positive arguments

1.1givenalgebra

Write $q (u) = (k - m u)^{2} + c^{2} u = m^{2} u^{2} + (c^{2} - 2 m k) u + k^{2}$ and $u_{*} = \frac{k}{m} - \frac{c^{2}}{2 m^{2}}$ . [assume-case 1, assume-case 2] Expanding $m^{2} (u - u_{*})^{2}$ and using $- 2 m^{2} u_{*} = c^{2} - 2 m k$ gives $q (u) = m^{2} (u - u_{*})^{2} + (k^{2} - m^{2} u_{*}^{2}), q^{'} (u) = 2 m^{2} (u - u_{*}),$ and the constant is $(k^{2} - m^{2} u_{*}^{2}) = (k - m u_{*}) (k + m u_{*}) = \frac{c^{2}}{2 m} \cdot \frac{4 m k - c^{2}}{2 m} = \frac{c^{2} (4 m k - c^{2})}{4 m^{2}}$ , because $k - m u_{*} = \frac{c^{2}}{2 m}$ and $k + m u_{*} = \frac{4 m k - c^{2}}{2 m}$ ; in particular $q$ is a quadratic with positive leading coefficient and unique global minimiser $u_{*}$ and $q (u_{*}) = \frac{c^{2} (4 m k - c^{2})}{4 m^{2}}$ . Also $u_{*} > 0$ if and only if $c^{2} < 2 m k$ ; in this branch $4 m k - c^{2} > 0$ , so $q (u_{*}) > 0$ . For every $u \geq 0$ , $q (u) = (k - m u)^{2} + c^{2} u > 0$ : at $u = 0$ it equals $k^{2} > 0$ , and at $u > 0$ the second summand is positive.

2.1step 1.1F2

Monotonicity of $Ω \mapsto q (Ω^{2})$ : by [F2], its derivative is $2 Ω q^{'} (Ω^{2}) = 4 m^{2} Ω (Ω^{2} - u_{*})$ . Hence if $u_{*} > 0$ this derivative is negative on $(0, Ω_{*})$ and positive on $(Ω_{*}, \infty)$ , so $q (Ω^{2})$ is strictly decreasing on $[0, Ω_{*}]$ and strictly increasing on $[Ω_{*}, \infty)$ (strictness on the closed intervals follows from [F2] on every subinterval and continuity); if $u_{*} \leq 0$ the derivative is positive on $(0, \infty)$ , so $q (Ω^{2})$ is strictly increasing on $[0, \infty)$ .

3.1step 2.1F1F3algebra∎

Conclusion. [cases-exhaustive: $u_{*} > 0$ ; $u_{*} \leq 0$ ] If $u_{*} > 0$ , then on $[0, Ω_{*}]$ the value $q (Ω^{2})$ strictly decreases to $q (Ω_{*}^{2}) = q (u_{*})$ and on $[Ω_{*}, \infty)$ it strictly increases from $q (u_{*})$ ; since $x \mapsto 1 / x$ is strictly decreasing on $(0, \infty)$ and $x \mapsto \sqrt{x}$ strictly increasing on $[0, \infty)$ by [F3], $A = ∣ f_{0} ∣ / \sqrt{q (Ω^{2})}$ is strictly increasing on $[0, Ω_{*}]$ and strictly decreasing on $[Ω_{*}, \infty)$ , so its maximum is attained exactly at $Ω_{*}$ , with $A (Ω_{*}) = ∣ f_{0} ∣ / \sqrt{q (u_{*})} = \frac{2 m ∣ f_{0} ∣}{c \sqrt{4 m k - c^{2}}}$ . If $u_{*} \leq 0$ , then $q (Ω^{2})$ is strictly increasing on $[0, \infty)$ , so $A$ is strictly decreasing there and its maximum is attained exactly at $Ω = 0$ .

Remarks

The undamped case. For $c = 0$ the same computation gives $q (u) = (k - m u)^{2}$ , whose zero is $u = k / m$ , i.e. $Ω = ω_{0} = \sqrt{k / m}$ ; there the denominator of the steady-response formula vanishes and $A$ (the modulus of the response function) is unbounded above in every neighbourhood of $ω_{0}$ meeting $[0, \infty) ∖ {ω_{0}}$ . Hence for $c = 0$ the amplitude has no maximum on $[0, \infty)$ ; it is strictly increasing on $[0, ω_{0})$ , which is the increasing branch that persists in the $c > 0$ case above. This matches the resonant case of Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ clause 2, where the response has absolute values tending to infinity along the quarter-turn sequence when $f_{0} \neq 0$ .

The amplitude of the sinusoidally forced damped oscillator: location and value of its maximum

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources