From fbf30bbbbbb37809da3a88d2cc0f7beb79695600 Mon Sep 17 00:00:00 2001 From: Giuseppe Sorge Date: Wed, 1 Jul 2026 22:56:22 +0200 Subject: [PATCH 1/3] feat(ClassicalMechanics): add Caldirola-Kanai lagrangian for damped oscillator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds section F to DampedHarmonicOscillator/Basic.lean: - lagrangian: the Caldirola-Kanai lagrangian exp(γ/m t) * (T - V), with lagrangian_eq, lagrangian_eq_exp_mul_kineticEnergy_sub_potentialEnergy, lagrangian_of_isUndamped, contDiff_lagrangian - gradient_lagrangian_position_eq / gradient_lagrangian_velocity_eq via the helper gradient_const_mul - gradLagrangian: the variational gradient of the action, simplified by gradLagrangian_eq_force to exp(γ/m t) • (F - m a) - equationOfMotion_iff_gradLagrangian_zero: the equation of motion holds iff the variational gradient vanishes Adds Time.val_contDiff (@[fun_prop]) to SpaceAndTime/Time/Derivatives.lean, completing the measurable/differentiable/contDiff API for Time.val. Marks the lagrangian, variational-gradient, and (inherited) kinetic/potential energy requirements done in API-map.yaml. Toward #905. Co-Authored-By: Claude Fable 5 --- .../DampedHarmonicOscillator/API-map.yaml | 22 +- .../DampedHarmonicOscillator/Basic.lean | 217 ++++++++++++++++++ Physlib/SpaceAndTime/Time/Derivatives.lean | 5 + 3 files changed, 236 insertions(+), 8 deletions(-) diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml index 8099e60f9..0b10e4f84 100644 --- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml +++ b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml @@ -82,22 +82,28 @@ Requirements: location: Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean (trajectory_equationOfMotion) - description: The API shall contain the definition of the kinetic energy. - done: false - location: N/A + done: true + location: > + Inherited from Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (kineticEnergy), + since DampedHarmonicOscillator extends HarmonicOscillator. - description: The API shall contain the definition of the potential energy. - done: false - location: N/A + done: true + location: > + Inherited from Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (potentialEnergy), + since DampedHarmonicOscillator extends HarmonicOscillator. - description: The API shall contain the definition of the Lagrangian. - done: false - location: N/A + done: true + location: Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean (lagrangian) - description: > The API shall contain a simplification of the variational gradient of the Lagrangian to the Euler-Lagrange equations. - done: false - location: N/A + done: true + location: > + Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean + (gradLagrangian, gradLagrangian_eq_force, equationOfMotion_iff_gradLagrangian_zero) - description: > The API shall prove that the selected trajectory is the unique solution of the diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index 897b98f92..b37b320b9 100644 --- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -48,6 +48,10 @@ In the `Basic` module: - `angularFrequency` selects the real frequency parameter from the damping regime. - `toUndamped_equationOfMotion` relates the damped and undamped equations of motion when the damping coefficient is zero. +- `lagrangian` defines the Caldirola–Kanai lagrangian `exp (γ/m * t) * (T - V)`. +- `gradLagrangian` defines the variational gradient of the corresponding action, and + `equationOfMotion_iff_gradLagrangian_zero` shows that its vanishing is equivalent to + the equation of motion. In the `Solution` module: - `InitialConditions` contains the initial position and velocity. @@ -64,6 +68,14 @@ In the `Solution` module: - C.2. Equation of motion if and only if Newton's second law - D. Damping regimes - E. To undamped oscillator +- F. The Caldirola–Kanai lagrangian and the equation of motion + - F.1. The lagrangian + - F.1.1. Equalities for the lagrangian + - F.1.2. Smoothness of the lagrangian + - F.1.3. Gradients of the lagrangian + - F.2. The variational gradient of the action + - F.2.1. The variational gradient and Newton's second law + - F.3. Equation of motion iff the variational gradient vanishes ## iv. References @@ -71,6 +83,10 @@ References for the damped harmonic oscillator include: - Landau & Lifshitz, Mechanics, page 76, section 25. - Goldstein, Classical Mechanics, Chapter 2. +References for the Caldirola–Kanai lagrangian include: +- Caldirola, Nuovo Cimento 18 (1941) 393. +- Kanai, Progress of Theoretical Physics 3 (1948) 440. + -/ @[expose] public section @@ -457,6 +473,207 @@ lemma toUndamped_equationOfMotion (S : DampedHarmonicOscillator) (hS : S.IsUndam _ = force S xₜ t := by simp [force, HarmonicOscillator.force_eq_linear, toUndamped, hγ] +/-! + +## F. The Caldirola–Kanai lagrangian and the equation of motion + +The damped harmonic oscillator is not conservative, so the undamped lagrangian +`T - V` does not reproduce the damped equation of motion. Instead we use the +Caldirola–Kanai lagrangian, which multiplies the undamped lagrangian by the +time-dependent factor `exp (γ/m * t)`: + +$$L(t, x, v) = e^{(\gamma/m) t}\left(\frac{1}{2} m \|v\|^2 - \frac{1}{2} k \|x\|^2\right)$$ + +Setting the variational gradient of the corresponding action equal to zero +recovers exactly the damped equation of motion `m ẍ + γ ẋ + k x = 0`. + +-/ + +/-! + +### F.1. The lagrangian + +We define the Caldirola–Kanai lagrangian as the lagrangian of the underlying +undamped harmonic oscillator multiplied by the exponential factor `exp (γ/m * t)`. + +-/ + +/-- The Caldirola–Kanai lagrangian of the damped harmonic oscillator. It is the +lagrangian of the underlying undamped harmonic oscillator multiplied by the +time-dependent factor `exp (γ/m * t)`. -/ +noncomputable def lagrangian (t : Time) (x v : EuclideanSpace ℝ (Fin 1)) : ℝ := + exp (S.γ / S.m * t) * S.toHarmonicOscillator.lagrangian t x v + +/-! + +#### F.1.1. Equalities for the lagrangian + +We prove some simple equalities for the lagrangian, in particular that when applied to a +trajectory it is the exponential factor times the kinetic energy minus the potential energy, +and that it reduces to the undamped lagrangian when the damping coefficient is zero. + +-/ + +lemma lagrangian_eq : S.lagrangian = fun (t : Time) (x v : EuclideanSpace ℝ (Fin 1)) => + exp (S.γ / S.m * t) * (1 / (2 : ℝ) * S.m * ⟪v, v⟫_ℝ - 1 / (2 : ℝ) * S.k * ⟪x, x⟫_ℝ) := by + funext t x v + rw [lagrangian, S.toHarmonicOscillator.lagrangian_eq] + +lemma lagrangian_eq_exp_mul_kineticEnergy_sub_potentialEnergy (t : Time) + (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : + S.lagrangian t (xₜ t) (∂ₜ xₜ t) = + exp (S.γ / S.m * t) * (S.kineticEnergy xₜ t - S.potentialEnergy (xₜ t)) := by + rw [lagrangian, S.toHarmonicOscillator.lagrangian_eq_kineticEnergy_sub_potentialEnergy] + +/-- When the damping coefficient is zero, the Caldirola–Kanai lagrangian is the +lagrangian of the underlying undamped harmonic oscillator. -/ +lemma lagrangian_of_isUndamped (hS : S.IsUndamped) : + S.lagrangian = S.toHarmonicOscillator.lagrangian := by + have hγ : S.γ = 0 := by simpa [IsUndamped] using hS + funext t x v + rw [lagrangian, hγ] + simp + +/-! + +#### F.1.2. Smoothness of the lagrangian + +The lagrangian is smooth in all its arguments. + +-/ + +@[fun_prop] +lemma contDiff_lagrangian (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.lagrangian := by + have h : ↿S.lagrangian = + fun p : Time × EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) => + exp (S.γ / S.m * p.1) * ↿S.toHarmonicOscillator.lagrangian p := rfl + rw [h] + fun_prop + +/-! + +#### F.1.3. Gradients of the lagrangian + +We now show results related to the gradients of the lagrangian with respect to the +position and velocity. They follow from the corresponding gradients of the undamped +lagrangian, using that the gradient scales with the constant `exp (γ/m * t)`. + +-/ + +lemma gradient_const_mul {f : EuclideanSpace ℝ (Fin 1) → ℝ} {x : EuclideanSpace ℝ (Fin 1)} + (c : ℝ) (hf : DifferentiableAt ℝ f x) : + gradient (fun y => c * f y) x = c • gradient f x := by + unfold gradient + rw [fderiv_const_mul hf] + simp [map_smul] + +lemma gradient_lagrangian_position_eq (t : Time) (x v : EuclideanSpace ℝ (Fin 1)) : + gradient (fun x => S.lagrangian t x v) x = -(exp (S.γ / S.m * t) * S.k) • x := by + have hf : DifferentiableAt ℝ (fun y => S.toHarmonicOscillator.lagrangian t y v) x := by + simp only [HarmonicOscillator.lagrangian_eq] + fun_prop + have h_eq : (fun y => S.lagrangian t y v) = + fun y => exp (S.γ / S.m * t) * S.toHarmonicOscillator.lagrangian t y v := rfl + rw [h_eq, gradient_const_mul _ hf, + S.toHarmonicOscillator.gradient_lagrangian_position_eq] + module + +lemma gradient_lagrangian_velocity_eq (t : Time) (x v : EuclideanSpace ℝ (Fin 1)) : + gradient (S.lagrangian t x) v = (exp (S.γ / S.m * t) * S.m) • v := by + have hf : DifferentiableAt ℝ (fun w => S.toHarmonicOscillator.lagrangian t x w) v := by + simp only [HarmonicOscillator.lagrangian_eq] + fun_prop + have h_eq : S.lagrangian t x = + fun w => exp (S.γ / S.m * t) * S.toHarmonicOscillator.lagrangian t x w := rfl + rw [h_eq, gradient_const_mul _ hf, + S.toHarmonicOscillator.gradient_lagrangian_velocity_eq, smul_smul] + +/-! + +### F.2. The variational gradient of the action + +We now write down the variational gradient of the action of the damped harmonic +oscillator, for a trajectory $x(t)$ this is equal to + +$$t\mapsto \left.\frac{\partial L(t, \dot x (t), q)}{\partial q}\right|_{q = x(t)} - + \frac{d}{dt} \left.\frac{\partial L(t, v, x(t))}{\partial v}\right|_{v = \dot x (t)}$$ + +Setting this equal to zero corresponds to the Euler-Lagrange equations, and thereby the +equation of motion. + +-/ + +/-- The variational gradient of the action of the damped harmonic oscillator. -/ +noncomputable def gradLagrangian (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : + Time → EuclideanSpace ℝ (Fin 1) := + (δ (q':=xₜ), ∫ t, S.lagrangian t (q' t) (fderiv ℝ q' t 1)) + +lemma gradLagrangian_eq_eulerLagrangeOp (xₜ : Time → EuclideanSpace ℝ (Fin 1)) + (hq : ContDiff ℝ ∞ xₜ) : + S.gradLagrangian xₜ = eulerLagrangeOp S.lagrangian xₜ := by + rw [gradLagrangian, + ClassicalMechanics.euler_lagrange_varGradient _ _ hq (S.contDiff_lagrangian _)] + +/-! + +#### F.2.1. The variational gradient and Newton's second law + +We simplify the variational gradient of the action to the exponential factor times +the difference between the force and mass times acceleration. + +-/ + +private lemma deriv_exp_smul (a : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1)) + (hy : Differentiable ℝ y) (t : Time) : + ∂ₜ (fun t' : Time => exp (a * t'.val) • y t') t = + exp (a * t.val) • (∂ₜ y t + a • y t) := by + rw [Time.deriv] + rw [fderiv_fun_smul (by fun_prop) (hy t)] + rw [fderiv_exp (by fun_prop), fderiv_fun_mul (by fun_prop) (by fun_prop)] + simp only [_root_.add_apply, _root_.smul_apply, + ContinuousLinearMap.smulRight_apply, Time.fderiv_val, smul_eq_mul, mul_one] + rw [← Time.deriv_eq] + simp [smul_add, smul_smul] + +/-- The variational gradient of the Caldirola–Kanai action is the exponential factor +times the difference of the force and mass times acceleration appearing in +Newton's second law. -/ +lemma gradLagrangian_eq_force (xₜ : Time → EuclideanSpace ℝ (Fin 1)) + (hx : ContDiff ℝ ∞ xₜ) : + S.gradLagrangian xₜ = fun t : Time => + exp (S.γ / S.m * t) • (force S xₜ t - S.m • ∂ₜ (∂ₜ xₜ) t) := by + have hdx : Differentiable ℝ (∂ₜ xₜ) := deriv_differentiable_of_contDiff xₜ hx + funext t + rw [gradLagrangian_eq_eulerLagrangeOp S xₜ hx, eulerLagrangeOp] + have h2 : ∂ₜ (fun t' => gradient (S.lagrangian t' (xₜ t') ·) (∂ₜ xₜ t')) t = + exp (S.γ / S.m * t) • (S.m • ∂ₜ (∂ₜ xₜ) t + S.γ • ∂ₜ xₜ t) := by + conv_lhs => + arg 1 + ext t' + rw [gradient_lagrangian_velocity_eq, ← smul_smul] + rw [deriv_exp_smul (S.γ / S.m) (fun t' => S.m • ∂ₜ xₜ t') (hdx.const_smul S.m) t] + rw [Time.deriv_smul _ _ hdx, smul_smul, div_mul_cancel₀ _ S.m_ne_zero] + rw [gradient_lagrangian_position_eq, h2, force] + module + +/-! + +### F.3. Equation of motion iff the variational gradient vanishes + +The equation of motion of the damped harmonic oscillator holds if and only if the +variational gradient of the Caldirola–Kanai action vanishes, since the exponential +factor is never zero. + +-/ + +lemma equationOfMotion_iff_gradLagrangian_zero (xₜ : Time → EuclideanSpace ℝ (Fin 1)) + (hx : ContDiff ℝ ∞ xₜ) : + S.EquationOfMotion xₜ ↔ S.gradLagrangian xₜ = 0 := by + rw [S.equationOfMotion_iff_newtons_2nd_law xₜ, gradLagrangian_eq_force S xₜ hx, funext_iff] + refine forall_congr' fun t => ?_ + simp only [Pi.zero_apply, smul_eq_zero, Real.exp_ne_zero, false_or, sub_eq_zero] + exact eq_comm + end DampedHarmonicOscillator end ClassicalMechanics diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 00c2dd385..7a489b20f 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -163,6 +163,11 @@ lemma deriv_const [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) : open MeasureTheory ContDiff InnerProductSpace Time +@[fun_prop] +lemma val_contDiff {n : WithTop ℕ∞} : ContDiff ℝ n Time.val := by + change ContDiff ℝ n toRealCLM + fun_prop + @[fun_prop] lemma deriv_differentiable_of_contDiff {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (f : Time → M) (hf : ContDiff ℝ ∞ f) : From 105b93a566e83d594141020a735e06f89f7852e5 Mon Sep 17 00:00:00 2001 From: Giuseppe Sorge Date: Wed, 1 Jul 2026 23:11:34 +0200 Subject: [PATCH 2/3] docs(ClassicalMechanics): apply review fixes to Caldirola-Kanai section - fix transposed L(t, x, v) arguments in the F.2 variational-gradient formula - mark gradient_const_mul private (mirrors HarmonicOscillator's private helper) - pack gradLagrangian_eq_force signature onto one line (HO precedent) - sync API-map.yaml Overview and References with the new section F - retitle Time/Derivatives section D to cover Time.val_contDiff Toward #905. Co-Authored-By: Claude Fable 5 --- .../DampedHarmonicOscillator/API-map.yaml | 8 ++++++-- .../DampedHarmonicOscillator/Basic.lean | 9 ++++----- Physlib/SpaceAndTime/Time/Derivatives.lean | 4 ++-- 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml index 0b10e4f84..90a63358b 100644 --- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml +++ b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml @@ -15,8 +15,10 @@ Overview: | equivalence with Newton's second law, the rate of mechanical-energy dissipation along solutions, the three damping regimes (underdamped, critically damped, overdamped) selected by the sign of the discriminant `γ² - 4 m k` together with - the decay rate and regime-selected angular frequency, and the reduction to the - undamped harmonic oscillator when `γ = 0`. The `Solution` module defines the + the decay rate and regime-selected angular frequency, the reduction to the + undamped harmonic oscillator when `γ = 0`, and the Caldirola–Kanai lagrangian + `exp (γ/m * t) * (T - V)`, whose variational gradient vanishes if and only if + the equation of motion holds. The `Solution` module defines the initial conditions, the explicit closed-form `trajectory` selected from the damping regime (trigonometric, polynomial, or hyperbolic, each times an exponential decay factor), and proves that the selected trajectory satisfies the @@ -29,6 +31,8 @@ ParentAPIs: References: - Landau & Lifshitz, Mechanics, page 76, section 25. - Goldstein, Classical Mechanics, Chapter 2. + - Caldirola, Nuovo Cimento 18 (1941) 393. + - Kanai, Progress of Theoretical Physics 3 (1948) 440. Requirements: diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean index b37b320b9..7ec778c9c 100644 --- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean +++ b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean @@ -560,7 +560,7 @@ lagrangian, using that the gradient scales with the constant `exp (γ/m * t)`. -/ -lemma gradient_const_mul {f : EuclideanSpace ℝ (Fin 1) → ℝ} {x : EuclideanSpace ℝ (Fin 1)} +private lemma gradient_const_mul {f : EuclideanSpace ℝ (Fin 1) → ℝ} {x : EuclideanSpace ℝ (Fin 1)} (c : ℝ) (hf : DifferentiableAt ℝ f x) : gradient (fun y => c * f y) x = c • gradient f x := by unfold gradient @@ -595,8 +595,8 @@ lemma gradient_lagrangian_velocity_eq (t : Time) (x v : EuclideanSpace ℝ (Fin We now write down the variational gradient of the action of the damped harmonic oscillator, for a trajectory $x(t)$ this is equal to -$$t\mapsto \left.\frac{\partial L(t, \dot x (t), q)}{\partial q}\right|_{q = x(t)} - - \frac{d}{dt} \left.\frac{\partial L(t, v, x(t))}{\partial v}\right|_{v = \dot x (t)}$$ +$$t\mapsto \left.\frac{\partial L(t, q, \dot x (t))}{\partial q}\right|_{q = x(t)} - + \frac{d}{dt} \left.\frac{\partial L(t, x(t), v)}{\partial v}\right|_{v = \dot x (t)}$$ Setting this equal to zero corresponds to the Euler-Lagrange equations, and thereby the equation of motion. @@ -638,8 +638,7 @@ private lemma deriv_exp_smul (a : ℝ) (y : Time → EuclideanSpace ℝ (Fin 1)) /-- The variational gradient of the Caldirola–Kanai action is the exponential factor times the difference of the force and mass times acceleration appearing in Newton's second law. -/ -lemma gradLagrangian_eq_force (xₜ : Time → EuclideanSpace ℝ (Fin 1)) - (hx : ContDiff ℝ ∞ xₜ) : +lemma gradLagrangian_eq_force (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) : S.gradLagrangian xₜ = fun t : Time => exp (S.γ / S.m * t) • (force S xₜ t - S.m • ∂ₜ (∂ₜ xₜ) t) := by have hdx : Differentiable ℝ (∂ₜ xₜ) := deriv_differentiable_of_contDiff xₜ hx diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 7a489b20f..95e797537 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -30,7 +30,7 @@ In this module we define and prove basic lemmas about derivatives of functions o - A.2. Derivatives of functions into manifolds - B. Linearlity properties of the derivative - C. Derivative of constant functions -- D. Smoothness properties of the derivative +- D. Smoothness properties - E. Derivatives of components ## iv. References @@ -157,7 +157,7 @@ lemma deriv_const [NormedAddCommGroup M] [NormedSpace ℝ M] (m : M) : /-! -## D. Smoothness properties of the derivative +## D. Smoothness properties -/ From 4a5911ebcdfed001830645fcaf4163b819d3910d Mon Sep 17 00:00:00 2001 From: Giuseppe Sorge Date: Thu, 2 Jul 2026 14:02:02 +0200 Subject: [PATCH 3/3] docs(ClassicalMechanics): point inherited energy API-map locations at their defining file Review: keep 'location' machine-parseable as 'file (name)'; the inheritance rationale is already stated in the Overview. Toward #905. Co-Authored-By: Claude Fable 5 --- .../DampedHarmonicOscillator/API-map.yaml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml index 90a63358b..fd8e03750 100644 --- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml +++ b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/API-map.yaml @@ -87,15 +87,11 @@ Requirements: - description: The API shall contain the definition of the kinetic energy. done: true - location: > - Inherited from Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (kineticEnergy), - since DampedHarmonicOscillator extends HarmonicOscillator. + location: Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (kineticEnergy) - description: The API shall contain the definition of the potential energy. done: true - location: > - Inherited from Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (potentialEnergy), - since DampedHarmonicOscillator extends HarmonicOscillator. + location: Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (potentialEnergy) - description: The API shall contain the definition of the Lagrangian. done: true