Pipeline-generated

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.

Cm Math Approximation — Examples

1 · Prerequisites

2 · Summary

The companion page to cm-math-approximation gathers explicit worked checks for its oscillator, forcing, linearization, averaging and adiabatic results. Everything here is mathematics: the items carry domain: mathematics, depend only on mathematical suppliers, and make no physical or empirical claim.

Five worked initial value problems for the homogeneous oscillator across the discriminant, degenerate and repulsive cases solves five initial value problems of the homogeneous model, one in each discriminant case and in the degenerate $k \leq 0$ cases; Resonant forcing at $Ω = ω_{0}$ and the two regimes of the amplitude maximum checks the resonant solution $\frac{1}{2} t \sin t$ of $x^{''} + x = \cos t$ and evaluates the amplitude maximum in its two regimes; Constant forcing: free fall and the approach to terminal velocity under linear drag treats constant forcing with the convolution formula, including the approach to terminal velocity under linear drag. Finite-time linearization bound for the planar pendulum with explicit constants verifies the quadratic remainder and growth constants for $F (θ, ω) = (ω, - \sin θ)$ on the ball of radius $1 / 2$ and evaluates the resulting error bound for a small datum. Averaging estimate on $[0, 100]$ for the scalar equation $x^{'} = ε \cos t$ computes the average and deviation for $f (t, x) = \cos t$ , checks the trapping hypothesis, and compares the theorem's bound with the exact solution on $[0, 100]$ ; An exactly solvable adiabatic branch: $K = I + ε I \cos θ$ and comparison with the drift bound exhibits the exactly invariant quantity $I (1 + ε \cos θ)$ for the branch $K = I + ε I \cos θ$ , verifies the trapping in the stated action window, and evaluates the drift bound. Continuity alone does not give uniqueness: $x^{'} = \sqrt{∣ x ∣}$ through the origin is the counterexample $x^{'} = \sqrt{∣ x ∣}$ through the origin, showing that continuity of the field cannot replace the Lipschitz hypothesis in the uniqueness results, and A bounded field whose solution leaves the domain in finite time: $x^{'} = v$ , $v^{'} = 0$ on $(0, \infty) \times (- 2, 2)$ shows a solution of a bounded field leaving its domain at a finite time.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Five worked initial value problems for the homogeneous oscillator across the discriminant, degenerate and repulsive cases

Example

In each line, $m = 1$ and the initial datum $(x_{0}, v_{0})$ is prescribed for the homogeneous model with time domain $I = R$ and zero forcing, $x^{''} + c x^{'} + k x = 0$ (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data). The solution is read off from the classification theorem and the degenerate-case proposition, and its initial values are checked explicitly.

(i) $k = 4$ , $c = 0$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = \cos (2 t)$ .
(ii) $k = 1$ , $c = 2$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = (1 + t) e^{- t}$ .
(iii) $k = 1$ , $c = 3$ , $(x_{0}, v_{0}) = (1, 0)$ : with $λ_{\pm} = (- 3 \pm \sqrt{5}) / 2$ the solution is $x (t) = (- λ_{-} e^{λ_{+} t} + λ_{+} e^{λ_{-} t}) / \sqrt{5}$ .
(iv) $k = 0$ , $c = 2$ , $(x_{0}, v_{0}) = (0, 1)$ : the solution is $x (t) = \frac{1}{2} (1 - e^{- 2 t})$ .
(v) $k = - 1$ , $c = 0$ , $(x_{0}, v_{0}) = (1, 0)$ : the solution is $x (t) = \frac{1}{2} (e^{t} + e^{- t})$ , which is unbounded on $[0, \infty)$ .

Facts & Assumptions

Given: The homogeneous model of The damped driven oscillator model: second-order equation, phase-plane system and characteristic data with $m = 1$ and the parameters of the five lines.

[L1]

For $k > 0$ the solutions are classified by the sign of $Δ = c^{2} - 4 m k$ as in The homogeneous damped oscillator: solution classification by the discriminant and uniqueness for initial data: distinct real roots in case 1, a double root $λ = - c / (2 m)$ in case 2, and the family $e^{- γ t} (A \cos ω t + B \sin ω t)$ with $γ = c / (2 m)$ , $ω = \sqrt{k / m - γ^{2}}$ in case 3; clause 4 gives the coefficient formulas $A = (v_{0} - λ_{-} x_{0}) / (λ_{+} - λ_{-})$ , $B = (λ_{+} x_{0} - v_{0}) / (λ_{+} - λ_{-})$ in case 1; $A = x_{0}$ , $B = v_{0} - λ x_{0}$ in case 2; $A = x_{0}$ , $B = (v_{0} + γ x_{0}) / ω$ in case 3. [given]

[L2]

For $k \leq 0$ the solutions are those of The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0: for $k = 0$ , $c > 0$ they are $A + B e^{- c t / m}$ with $A = x_{0} + v_{0} m / c$ , $B = - v_{0} m / c$ ; for $k < 0$ they are $A e^{λ_{+} t} + B e^{λ_{-} t}$ with $λ_{\pm} = (- c \pm \sqrt{c^{2} - 4 m k}) / (2 m)$ , $λ_{-} < 0 < λ_{+}$ , and $e^{λ_{+} t} \to + \infty$ . [given]

[L3]

$(\cos t)^{'} = - \sin t$ , $(\sin t)^{'} = \cos t$ , and $(e^{μ t})^{'} = μ e^{μ t}$ for real $μ$ . [thm-sine-and-cosine-derivatives, thm-derivative-of-exponential]

Verification

technique · direct; compute the discriminant and coefficients in each line and check the initial data

1.1givenL1L3algebra

Line (i): $Δ = 0 - 16 < 0$ and $γ = 0$ , $ω = \sqrt{4} = 2$ , so by [L1] case 3 the solution is $A \cos 2 t + B \sin 2 t$ with $A = x_{0} = 1$ , $B = (v_{0} + γ x_{0}) / ω = 0$ ; by [L3] the candidate $\cos (2 t)$ has value $1$ and derivative $- 2 \sin (2 t)$ vanishing at $0$ , so it is the solution.

1.2givenL1L3algebra

Line (ii): $Δ = 4 - 4 = 0$ , so the double root is $λ = - 1$ and the family is $(A + B t) e^{- t}$ with $A = x_{0} = 1$ , $B = v_{0} - λ x_{0} = 1$ ; the candidate $(1 + t) e^{- t}$ has the value $1$ and derivative $e^{- t} - (1 + t) e^{- t} = - t e^{- t}$ equal to $0$ at $t = 0$ , matching $(x_{0}, v_{0}) = (1, 0)$ .

1.3givenL1algebra

Line (iii): $Δ = 5 > 0$ and $λ_{\pm} = (- 3 \pm \sqrt{5}) / 2$ with $λ_{+} - λ_{-} = \sqrt{5}$ and $λ_{+} + λ_{-} = - 3$ ; the coefficients of [L1] case 1 are $A = (v_{0} - λ_{-} x_{0}) / \sqrt{5} = - λ_{-} / \sqrt{5}$ and $B = (λ_{+} x_{0} - v_{0}) / \sqrt{5} = λ_{+} / \sqrt{5}$ , so the solution is $x (t) = A e^{λ_{+} t} + B e^{λ_{-} t} = (- λ_{-} e^{λ_{+} t} + λ_{+} e^{λ_{-} t}) / \sqrt{5}$ . Then $x (0) = (λ_{+} - λ_{-}) / \sqrt{5} = 1$ and $x^{'} (0) = λ_{+} A + λ_{-} B = (- λ_{+} λ_{-} + λ_{-} λ_{+}) / \sqrt{5} = 0$ , matching $(x_{0}, v_{0}) = (1, 0)$ .

1.4givenL2L3algebra

Line (iv): $k = 0$ , $c = 2 > 0$ , and [L2] gives $x (t) = A + B e^{- 2 t}$ with $A = 0 + 1 / 2 = 1 / 2$ , $B = - 1 / 2$ , that is $x (t) = \frac{1}{2} (1 - e^{- 2 t})$ ; its derivative is $e^{- 2 t}$ by [L3], so $x (0) = 0$ and $x^{'} (0) = 1$ .

2.1givenL2L3algebra∎

Line (v): $k = - 1 < 0$ and $λ_{\pm} = \pm 1$ by [L2]; the solution with data $(1, 0)$ is $\frac{1}{2} e^{t} + \frac{1}{2} e^{- t}$ (the coefficients $A = B = 1 / 2$ solve $A + B = 1$ , $A - B = 0$ ), and it is unbounded on $[0, \infty)$ because $e^{t} \to + \infty$ , in accordance with [L2].

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Resonant forcing at $Ω = ω_{0}$ and the two regimes of the amplitude maximum

Example

Consider the forced model $m x^{''} + c x^{'} + k x = f_{0} \cos (Ω t)$ on time domain $I = R$ with the values and conclusions below (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data, Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ , The amplitude of the sinusoidally forced damped oscillator: location and value of its maximum).

(i) Resonance: $m = k = f_{0} = 1$ , $c = 0$ , $Ω = ω_{0} = 1$ . Then $x_{p} (t) = \frac{1}{2} t \sin t$ is a solution of $x^{''} + x = \cos t$ , it satisfies $x_{p} (0) = 0$ , $x_{p}^{'} (0) = 0$ , and $∣ x_{p} ∣$ is unbounded on $[0, \infty)$ .
(ii) Amplitude peak above zero frequency: $m = k = f_{0} = 1$ , $c = 1$ . Then $u_{*} = 1 - \frac{1}{2} = \frac{1}{2} > 0$ , the maximum of $A (Ω) = 1 / \sqrt{(1 - Ω^{2})^{2} + Ω^{2}}$ is attained at $Ω_{*} = 1 / \sqrt{2}$ , and $A (Ω_{*}) = 2 / \sqrt{3}$ , while $A (0) = A (1) = 1$ .
(iii) Amplitude peak at zero frequency: $m = k = f_{0} = 1$ , $c = 2$ . Then $u_{*} = 1 - 2 = - 1 \leq 0$ , and the maximum of $A (Ω) = 1 / \sqrt{(1 - Ω^{2})^{2} + 4 Ω^{2}}$ on $[0, \infty)$ is attained at $Ω = 0$ with value $1$ , while $A (1) = 1 / 2$ .

Facts & Assumptions

Given: The five parameters in each line and the steady-response formulae of Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ clause 1 and The amplitude of the sinusoidally forced damped oscillator: location and value of its maximum.

[L1]

In the resonant case $c = 0$ , $Ω = ω_{0} = \sqrt{k / m}$ the function $x_{p} (t) = f_{0} t \sin (ω_{0} t) / (2 m ω_{0})$ is a solution of the forced model on $R$ and is unbounded on $[0, \infty)$ when $f_{0} \neq 0$ (Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ clause 2). [given]

[L2]

If $c > 0$ the amplitude of the steady response is $A (Ω) = ∣ f_{0} ∣ / \sqrt{(k - m Ω^{2})^{2} + c^{2} Ω^{2}}$ ; its maximum is attained at $Ω_{*} = \sqrt{u_{*}}$ when $u_{*} = k / m - c^{2} / (2 m^{2}) > 0$ , with value $2 m ∣ f_{0} ∣ / (c \sqrt{4 m k - c^{2}})$ , and at $Ω = 0$ when $u_{*} \leq 0$ (The amplitude of the sinusoidally forced damped oscillator: location and value of its maximum; the connection to the steady response is clause 1 of Sinusoidal forcing: the steady response, its amplitude and phase, and resonance at $Ω = \sqrt{k / m}$ ). [given]

[L3]

$(\sin t)^{'} = \cos t$ , $(\cos t)^{'} = - \sin t$ ; sums and products are differentiated by the algebra of derivatives and the chain rule. [thm-sine-and-cosine-derivatives, thm-algebra-of-derivatives, thm-chain-rule]

Verification

technique · direct; substitute the resonant candidate, and evaluate the amplitude formula in the two regimes of the preceding proposition

1.1givenL1L3algebra

Line (i): with $m = ω_{0} = f_{0} = 1$ the candidate is $x_{p} (t) = \frac{1}{2} t \sin t$ ; by [L3], $x_{p}^{'} (t) = \frac{1}{2} (\sin t + t \cos t)$ and $x_{p}^{''} (t) = \frac{1}{2} (2 \cos t - t \sin t) = \cos t - \frac{1}{2} t \sin t$ , so $x_{p}^{''} + x_{p} = \cos t$ , as required, and $x_{p} (0) = 0 = x_{p}^{'} (0)$ . At $t_{k} = π / 2 + 2 π k$ one has $\sin t_{k} = 1$ and $∣ x_{p} (t_{k}) ∣ = t_{k} / 2 \to \infty$ , so $x_{p}$ is unbounded on $[0, \infty)$ , in agreement with [L1].

1.2givenL2algebra

Line (ii): here $u_{*} = 1 - 1 / 2 = 1 / 2 > 0$ and $4 m k - c^{2} = 3$ , so [L2] locates the maximum at $Ω_{*} = 1 / \sqrt{2}$ with value $2 / \sqrt{3}$ ; directly, $(1 - Ω_{*}^{2})^{2} + Ω_{*}^{2} = (1 / 2)^{2} + 1 / 2 = 3 / 4$ , so $A (Ω_{*}) = 2 / \sqrt{3}$ , while $A (0) = 1$ and $A (1) = 1 / \sqrt{0 + 1} = 1$ , both below $2 / \sqrt{3}$ .

2.1givenL2algebra∎

Line (iii): here $u_{*} = 1 - 2 = - 1 \leq 0$ , so [L2] locates the maximum at $0$ with value $A (0) = 1 / \sqrt{1} = 1$ ; directly, $A (1) = 1 / \sqrt{(0)^{2} + 4} = 1 / 2 < 1$ , and the same formula gives $A (Ω) \leq 1$ for all $Ω \geq 0$ because $(1 - Ω^{2})^{2} + 4 Ω^{2} = 1 + 2 Ω^{2} + Ω^{4} \geq 1$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Constant forcing: free fall and the approach to terminal velocity under linear drag

Example

Let $m > 0$ , $g \in R$ and consider the two constant-forcing models with time domain $I = R$ (the half-line solution in (ii) is the restriction of its global solution) (The damped driven oscillator model: second-order equation, phase-plane system and characteristic data).

(i) Uniform force: $x^{''} = g$ with data $x (0) = x_{0}$ , $x^{'} (0) = v_{0}$ . The unique solution is $x (t) = x_{0} + v_{0} t + \frac{1}{2} g t^{2}$ .
(ii) Linear drag: $m = 1$ , $c = 2$ , $g = 1$ , that is $x^{''} + 2 x^{'} = 1$ , with data $(x_{0}, v_{0}) = (0, 0)$ . The unique solution on $[0, \infty)$ is $x (t) = \frac{1}{2} t - \frac{1}{4} (1 - e^{- 2 t})$ , and its velocity $x^{'} (t) = \frac{1}{2} (1 - e^{- 2 t})$ increases to the limiting value $\frac{1}{2}$ .

Facts & Assumptions

Given: The parameters $m, g$ and the data of the two lines; the forced oscillator theorem applies in both since $k = 0 \geq 0$ and the forcing is constant, hence continuous.

[L1]

For $m > 0$ , $c \geq 0$ , $k \geq 0$ and continuous $f$ , the unique solution of $m x^{''} + c x^{'} + k x = f$ with data $(x_{0}, v_{0})$ at $t_{0} = 0$ is $x = x_{h} + \int_{0}^{t} g (t - s) f (s) d s$ , where $x_{h}$ is the homogeneous solution with the data and $g$ is the homogeneous kernel with $g (0) = 0$ , $g^{'} (0) = 1 / m$ ; for $k = c = 0$ one has $g (u) = u / m$ , and for $k = 0$ , $c > 0$ one has $g (u) = (1 - e^{- c u / m}) / c$ (The forced oscillator with $k \geq 0$ : unique global solution and the convolution (Green's function) formula, The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0). [given]

[L2]

For $k = 0$ the homogeneous solutions are $x_{h} (t) = A + B e^{- c t / m}$ when $c > 0$ and $x_{h} (t) = A + B t$ when $c = 0$ , with $A = x_{0} + v_{0} m / c$ , $B = - v_{0} m / c$ respectively $A = x_{0}$ , $B = v_{0}$ (The degenerate and repulsive oscillator: solutions for k=0 and the explicit growing solution for k<0). [given]

[L3]

$(e^{μ t})^{'} = μ e^{μ t}$ for real $μ$ , and sums and scalar multiples are differentiated termwise. [thm-derivative-of-exponential, thm-algebra-of-derivatives]

Verification

technique · direct; read the solutions off the convolution formula in the two degenerate cases and differentiate

1.1givenL1L2algebra

Line (i): here $c = k = 0$ , so [L1] gives $g (u) = u / m$ and $x_{h} (t) = x_{0} + v_{0} t$ by [L2]; hence $x (t) = x_{0} + v_{0} t + \int_{0}^{t} \frac{t - s}{m} m g d s = x_{0} + v_{0} t + g \int_{0}^{t} (t - s) d s = x_{0} + v_{0} t + \frac{1}{2} g t^{2},$ because $\int_{0}^{t} (t - s) d s = t^{2} / 2$ .

1.2givenL1L2algebra

Line (ii): here $m = 1$ , $c = 2$ , $k = 0$ and $f \equiv 1$ ; by [L1], $g (u) = (1 - e^{- 2 u}) / 2$ , and the datum $(0, 0)$ gives $x_{h} = 0$ by [L2]. Hence $x (t) = \int_{0}^{t} \frac{1 - e^{- 2 (t - s)}}{2} d s = \frac{t}{2} - \frac{1}{4} (1 - e^{- 2 t}) .$

2.1step 1.1step 1.2L3algebra∎

Velocity: by [L3], $x^{'} (t) = \frac{1}{2} - \frac{1}{4} \cdot 2 e^{- 2 t} = \frac{1}{2} (1 - e^{- 2 t})$ , so $x^{'} (0) = 0$ and $x^{'} (t) \to \frac{1}{2}$ as $t \to + \infty$ because $e^{- 2 t} \to 0$ ; moreover $x^{''} (t) = e^{- 2 t}$ , so $x^{''} + 2 x^{'} = e^{- 2 t} + 1 - e^{- 2 t} = 1$ , confirming both lines satisfy their equations with the prescribed data.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Finite-time linearization bound for the planar pendulum with explicit constants

Example

Let $l = g = 1$ and consider the planar pendulum field

$F : R^{2} \to R^{2}, F (θ, ω) = (ω, - \sin θ),$

Let $A : R^{2} \to R^{2}$ be the linear map $A (θ, ω) : = (ω, - θ)$ , and let $A = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array}) \in M_{2} (R)$ be its standard-coordinate matrix; use the matrix action of $A$ from Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate. On the closed ball $\overline{B} (0, \frac{1}{2})$ one has

$∥ F (z) - A z ∥_{2} \leq \frac{1}{12} ∥ z ∥_{2}^{2}, ∥ F (z) ∥_{2} \leq ∥ z ∥_{2},$

so the linearization theorem applies with $r = \frac{1}{2}$ , $C = \frac{1}{12}$ , $L = 1$ . For the datum $z_{0} = (\frac{1}{100}, 0)$ and $T = 1$ one has $δ e^{L T} = \frac{e}{100} < \frac{3}{100} < \frac{1}{20} < \frac{1}{2}$ , and the theorem bounds the linearization error by

$∥ z (t) - y (t) ∥_{2} \leq \frac{δ^{2}}{12} \int_{0}^{1} e^{(1 - s)} e^{2 s} d s < 10^{- 4} (0 \leq t \leq 1),$

where $y$ solves $y^{'} = A y$ , $y (0) = z_{0}$ ; in particular the linear solution stays within $10^{- 4}$ of the nonlinear one on $[0, 1]$ .

Facts & Assumptions

Given: The field $F$ , the matrix $A$ , the radius $r = 1 / 2$ , the datum $z_{0} = (1 / 100, 0)$ and the horizon $T = 1$ .

[L1]

The linearization theorem (Finite-time linearization error bound: quadratic remainder, exponential growth bound and the variation-of-constants estimate): if $U \subseteq R^{n}$ is open, $0 \in U$ , $F : U \to R^{n}$ is continuous and locally Lipschitz in the state variable, $r, T > 0$ , $C, L \geq 0$ , $\overline{B} (0, r) \subseteq U$ , $δ = ∥ z_{0} ∥_{2} > 0$ , and $∥ F (z) - A z ∥_{2} \leq C ∥ z ∥_{2}^{2}$ and $∥ F (z) ∥_{2} \leq L ∥ z ∥_{2}$ for $∥ z ∥_{2} \leq r$ and $δ e^{L T} < r$ , then the nonlinear solution exists on $[0, T]$ and $∥ z (t) - y (t) ∥_{2} \leq C δ^{2} \int_{0}^{t} e^{∥ A ∥ (t - s)} e^{2 L s} d s$ for $t \in [0, T]$ . [given]

[L2]

Taylor remainder bound: if $f$ has derivatives through order $n + 1$ on the closed interval between $a$ and $x$ , with endpoint continuity, and $∣ f^{(n + 1)} ∣ \leq M$ there, then $∣ R_{n, a} f (x) ∣ \leq M ∣ x - a ∣^{n + 1} / (n + 1)!$ (A uniform derivative bound gives a uniform Taylor remainder bound); with $f = \sin$ , $n = 2$ , $a = 0$ and $M = 1$ this gives $∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6$ , since $∣ \sin^{'''} ∣ = ∣ \cos ∣ \leq 1$ (The derivatives of sine and cosine are cosine and minus sine, Signs, monotonicity intervals, and ranges of sine and cosine). [given]

[L3]

Operator norm: $∥ A ∥ = \sup_{∥ u ∥_{2} = 1} ∥ A u ∥_{2}$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum); for $A = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ and $u = (u_{1}, u_{2})$ one has $A u = (u_{2}, - u_{1})$ , so $∥ A u ∥_{2} = ∥ u ∥_{2}$ and $∥ A ∥ = 1$ . [given]

[L4]

$2 < e < 3$ (The elementary numerical bound $2 < e < 3$ ); the exponential is positive, increasing and satisfies $e^{x + y} = e^{x} e^{y}$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ); and $∣ \cos u ∣ \leq 1$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[L6]

The mean value theorem used below is 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)$ .

[L5]

The integral is monotone for continuous real integrands (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ), and $\int_{0}^{1} 9 d s = 9$ by the constant-integral formula (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Verification

technique · direct; estimate the two remainder terms of the pendulum field on the ball and substitute the explicit constants into the theorem

1.1givenL2algebra

Quadratic remainder: for $z = (θ, ω)$ with $∥ z ∥_{2} \leq 1 / 2$ , $F (z) - A z = (0, - \sin θ) - (0, - θ) = (0, θ - \sin θ),$ so $∥ F (z) - A z ∥_{2} = ∣ \sin θ - θ ∣ \leq ∣ θ ∣^{3} / 6 \leq \frac{1}{2} ∣ θ ∣^{2} / 6 \leq \frac{1}{12} ∥ z ∥_{2}^{2}$ by [L2] and $∣ θ ∣ \leq ∥ z ∥_{2} \leq 1 / 2$ ; hence $C = 1 / 12$ is admissible.

1.2givenL1L3L4L6algebra

Regularity and growth: $U = R^{2}$ is open and contains $\overline{B} (0, 1 / 2)$ . The differentiable sine and coordinate functions make $F$ continuous. For $z = (θ, ω)$ and $w = (η, ν)$ , [L6] and [L4] give $∣ \sin θ - \sin η ∣ \leq ∣ θ - η ∣$ , hence $∥ F (z) - F (w) ∥_{2}^{2} = (ω - ν)^{2} + (\sin θ - \sin η)^{2} \leq ∥ z - w ∥_{2}^{2}$ . Thus $F$ is globally $1$ -Lipschitz and in particular locally Lipschitz in the state variable. Growth bound: if $θ \neq 0$ , 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)$ ) applied to $\sin$ between $0$ and $θ$ , with $∣ \cos ∣ \leq 1$ from [L4], gives $∣ \sin θ ∣ = ∣ \sin θ - \sin 0 ∣ \leq ∣ θ ∣$ ; this inequality is immediate at $θ = 0$ . Thus $∥ F (z) ∥_{2}^{2} = ω^{2} + \sin^{2} θ \leq ω^{2} + θ^{2} = ∥ z ∥_{2}^{2}$ , so $L = 1$ is admissible. With $δ = 1 / 100$ and $T = 1$ , [L4] gives $δ e^{L T} = e / 100 < 3 / 100 < 1 / 20 < 1 / 2 = r$ , so the hypotheses of [L1] hold.

2.1step 1.1step 1.2L1L3L4L5algebra∎

Substitute: by [L1] and [L3], for $0 \leq t \leq 1$ the error is at most $\frac{1}{12} δ^{2} \int_{0}^{t} e^{(1 - s)} e^{2 s} d s \leq \frac{1}{12} δ^{2} \int_{0}^{1} e^{(1 - s)} e^{2 s} d s$ , since $e^{t - s} \leq e^{1 - s}$ for $s \leq t \leq 1$ and the resulting integrand is positive by [L4]. The addition formula gives $e^{(1 - s)} e^{2 s} = e^{1 + s}$ ; since $0 \leq s \leq 1$ , monotonicity gives $e^{1 + s} \leq e^{2} < 9$ by [L4]. Monotonicity of the integral [L5] therefore yields $\int_{0}^{1} e^{1 + s} d s \leq 9$ , and the error is at most $\frac{1}{12} \cdot 10^{- 4} \cdot 9 = \frac{3}{4} \cdot 10^{- 4} < 10^{- 4}$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Averaging estimate on $[0, 100]$ for the scalar equation $x^{'} = ε \cos t$

Example

Take $n = 1$ , $P = 2 π$ , $O = R$ , $f (t, x) = \cos t$ (independent of $x$ ), $x_{0} = 0$ , and the trapping data $R = 1$ , $ρ = \frac{1}{2}$ , $A = 1$ . Then $f$ is continuous, $C^{1}$ in $x$ with $D_{x} f = 0$ , and $2 π$ -periodic in $t$ ; on $R \times \overline{B} (0, 1)$ one may take $M = 1$ and $L = 0$ . The average and deviation of Periodic averaging data: the average field, the oscillatory part and the periodic deviation are

$\overset{ˉ}{f} = 0, g (t, x) = \sin t (0 \leq t \leq 2 π, extended 2 π -periodically) .$

The averaged system is $y^{'} = 0$ , so $y (t) \equiv 0$ solves it and stays in $\overline{B} (0, \frac{1}{2})$ . With $B = 2 M P = 4 π$ , $B_{1} = 2 L P = 0$ and $K = e^{L A} [B + (L B + B_{1} M) A] = 4 π$ , the smallness hypothesis reads $ε \cdot 4 π < \frac{1}{2}$ ; for $ε = \frac{1}{100}$ it holds because $ε K = \frac{π}{25} < \frac{1}{2}$ . The averaging theorem then gives

$∣ x (t) - y (t) ∣ = ∣ x (t) ∣ \leq \frac{π}{25} (0 \leq t \leq 100) .$

The exact solution is $x (t) = \frac{1}{100} \sin t$ , whose modulus is at most $\frac{1}{100}$ ; the theorem's bound is valid but not sharp here.

Facts & Assumptions

Given: The data above and the scalar ODE $x^{'} = ε \cos t$ , $x (0) = 0$ .

[L1]

For this $f$ , $\overset{ˉ}{f} (x) = \frac{1}{2 π} \int_{0}^{2 π} \cos s d s = 0$ and $g (t, x) = \int_{0}^{t} \cos s d s = \sin t$ on $[0, 2 π]$ , extended periodically; this is the construction of Periodic averaging data: the average field, the oscillatory part and the periodic deviation, evaluated with the fundamental theorem for continuous integrands (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$ , The derivatives of sine and cosine are cosine and minus sine); the endpoint values $\sin 0 = \sin (2 π) = 0$ and periodicity used here are supplied by [L4]. [given]

[L2]

The averaging theorem (Averaging for fast periodic oscillations: order- $ε$ agreement on the $O (1 / ε)$ time scale): under its hypotheses with a solution $y : [0, A / ε] \to \overline{B} (x_{0}, R - ρ)$ of the averaged system and $ε K < ρ$ , the solution $x$ of $x^{'} = ε f (t, x)$ , $x (0) = x_{0}$ exists on $[0, A / ε]$ and satisfies $∥ x (t) - y (t) ∥_{2} \leq ε K$ there, with $K = e^{L A} [B + (L B + B_{1} M) A]$ , $B = 2 M P$ , $B_{1} = 2 L P$ . [given]

[L3]

The definition $π = 2 γ$ and theorem $0 < γ < 2$ give $0 < π < 4$ (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two).

[L4]

Sine and cosine are $2 π$ -periodic, and $\sin (2 π) = \sin 0 = 0$ by their zero set (The zero sets of sine and cosine and the least positive common period 2 pi). Their ranges are $[- 1, 1]$ (Signs, monotonicity intervals, and ranges of sine and cosine); in particular $∣ \cos t ∣, ∣ \sin t ∣ \leq 1$ . Their differentiability in [L1] gives continuity.

Verification

technique · direct; evaluate the averaging data, check the hypotheses, and compare the bound with the exact solution

1.1givenL1L3L4algebra

By [L4], the continuous field $f (t, x) = \cos t$ is $2 π$ -periodic and bounded by one; its state derivative is zero, so $M = 1$ and $L = 0$ meet the hypotheses on $O = R$ . By [L1], $\overset{ˉ}{f} = 0$ and $g (t, x) = \sin t$ , so the averaged system is $y^{'} = 0$ ; the constant curve $y \equiv 0$ is its solution with $y (0) = 0$ on $[0, 100]$ , and $∥ y (t) - 0 ∥ = 0 \leq R - ρ = \frac{1}{2}$ . The constants are $M = 1$ , $L = 0$ , $B = 4 π$ , $B_{1} = 0$ , $K = e^{0} [4 π + 0] = 4 π$ , and with $ε = \frac{1}{100}$ , [L3] gives $ε K = \frac{π}{25} < \frac{4}{25} < 1 / 2 = ρ$ .

2.1step 1.1L1L2L4algebra∎

By [L2] the solution $x$ of $x^{'} = \frac{1}{100} \cos t$ , $x (0) = 0$ exists on $[0, 100]$ and satisfies $∣ x (t) ∣ \leq \frac{π}{25}$ there. Directly, the primitive $\sin t$ gives $x (t) = \frac{1}{100} \sin t$ by [L1], so $∣ x (t) ∣ \leq \frac{1}{100}$ by [L4]; the stated bound holds and is not attained.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

An exactly solvable adiabatic branch: $K = I + ε I \cos θ$ and comparison with the drift bound

Example

Take $J = R$ , $S = R$ , $h (I, s) = I$ and $k (I, θ, s) = I \cos θ$ in the datum of A one-frequency parameter-dependent action-angle branch, its transformed Hamiltonian and its drift generator, with $ε = \frac{1}{10}$ , $A = 2$ , $ω_{0} = 1$ , $K = [6 / 5, 19 / 10]$ , $S_{0} = [0, 2]$ , $s_{0} = 0$ and initial datum $I (0) = 3 / 2$ , $θ (0) = 0$ . The branch system is

$I^{'} = ε I \sin θ, θ^{'} = 1 + ε \cos θ, s^{'} = ε,$

so $s (t) = ε t$ stays in $S_{0} = [0, 2]$ on $[0, A / ε] = [0, 20]$ , and $I (t)$ stays in $K$ for all $t \geq 0$ . The quantity $J : = I (1 + ε \cos θ)$ is exactly invariant, the solution stays in $K \times S_{0}$ on $[0, A / ε]$ , and

$∣ I (t) - I (0) ∣ \leq \frac{1}{3} (t \geq 0),$

while the drift bound of Adiabatic action drift bound: order- $ε$ change of the action on the $O (1 / ε)$ time scale evaluates in this instance to $∣ I (t) - I (0) ∣ \leq \frac{19}{50}$ .

Facts & Assumptions

Given: The datum $h (I, s) = I$ , $k (I, θ, s) = I \cos θ$ , $ε = 1 / 10$ , and the sets and data above.

[L1]

The branch vector field is $I^{'} = - ε \partial_{θ} k$ , $θ^{'} = \partial_{I} h + ε \partial_{I} k$ , $s^{'} = ε$ ; here $\partial_{I} h = 1$ , $\partial_{θ} k = - I \sin θ$ and $\partial_{I} k = \cos θ$ , so the field is as displayed (A one-frequency parameter-dependent action-angle branch, its transformed Hamiltonian and its drift generator). [given]

[L2]

The drift bound (Adiabatic action drift bound: order- $ε$ change of the action on the $O (1 / ε)$ time scale): if $∣ \partial_{I} h ∣ \geq ω_{0}$ and the branch solution stays in the compact sets $K \times S_{0}$ , then $∣ I (t) - I (0) ∣ \leq ε [2 \sup_{K \times [0, 2 π] \times S_{0}} ∣ g ∣ + A \sup_{K \times [0, 2 π] \times S_{0}} ∣ \partial_{I} g \partial_{θ} k - \partial_{θ} g \partial_{I} k - \partial_{s} g ∣],$ where $g = (k - ⟨ k ⟩) / \partial_{I} h$ and $⟨ k ⟩$ is the $θ$ -average of $k$ . [given]

[L3]

$(\sin θ)^{'} = \cos θ$ and $(\cos θ)^{'} = - \sin θ$ , and derivatives of sums and products follow the algebra of derivatives and the chain rule. (The derivatives of sine and cosine are cosine and minus sine, 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$ )

[L4]

$∣ \sin θ ∣ \leq 1$ and $∣ \cos θ ∣ \leq 1$ for all real $θ$ (Signs, monotonicity intervals, and ranges of sine and cosine); the mean value theorem then gives $∣ \sin θ - \sin ϑ ∣ \leq ∣ θ - ϑ ∣$ and $∣ \cos θ - \cos ϑ ∣ \leq ∣ θ - ϑ ∣$ (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)$ ).

[L5]

Local Lipschitz continuity in the state variable is the neighborhood-uniform state-Lipschitz property of Local Lipschitz continuity in the state variable, locally uniform in time and parameters. For a continuous field with this property on an open ODE domain, there is a unique maximal solution through each datum, and a solution of an autonomous field whose state remains in a compact subset of its open state domain near a finite endpoint extends past that endpoint (First-order systems, initial value problems, and solutions on intervals, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, Extensions, maximal solutions, maximal intervals, and global solutions, 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).

[L6]

If a differentiable vector-valued curve on a compact interval has derivative norm at most $C$ , then its endpoint difference has norm at most $C$ times the interval length (If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz).

[L7]

The zero-derivative constancy fact used below is 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: a differentiable real function on an interval whose derivative vanishes is constant.

Verification

technique · direct; exhibit an exact invariant of the branch system, check the trapping, and evaluate the theorem's constant

1.1L1L4L5algebra

Write the branch field as $V (I, θ, s) = (\frac{1}{10} I \sin θ, 1 + \frac{1}{10} \cos θ, \frac{1}{10})$ . On each cube $C_{N} = [- N, N]^{3}$ with $N > 0$ , [L4] gives, for $p = (I, θ, s)$ and $q = (I^{'}, ϑ, s^{'})$ , $∣ I \sin θ - I^{'} \sin ϑ ∣ \leq ∣ I - I^{'} ∣ + N ∣ θ - ϑ ∣, ∣ \cos θ - \cos ϑ ∣ \leq ∣ θ - ϑ ∣ .$ Hence $∥ V (p) - V (q) ∥_{2} \leq \frac{1}{10} (∣ I - I^{'} ∣ + (N + 1) ∣ θ - ϑ ∣) \leq \frac{N + 2}{10} ∥ p - q ∥_{2}$ . Thus $V$ is continuous and locally Lipschitz on its open domain $R^{3}$ ; by [L5] there is a unique maximal solution $(I, θ, s) : (α, β) \to R^{3}$ through the stated datum.

2.1step 1.1L1L3L7algebra

Along the maximal solution of step 1.1, [L1] gives $I^{'} = \frac{1}{10} I \sin θ$ , $θ^{'} = 1 + \frac{1}{10} \cos θ$ , $s^{'} = \frac{1}{10}$ . Put $J (t) : = I (t) (1 + \frac{1}{10} \cos θ (t))$ . By [L3], $J^{'} = \frac{1}{10} I \sin θ (1 + \frac{1}{10} \cos θ) + I (- \frac{1}{10} \sin θ) (1 + \frac{1}{10} \cos θ) = 0,$ so [L7] makes $J$ constant; with $I (0) = 3 / 2$ , $θ (0) = 0$ we get $J \equiv \frac{33}{20}$ .

3.1step 1.1step 2.1L2L4L5L6algebra

Trapping and global forward existence: on $[0, β)$ , step 2.1 and [L4] give $9 / 10 \leq 1 + \frac{1}{10} \cos θ (t) \leq 11 / 10$ and hence $\frac{3}{2} = \frac{33}{20} \cdot \frac{10}{11} \leq I (t) = \frac{33 / 20}{1 + \frac{1}{10} \cos θ (t)} \leq \frac{33}{20} \cdot \frac{10}{9} = \frac{11}{6} .$ Also $∣ θ^{'} (t) ∣ \leq 11 / 10$ and $∣ s^{'} (t) ∣ = 1 / 10$ , so [L6] gives $∣ θ (t) ∣ \leq 11 t / 10$ and $s (t) = t / 10$ . If $β < + \infty$ , the state curve near $β$ stays in the compact subset $[\frac{3}{2}, \frac{11}{6}] \times [- \frac{11 β}{10}, \frac{11 β}{10}] \times [0, \frac{β}{10}]$ of $R^{3}$ ; the autonomous compact-continuation clause of [L5] extends the maximal solution past $β$ , a contradiction. Hence $β = + \infty$ . Since $s (t) = t / 10$ , on $[0, 20] = [0, A / ε]$ we have $s (t) \in S_{0}$ , and the bounds above place $I (t)$ strictly inside $K = [6 / 5, 19 / 10]$ . Thus the solution stays in $K \times S_{0}$ on the required horizon, and [L2] applies.

4.1step 2.1step 3.1L2algebra∎

Evaluate the theorem's constant: $⟨ k ⟩ (I, s) = \frac{1}{2 π} \int_{0}^{2 π} I \cos θ d θ = 0$ , so $g = I \cos θ$ and $\sup_{K \times [0, 2 π] \times S_{0}} ∣ g ∣ = \frac{19}{10}$ . Moreover $\partial_{I} g = \cos θ$ , $\partial_{θ} g = - I \sin θ$ , $\partial_{s} g = 0$ , and with $\partial_{θ} k = - I \sin θ$ , $\partial_{I} k = \cos θ$ one has $\partial_{I} g \partial_{θ} k - \partial_{θ} g \partial_{I} k - \partial_{s} g = - I \cos θ \sin θ + I \sin θ \cos θ = 0$ . The theorem thus gives $∣ I (t) - I (0) ∣ \leq \frac{1}{10} \cdot 2 \cdot \frac{19}{10} = \frac{19}{50}$ , while the exact invariant gives $∣ I (t) - I (0) ∣ = \frac{1}{10} \cdot \frac{3}{2} \frac{∣ \cos θ (0) - \cos θ (t) ∣}{1 + \frac{1}{10} \cos θ (t)} \leq \frac{1}{10} \cdot \frac{3}{2} \cdot \frac{2}{9 / 10} = \frac{1}{3},$ consistent with the bound.

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passOpen item page →

Continuity alone does not give uniqueness: $x^{'} = \sqrt{∣ x ∣}$ through the origin

Statement refuted

Let $F : R \to R$ be continuous. Then for every $x_{0} \in R$ the initial value problem $x^{'} = F (x)$ , $x (0) = x_{0}$ has at most one solution on every interval containing $0$ .

Facts & Assumptions

Given: The field $F (x) = \sqrt{∣ x ∣}$ and the initial value problem $x^{'} = F (x)$ , $x (0) = 0$ .

[L1]

A solution on an interval $I$ is a differentiable $x : I \to R$ with $x^{'} (t) = F (x (t))$ for every $t \in I$ and $x (0) = 0$ (First-order systems, initial value problems, and solutions on intervals, 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). [given]

[L2]

$u \mapsto ∣ u ∣$ and $u \mapsto \sqrt{u}$ (on $[0, \infty)$ ) are continuous, and sums, products and compositions of continuous functions are continuous; squaring is continuous by the polynomial clause of Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, injective on $[0, \infty)$ by Squaring is monotone on the nonnegatives, and onto $[0, \infty)$ by Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , so $\sqrt{\cdot}$ is its continuous inverse on $[0, \infty)$ (Absolute value in an ordered field, Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ , Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point). [given]

[L3]

$(u^{2})^{'} = 2 u$ , and the chain rule and algebra of derivatives differentiate compositions, products and sums (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, 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$ ). [given]

Counterexample

technique · direct; exhibit two distinct solutions through the same initial datum

1.1givenL2

The map $F (x) = \sqrt{∣ x ∣}$ is continuous on $R$ as the composition of $u \mapsto ∣ u ∣$ with the square root, by [L2], so the hypothesis of the refuted statement holds.

1.2givenL1

The zero function $x_{0} \equiv 0$ is a solution: it is differentiable with derivative $0 = F (0)$ everywhere.

1.3givenL3algebra

Define $x_{1} : R \to R$ by $x_{1} (t) = 0$ for $t \leq 1$ and $x_{1} (t) = (t - 1)^{2} / 4$ for $t \geq 1$ . Then $x_{1}$ is continuous, and it is differentiable at $t = 1$ with derivative $0$ from both sides: for $h > 0$ , $(h^{2} / 4) / h = h / 4 \to 0$ , while the left difference quotient is $0$ . For $t \neq 1$ the derivative is $0$ (for $t < 1$ ) or $(t - 1) / 2$ (for $t > 1$ ) by [L3]. Hence $x_{1}$ is differentiable on $R$ with $x_{1} (0) = 0$ .

2.1step 1.2step 1.3L1L2algebra∎

For $t > 1$ , $x_{1} (t) = (t - 1)^{2} / 4 \geq 0$ and $(t - 1) / 2 > 0$ , so uniqueness of the nonnegative square root in [L2] gives $\sqrt{∣ x_{1} (t) ∣} = (t - 1) / 2 = x_{1}^{'} (t)$ ; for $t \leq 1$ , $x_{1} (t) = 0$ and $x_{1}^{'} (t) = 0 = \sqrt{∣ 0 ∣}$ . Hence $x_{1}$ is a solution of $x^{'} = F (x)$ through $(0, 0)$ by [L1], and it differs from the zero solution on $(1, \infty)$ : the initial value problem has two distinct solutions on every interval containing $[0, 2]$ , refuting the statement.

Remarks

Why the Lipschitz hypothesis matters. The local uniqueness lemma Continuous and Lipschitz dependence on the initial condition on a Picard-Lindelof cylinder assumes a state-Lipschitz constant; here $F$ fails that hypothesis at the equilibrium: $∣ F (x) - F (0) ∣ / ∣ x ∣ = 1 / \sqrt{∣ x ∣} \to \infty$ as $x \to 0$ . The counterexample shows that continuity alone cannot replace it, so the Lipschitz hypothesis in the oscillator existence and uniqueness results is not redundant.
No physical claim. This is a statement about an abstract scalar ODE; it makes no assertion about any mechanical model.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A bounded field whose solution leaves the domain in finite time: $x^{'} = v$ , $v^{'} = 0$ on $(0, \infty) \times (- 2, 2)$

Example

Let $U = (0, \infty) \times (- 2, 2) \subseteq R^{2}$ and let $F : U \to R^{2}$ , $F (x, v) = (v, 0)$ , so that the first-order system $(x, v)^{'} = F (x, v)$ is the free particle with velocity $v$ (The local flow of an autonomous first-order system). The solution of $z^{'} = F (z)$ , $z (0) = (1, - 1)$ is

$z (t) = (x (t), v (t)) = (1 - t, - 1), t \in (- \infty, 1) .$

Its maximal interval of existence is $(- \infty, 1)$ : at $t = 1$ the position reaches the excluded boundary value $x = 0$ , although $∥ F (x, v) ∥ = ∣ v ∣ < 2$ is bounded on $U$ and the field extends smoothly to the plane. Hence a finite maximal interval does not require the field to blow up; the domain can force it.

Facts & Assumptions

Given: The domain $U = (0, \infty) \times (- 2, 2)$ , the field $F (x, v) = (v, 0)$ , and the datum $z_{0} = (1, - 1)$ .

[L1]

$F$ is continuous and locally Lipschitz in the state variable; the flow, maximal solutions and maximal intervals are those of The local flow of an autonomous first-order system and Extensions, maximal solutions, maximal intervals, and global solutions; every initial value problem has a unique maximal solution, and every other solution through the same data is a restriction of it (Every Picard–Lindelöf initial value problem has one maximal solution on an open interval, First-order systems, initial value problems, and solutions on intervals). A solution on an interval $I$ must satisfy $(t, z (t)) \in R \times U$ for every $t \in I$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). [given]

Verification

technique · direct; verify the explicit solution, then show no extension past $t=1$ can meet the domain condition

1.1givenL1algebra

The curve $z (t) = (1 - t, - 1)$ is defined for $t < 1$ and lies in $R \times U$ there because $1 - t > 0$ and $- 1 \in (- 2, 2)$ ; it is differentiable with $z^{'} (t) = (- 1, 0) = F (z (t))$ for every $t < 1$ , and $z (0) = (1, - 1)$ . So it is a solution on $(- \infty, 1)$ .

2.1step 1.1L1algebra∎

Maximality: suppose a solution $ζ$ through $(1, - 1)$ were defined on an interval containing some $t_{0} > 1$ . By [L1] it agrees with $z$ on the overlap of their intervals and is continuous at $t = 1$ , so $ζ (1) = \lim_{t ↑ 1} (1 - t, - 1) = (0, - 1)$ , i.e. its position is $0$ at time $1$ ; but then $(1, ζ (1)) = (1, (0, - 1))$ does not lie in $R \times U$ , contradicting the domain condition for a solution on that interval. Hence no solution through the datum is defined at $t_{0} > 1$ , while $z$ is defined at every $t < 1$ ; the maximal interval is exactly $(- \infty, 1)$ . In particular the maximal solution escapes the domain at the finite time $1$ with $∥ F (x, v) ∥ = ∣ v ∣ < 2$ bounded on $U$ , so boundedness of the field alone does not guarantee a global solution.

Cm Math Approximation — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

Five worked initial value problems for the homogeneous oscillator across the discriminant, degenerate and repulsive cases

Example

Facts & Assumptions

Verification

Resonant forcing at Ω=ω0Ω=ω0​ and the two regimes of the amplitude maximum

Example

Facts & Assumptions

Verification

Constant forcing: free fall and the approach to terminal velocity under linear drag

Example

Facts & Assumptions

Verification

Finite-time linearization bound for the planar pendulum with explicit constants

Example

Facts & Assumptions

Verification

Averaging estimate on [0,100][0,100] for the scalar equation x′=εcos⁡tx′=εcost

Example

Facts & Assumptions

Verification

An exactly solvable adiabatic branch: K=I+εIcos⁡θK=I+εIcosθ and comparison with the drift bound

Example

Facts & Assumptions

Verification

Continuity alone does not give uniqueness: x′=∣x∣x′=∣x∣​ through the origin

Statement refuted

Facts & Assumptions

Counterexample

Remarks

A bounded field whose solution leaves the domain in finite time: x′=vx′=v, v′=0v′=0 on (0,∞)×(−2,2)(0,∞)×(−2,2)

Example

Facts & Assumptions

Verification

Sources

Resonant forcing at $Ω = ω_{0}$ and the two regimes of the amplitude maximum

Averaging estimate on $[0, 100]$ for the scalar equation $x^{'} = ε \cos t$

An exactly solvable adiabatic branch: $K = I + ε I \cos θ$ and comparison with the drift bound

Continuity alone does not give uniqueness: $x^{'} = \sqrt{∣ x ∣}$ through the origin

A bounded field whose solution leaves the domain in finite time: $x^{'} = v$ , $v^{'} = 0$ on $(0, \infty) \times (- 2, 2)$