1. Physlib
  2. ClassicalMechanics
  3. HarmonicOscillator
  4. Solving the classical harmonic oscillator
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Nathaneal Sajan, Joseph Tooby-Smith, Lode Vermeulen -/ module public import Physlib.ClassicalMechanics.HarmonicOscillator.Basic public import Mathlib.Analysis.SpecialFunctions.Complex.Arg

Solutions to the classical harmonic oscillator

i. Overview

In this module we define the solutions to the classical harmonic oscillator, prove that they satisfy the equation of motion, and prove some properties of the solutions.

ii. Key results

    InitialConditions is a structure for the initial conditions for the harmonic oscillator.

    trajectories is the trajectories to the harmonic oscillator for given initial conditions.

    trajectories_equationOfMotion proves that the solution satisfies the equation of motion.

iii. Table of contents

    A. The initial conditions

      A.1. Definition of the initial conditions

      A.2. Relation to other types of initial conditions

        A.2.1. Initial conditions at arbitrary time

        A.2.2. Initial conditions from two positions at different times

        A.2.3. Initial conditions from two velocities at different times

      A.3. The zero initial conditions

        A.3.1. Simple results for the zero initial conditions

    B. Trajectories associated with the initial conditions

      B.1. The trajectory associated with the initial conditions

        B.1.1. Definitional equality for the trajectory

      B.2. The trajectory for zero initial conditions

      B.3. Smoothness of the trajectories

      B.4. Velocity of the trajectories

      B.5. Acceleration of the trajectories

      B.6. The initial conditions of the trajectories

    C. Trajectories and Equation of motion

      C.1. Uniqueness of the solutions

    D. The energy of the trajectories

      D.1. Correctness of InitialConditionsAtTime conversion

      D.2. Correctness of InitialConditionsFromTwoPositions conversion

      D.3. Correctness of InitialConditionsFromTwoVelocities conversion

    E. Amplitude–phase parametrization

      E.1. The amplitude–phase initial conditions

      E.2. Conversion to standard initial conditions

      E.3. The trajectory in normal form

      E.4. Recovering the amplitude and phase

    F. Special conditions of the trajectory

      F.1. Normal form for standard initial conditions

      F.2. Times at which the velocity is zero

      F.3. The position when the velocity is zero

      F.4. Times at which the trajectory passes through zero

    G. Periodicity and recurrence

      G.1. The period

      G.2. Periodicity of the trajectory

      G.3. Return to the initial state

iv. References

References for the classical harmonic oscillator include:

    Landau & Lifshitz, Mechanics, page 58, section 21.

TODO "Split this file into smaller modules, keeping `Solution.lean` as an umbrella import. The intended organization is: - `Solution.Basic` for trajectory construction and equation-of-motion facts; - `Solution.Energy` for energy-related lemmas; - `Solution.InitialData` for alternative initial-condition parametrizations; - `Solution.AmplitudePhase` for the amplitude-phase normal form; - `Solution.SpecialTimes` for velocity-zero times, turning points, and zero crossings; - `Solution.Periodicity` for period and recurrence facts."@[expose] public section

A. The initial conditions

We define the type of initial conditions for the harmonic oscillator. The initial conditions are currently defined as an initial position and an initial velocity, that is the values of the solution and its time derivative at time 0.

A.1. Definition of the initial conditions

We start by defining the type of initial conditions for the harmonic oscillator.

The initial conditions for the harmonic oscillator specified by an initial position, and an initial velocity.

The @[ext] attribute provides an extensionality lemma for InitialConditions. That is, a lemma which states that two initial conditions are equal if their initial positions and initial velocities are equal.

The initial position of the harmonic oscillator.

The initial velocity of the harmonic oscillator.

@[ext] structure InitialConditions where x₀ : EuclideanSpace ℝ (Fin 1) v₀ : EuclideanSpace ℝ (Fin 1)

A.2. Relation to other types of initial conditions

We relate the initial condition given by an initial position and an initial velocity to other specifications of initial conditions.

In this section, we implement alternative ways to specify initial conditions for the harmonic oscillator. The standard InitialConditions type specifies position and velocity at time t=0, but in practice it is often useful to specify initial conditions at other times or in other forms.

Currently implemented:

    Initial conditions at arbitrary time: Specify position and velocity at any time t₀, not necessarily at t=0. This is useful for problems where the natural reference time is not zero.

    Initial conditions from two positions at different times: Specify the position at two distinct times t₁ and t₂ that satisfy the non-degeneracy condition.

    Initial conditions from two velocities at different times: Specify the velocity at two distinct times t₁ and t₂ that satisfy the non-degeneracy condition.

    Amplitude–phase parametrization: Specify the solution as a single shifted cosine x(t) = A cos (ω t - φ) with amplitude A and phase φ.

All alternative forms can be converted to the standard InitialConditions type via conversion functions, and we prove that the converted initial conditions produce trajectories that satisfy the original specifications.

A.2.1. Initial conditions at arbitrary time

We define a type for initial conditions specified at an arbitrary time t₀, rather than at t=0. This is useful when the natural reference point for a problem is not at time zero.

The conversion to the standard InitialConditions works by "running the trajectory backward in time" from t₀ to 0. Given that we know x(t₀) and v(t₀), we use the harmonic oscillator solution formula with time-reversal to determine what x(0) and v(0) must have been.

Mathematically, if x(t) = cos(ωt)·x₀ + (sin(ωt)/ω)·v₀, then setting t = t₀: x(t₀) = cos(ωt₀)·x₀ + (sin(ωt₀)/ω)·v₀ v(t₀) = -ω·sin(ωt₀)·x₀ + cos(ωt₀)·v₀

Solving this linear system for x₀ and v₀ gives the formulas in toInitialConditions below.

Initial conditions for the harmonic oscillator specified at an arbitrary time t₀.

This structure allows specifying the position and velocity at any time t₀, not necessarily at t=0. This is useful for problems where the natural reference time is not zero.

The conditions can be converted to the standard InitialConditions format (at t=0) using the toInitialConditions function.

The time at which the initial conditions are specified.

The position at time t₀.

The velocity at time t₀.

@[ext] structure InitialConditionsAtTime where t₀ : Time x_t₀ : EuclideanSpace ℝ (Fin 1) v_t₀ : EuclideanSpace ℝ (Fin 1)

The correctness proofs showing that the conversion produces the expected trajectory are given later in section D.1, after the trajectory machinery has been defined.

A.2.2. Initial conditions from two positions at different times

We define a type for initial conditions specified by two measured positions x_t₁ and x_t₂ at two distinct times t₁ and t₂.

The conversion to the standard InitialConditions is obtained by solving for x₀ and v₀ the two equations given by evaluating the trajectory at t₁ and t₂: x_t₁ = cos(ωt₁)·x₀ + (sin(ωt₁)/ω)·v₀ x_t₂ = cos(ωt₂)·x₀ + (sin(ωt₂)/ω)·v₀

This linear system has determinant (cos(ωt₁)·sin(ωt₂) - cos(ωt₂)·sin(ωt₁))/ω = sin(ω(t₂-t₁))/ω. Writing Δ = sin(ω(t₂-t₁)), solving the system gives the formulas used below: x₀ = (sin(ωt₂)·x_t₁ - sin(ωt₁)·x_t₂)/Δ v₀ = ω·(cos(ωt₁)·x_t₂ - cos(ωt₂)·x_t₁)/Δ

The conversion is defined as a total function, but it recovers the initial conditions only when Δ = sin(ω(t₂-t₁)) ≠ 0, i.e. when t₂ - t₁ is not an integer multiple of half a period. The correctness proofs, under this nondegeneracy condition, are given later in section D.2.

Initial conditions for the harmonic oscillator specified by two positions x_t₁ and x_t₂ measured at two times t₁ and t₂ respectively.

The conditions can be converted to the standard InitialConditions format using the toInitialConditions function.

The first measurement time.

The position at time t₁.

The second measurement time.

The position at time t₂.

@[ext] structure InitialConditionsFromTwoPositions where t₁ : Time x_t₁ : EuclideanSpace ℝ (Fin 1) t₂ : Time x_t₂ : EuclideanSpace ℝ (Fin 1)
A.2.3. Initial conditions from two velocities at different times

We define a type for initial conditions specified by two measured velocities v_t₁ and v_t₂ at two distinct times t₁ and t₂.

The conversion to the standard InitialConditions is obtained by solving for x₀ and v₀ the two equations given by evaluating the velocity of the trajectory at t₁ and t₂: v_t₁ = -ω·sin(ωt₁)·x₀ + cos(ωt₁)·v₀ v_t₂ = -ω·sin(ωt₂)·x₀ + cos(ωt₂)·v₀

This linear system has determinant ω·(cos(ωt₁)·sin(ωt₂) - cos(ωt₂)·sin(ωt₁)) = ω·sin(ω(t₂-t₁)). Writing Δ = sin(ω(t₂-t₁)), solving the system gives the formulas used below: x₀ = (cos(ωt₂)·v_t₁ - cos(ωt₁)·v_t₂)/(ω·Δ) v₀ = (sin(ωt₂)·v_t₁ - sin(ωt₁)·v_t₂)/Δ

The conversion is defined as a total function, but it recovers the initial conditions only when Δ = sin(ω(t₂-t₁)) ≠ 0, i.e. when t₂ - t₁ is not an integer multiple of half a period. The correctness proofs, under this nondegeneracy condition, are given later in section D.3.

Initial conditions for the harmonic oscillator specified by two velocities v_t₁ and v_t₂ measured at two times t₁ and t₂ respectively.

The conditions can be converted to the standard InitialConditions format using the toInitialConditions function.

The first measurement time.

The velocity at time t₁.

The second measurement time.

The velocity at time t₂.

@[ext] structure InitialConditionsFromTwoVelocities where t₁ : Time v_t₁ : EuclideanSpace ℝ (Fin 1) t₂ : Time v_t₂ : EuclideanSpace ℝ (Fin 1)

A.3. The zero initial conditions

The zero initial conditions are the initial conditions with zero initial position and zero initial velocity.

In the end, we will see that this corresponds to the solution which is identically zero, i.e. the particle remains at rest at the origin.

The zero initial condition.

instance : Zero InitialConditions := ⟨0, 0⟩
A.3.1. Simple results for the zero initial conditions

Some simple results about the zero initial conditions.

The zero initial condition has zero starting point.

@[simp] lemma x₀_zero : x₀ 0 = 0 := rfl

The zero initial condition has zero starting velocity.

@[simp] lemma v₀_zero : v₀ 0 = 0 := rfl

B. Trajectories associated with the initial conditions

To each initial condition we association a trajectory. We will prove some basic properties of these trajectories.

Eventually we will show that these trajectories satisfy the equation of motion, for now we can think of them as some choice of trajectory associated with the initial conditions.

B.1. The trajectory associated with the initial conditions

B.1.1. Definitional equality for the trajectory

We show a basic definitional equality for the trajectory.

lemma trajectory_eq (IC : InitialConditions) : IC.trajectory S = fun t : Time => cos (S.ω * t) • IC.x₀ + (sin (S.ω * t)/S.ω) • IC.v₀ := rfl

B.2. The trajectory for zero initial conditions

The trajectory for zero initial conditions is the zero function.

For zero initial conditions, the trajectory is zero.

@[simp] lemma trajectory_zero : trajectory S 0 = fun _ => 0 := S:HarmonicOscillator⊢ trajectory S 0 = fun x => 0 All goals completed! 🐙

B.3. Smoothness of the trajectories

The trajectories for any initial conditions are smooth functions of time.

S:HarmonicOscillatorIC:InitialConditionsn:ℕ∞ω⊢ ContDiff ℝ n fun t => Real.cos (S.ω * t.val) • IC.x₀ + (Real.sin (S.ω * t.val) / S.ω) • IC.v₀ S:HarmonicOscillatorIC:InitialConditionsn:ℕ∞ωh:ContDiff ℝ n val⊢ ContDiff ℝ n fun t => Real.cos (S.ω * t.val) • IC.x₀ + (Real.sin (S.ω * t.val) / S.ω) • IC.v₀ All goals completed! 🐙

B.4. Velocity of the trajectories

We give a simplification of the velocity of the trajectory.

S:HarmonicOscillatorIC:InitialConditionst:Timeh1:fderiv ℝ (fun t => Real.sin (S.ω * t.val) / S.ω) t = (1 / S.ω) • fderiv ℝ (fun t => Real.sin (S.ω * t.val)) t⊢ (-Real.sin (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)) 1 • IC.x₀ + (S.ω⁻¹ * (Real.cos (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)) 1) • IC.v₀ = -(S.ω • Real.sin (S.ω * t.val) • IC.x₀) + Real.cos (S.ω * t.val) • IC.v₀ S:HarmonicOscillatorIC:InitialConditionst:Timeh1:fderiv ℝ (fun t => Real.sin (S.ω * t.val) / S.ω) t = (1 / S.ω) • fderiv ℝ (fun t => Real.sin (S.ω * t.val)) t⊢ -((Real.sin (S.ω * t.val) * S.ω) • IC.x₀) + (S.ω⁻¹ * (Real.cos (S.ω * t.val) * S.ω)) • IC.v₀ = -(S.ω • Real.sin (S.ω * t.val) • IC.x₀) + Real.cos (S.ω * t.val) • IC.v₀ S:HarmonicOscillatorIC:InitialConditionst:Timeh1:fderiv ℝ (fun t => Real.sin (S.ω * t.val) / S.ω) t = (1 / S.ω) • fderiv ℝ (fun t => Real.sin (S.ω * t.val)) t⊢ -((S.ω * Real.sin (S.ω * t.val)) • IC.x₀) + Real.cos (S.ω * t.val) • IC.v₀ = -(S.ω • Real.sin (S.ω * t.val) • IC.x₀) + Real.cos (S.ω * t.val) • IC.v₀ All goals completed! 🐙

B.5. Acceleration of the trajectories

We give a simplification of the acceleration of the trajectory.

S:HarmonicOscillatorIC:InitialConditionst:Time⊢ (-(S.ω • (Real.cos (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)).smulRight IC.x₀)) 1 + (-Real.sin (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)) 1 • IC.v₀ = -(S.ω ^ 2 • Real.cos (S.ω * t.val) • IC.x₀) - S.ω • Real.sin (S.ω * t.val) • IC.v₀ S:HarmonicOscillatorIC:InitialConditionst:Time⊢ (-(S.ω • (Real.cos (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)).smulRight IC.x₀)) 1 + (-Real.sin (S.ω * t.val) • (S.ω • fderiv ℝ val t + t.val • fderiv ℝ (fun t => S.ω) t)) 1 • IC.v₀ = -(S.ω ^ 2 • Real.cos (S.ω * t.val) • IC.x₀) - S.ω • Real.sin (S.ω * t.val) • IC.v₀ S:HarmonicOscillatorIC:InitialConditionst:Time⊢ -(S.ω • (Real.cos (S.ω * t.val) * S.ω) • IC.x₀) + -((Real.sin (S.ω * t.val) * S.ω) • IC.v₀) = -(S.ω ^ 2 • Real.cos (S.ω * t.val) • IC.x₀) - S.ω • Real.sin (S.ω * t.val) • IC.v₀ All goals completed! 🐙

B.6. The initial conditions of the trajectories

We show that, unsurprisingly, the trajectories have the initial conditions used to define them.

For a set of initial conditions IC the position of the solution at time 0 is IC.x₀.

@[simp] lemma trajectory_position_at_zero (IC : InitialConditions) : IC.trajectory S 0 = IC.x₀ := S:HarmonicOscillatorIC:InitialConditions⊢ trajectory S IC 0 = IC.x₀ All goals completed! 🐙
@[simp] lemma trajectory_velocity_at_zero (IC : InitialConditions) : ∂ₜ (IC.trajectory S) 0 = IC.v₀ := S:HarmonicOscillatorIC:InitialConditions⊢ ∂ₜ (trajectory S IC) 0 = IC.v₀ All goals completed! 🐙

C. Trajectories and Equation of motion

The trajectories satisfy the equation of motion for the harmonic oscillator.

S:HarmonicOscillatorIC:InitialConditionst:Timei✝:Fin 1hωm:S.ω ^ 2 * S.m = S.k⊢ -(S.ω ^ 2 * S.m * Real.cos (t.val * S.ω) * IC.x₀.ofLp i✝) + -(S.ω ^ 2 * S.m * (Real.sin (t.val * S.ω) / S.ω) * IC.v₀.ofLp i✝) - S.m * (-(S.ω ^ 2 * Real.cos (t.val * S.ω) * IC.x₀.ofLp i✝) - S.ω * Real.sin (t.val * S.ω) * IC.v₀.ofLp i✝) = 0 S:HarmonicOscillatorIC:InitialConditionst:Timei✝:Fin 1hωm:S.ω ^ 2 * S.m = S.k⊢ S.ω * S.m * (-(S.ω * Real.cos (S.ω * t.val) * IC.x₀.ofLp i✝) + -(Real.sin (S.ω * t.val) * IC.v₀.ofLp i✝) - (-(S.ω * Real.cos (S.ω * t.val) * IC.x₀.ofLp i✝) - Real.sin (S.ω * t.val) * IC.v₀.ofLp i✝)) = 0 All goals completed! 🐙

C.1. Uniqueness of the solutions

We show that the trajectories are the unique solutions to the equation of motion for the given initial conditions.

The trajectories to the equation of motion for a given set of initial conditions are unique.

Given any smooth x satisfying the equation of motion with the same initial position and velocity, the difference y = x - IC.trajectory S also solves the equation of motion with zero initial conditions; energy conservation then forces its energy, and hence y, to vanish identically, so x = IC.trajectory S.

S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)⊢ x t = trajectory S IC t S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:S.potentialEnergy (y t) = 0⊢ x t = trajectory S IC t S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0⊢ x t = trajectory S IC t S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0h:1 / 2 = 0⊢ x t = trajectory S IC tS:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0h:S.k * Inner.inner ℝ (y t) (y t) = 0⊢ x t = trajectory S IC t S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0h:1 / 2 = 0⊢ x t = trajectory S IC t All goals completed! 🐙 S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0h:S.k * Inner.inner ℝ (y t) (y t) = 0⊢ x t = trajectory S IC t S:HarmonicOscillatorIC:InitialConditionsx:Time → EuclideanSpace ℝ (Fin 1)hx:ContDiff ℝ ∞ xhEOM:S.EquationOfMotion xhx0:x 0 = IC.x₀hv0:∂ₜ x 0 = IC.v₀hTraj:ContDiff ℝ ∞ (trajectory S IC)dsub:∀ (f g : Time → EuclideanSpace ℝ (Fin 1)), Differentiable ℝ f → Differentiable ℝ g → (∂ₜ fun t => f t - g t) = fun t => ∂ₜ f t - ∂ₜ g ty:Time → EuclideanSpace ℝ (Fin 1) := fun t => x t - trajectory S IC thydef:y = fun t => x t - trajectory S IC thyContDiff:ContDiff ℝ ∞ yhy_deriv:∂ₜ y = fun t => ∂ₜ x t - ∂ₜ (trajectory S IC) thy_deriv2:∂ₜ (∂ₜ y) = fun t => ∂ₜ (∂ₜ x) t - ∂ₜ (∂ₜ (trajectory S IC)) thNewt_x:∀ (t : Time), S.m • ∂ₜ (∂ₜ x) t = S.force (x t)hNewt_traj:∀ (t : Time), S.m • ∂ₜ (∂ₜ (trajectory S IC)) t = S.force (trajectory S IC t)hEOM_y:S.EquationOfMotion yhE:∀ (t : Time), S.energy y t = 0t:Timehk:0 ≤ S.kineticEnergy y thp:0 ≤ S.potentialEnergy (y t)hpe:1 / 2 * (S.k * Inner.inner ℝ (y t) (y t)) = 0h:S.k * Inner.inner ℝ (y t) (y t) = 0hyt:x t - trajectory S IC t = 0⊢ x t = trajectory S IC t All goals completed! 🐙

D. The energy of the trajectories

For a given set of initial conditions, the energy of the trajectory is constant, due to the conservation of energy. Here we show it's value.

S:HarmonicOscillatorIC:InitialConditionst:Time⊢ S.energy (trajectory S IC) 0 = 1 / 2 * (S.m * ‖IC.v₀‖ ^ 2 + S.k * ‖IC.x₀‖ ^ 2) S:HarmonicOscillatorIC:InitialConditionst:Time⊢ 2⁻¹ * S.m * ‖IC.v₀‖ ^ 2 + 2⁻¹ * (S.k * ‖IC.x₀‖ ^ 2) = 2⁻¹ * (S.m * ‖IC.v₀‖ ^ 2 + S.k * ‖IC.x₀‖ ^ 2) All goals completed! 🐙

D.1. Correctness of InitialConditionsAtTime conversion

We now prove the correctness lemmas for the InitialConditionsAtTime.toInitialConditions conversion function. These show that the conversion produces a trajectory that passes through the specified position and velocity at the specified time.

The trajectory resulting from toInitialConditions passes through the specified position x_t₀ at time t₀.

S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ (fun t => Real.cos (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.v₀) IC.t₀ = IC.x_t₀ S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ ((fun t => Real.cos (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.v₀) IC.t₀).ofLp i = IC.x_t₀.ofLp i S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ Real.cos (S.ω * IC.t₀.val) * (Real.cos (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i - Real.sin (S.ω * IC.t₀.val) / S.ω * IC.v_t₀.ofLp i) + (Real.sin (S.ω * IC.t₀.val) / S.ω * (S.ω * (Real.sin (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i)) + Real.sin (S.ω * IC.t₀.val) / S.ω * (Real.cos (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i)) = IC.x_t₀.ofLp i S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ Real.cos (S.ω * IC.t₀.val) * (S.ω * Real.cos (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i - Real.sin (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i) + Real.sin (S.ω * IC.t₀.val) * (S.ω * IC.x_t₀.ofLp i * Real.sin (S.ω * IC.t₀.val) + Real.cos (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i) = S.ω * IC.x_t₀.ofLp i All goals completed! 🐙

The trajectory resulting from toInitialConditions has the specified velocity v_t₀ at time t₀.

S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ (fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.v₀) IC.t₀ = IC.v_t₀ S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ ((fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := Real.cos (S.ω * IC.t₀.val) • IC.x_t₀ - (Real.sin (S.ω * IC.t₀.val) / S.ω) • IC.v_t₀, v₀ := S.ω • Real.sin (S.ω * IC.t₀.val) • IC.x_t₀ + Real.cos (S.ω * IC.t₀.val) • IC.v_t₀ }.v₀) IC.t₀).ofLp i = IC.v_t₀.ofLp i S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ -(S.ω * (Real.sin (S.ω * IC.t₀.val) * (Real.cos (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i - Real.sin (S.ω * IC.t₀.val) / S.ω * IC.v_t₀.ofLp i))) + (Real.cos (S.ω * IC.t₀.val) * (S.ω * (Real.sin (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i)) + Real.cos (S.ω * IC.t₀.val) * (Real.cos (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i)) = IC.v_t₀.ofLp i S:HarmonicOscillatorIC:InitialConditionsAtTimei:Fin 1⊢ -(Real.sin (S.ω * IC.t₀.val) * (S.ω * Real.cos (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i - Real.sin (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i)) + Real.cos (S.ω * IC.t₀.val) * (S.ω * Real.sin (S.ω * IC.t₀.val) * IC.x_t₀.ofLp i + Real.cos (S.ω * IC.t₀.val) * IC.v_t₀.ofLp i) = IC.v_t₀.ofLp i All goals completed! 🐙

The energy of the trajectory at time t₀ equals the energy computed from the initial conditions at t₀.

lemma toInitialConditions_energy_at_t₀ (S : HarmonicOscillator) (IC : InitialConditionsAtTime) : S.energy ((IC.toInitialConditions S).trajectory S) IC.t₀ = 1/2 * (S.m * ‖IC.v_t₀‖^2 + S.k * ‖IC.x_t₀‖^2) := S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ S.energy (InitialConditions.trajectory S (toInitialConditions S IC)) IC.t₀ = 1 / 2 * (S.m * ‖IC.v_t₀‖ ^ 2 + S.k * ‖IC.x_t₀‖ ^ 2) S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ 1 / 2 * S.m * Inner.inner ℝ (∂ₜ (InitialConditions.trajectory S (toInitialConditions S IC)) IC.t₀) (∂ₜ (InitialConditions.trajectory S (toInitialConditions S IC)) IC.t₀) + (1 / 2) • S.k • Inner.inner ℝ (InitialConditions.trajectory S (toInitialConditions S IC) IC.t₀) (InitialConditions.trajectory S (toInitialConditions S IC) IC.t₀) = 1 / 2 * (S.m * ‖IC.v_t₀‖ ^ 2 + S.k * ‖IC.x_t₀‖ ^ 2) S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ 1 / 2 * S.m * Inner.inner ℝ IC.v_t₀ IC.v_t₀ + (1 / 2) • S.k • Inner.inner ℝ IC.x_t₀ IC.x_t₀ = 1 / 2 * (S.m * ‖IC.v_t₀‖ ^ 2 + S.k * ‖IC.x_t₀‖ ^ 2) S:HarmonicOscillatorIC:InitialConditionsAtTime⊢ 1 / 2 * S.m * ‖IC.v_t₀‖ ^ 2 + 1 / 2 * (S.k * ‖IC.x_t₀‖ ^ 2) = 1 / 2 * (S.m * ‖IC.v_t₀‖ ^ 2 + S.k * ‖IC.x_t₀‖ ^ 2) All goals completed! 🐙

D.2. Correctness of InitialConditionsFromTwoPositions conversion

The conversion recovers the initial conditions only when sin (S.ω * (t₂ - t₁)) ≠ 0. This condition fails exactly when ω·(t₂ - t₁) = n·π for some integer n, i.e. when t₂ - t₁ is an integer multiple of half a period; in that case x(t₂) = (-1)^n · x(t₁) for every trajectory, independent of v₀, so the two positions do not determine the initial conditions.

Under this nondegeneracy condition, we prove that the resulting trajectory passes through x_t₁ at t₁ and x_t₂ at t₂.

The trajectory from toInitialConditions passes through x_t₁ at time t₁, provided sin (S.ω * (t₂ - t₁)) ≠ 0.

S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0⊢ (fun t => Real.cos (S.ω * t.val) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.v₀) IC.t₁ = IC.x_t₁ S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ ((fun t => Real.cos (S.ω * t.val) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.v₀) IC.t₁).ofLp i = IC.x_t₁.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ Real.cos (S.ω * IC.t₁.val) * (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₂.ofLp i) + Real.sin (S.ω * IC.t₁.val) / S.ω * (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₂.ofLp i - S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₁.ofLp i) = IC.x_t₁.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ Real.cos (S.ω * IC.t₁.val) * (Real.sin (S.ω * IC.t₂.val) * IC.x_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) * IC.x_t₂.ofLp i) + Real.sin (S.ω * IC.t₁.val) * (Real.cos (S.ω * IC.t₁.val) * IC.x_t₂.ofLp i - IC.x_t₁.ofLp i * Real.cos (S.ω * IC.t₂.val)) = Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₁.ofLp i All goals completed! 🐙

The trajectory from toInitialConditions passes through x_t₂ at time t₂, provided sin (S.ω * (t₂ - t₁)) ≠ 0.

S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0⊢ (fun t => Real.cos (S.ω * t.val) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.v₀) IC.t₂ = IC.x_t₂ S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ ((fun t => Real.cos (S.ω * t.val) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂, v₀ := (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₂ - (S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.x_t₁ }.v₀) IC.t₂).ofLp i = IC.x_t₂.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ Real.cos (S.ω * IC.t₂.val) * (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₂.ofLp i) + Real.sin (S.ω * IC.t₂.val) / S.ω * (S.ω * Real.cos (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₂.ofLp i - S.ω * Real.cos (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₁.ofLp i) = IC.x_t₂.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoPositionshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ Real.cos (S.ω * IC.t₂.val) * (Real.sin (S.ω * IC.t₂.val) * IC.x_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) * IC.x_t₂.ofLp i) + Real.sin (S.ω * IC.t₂.val) * (IC.x_t₂.ofLp i * Real.cos (S.ω * IC.t₁.val) - Real.cos (S.ω * IC.t₂.val) * IC.x_t₁.ofLp i) = Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.x_t₂.ofLp i All goals completed! 🐙

D.3. Correctness of InitialConditionsFromTwoVelocities conversion

The conversion recovers the initial conditions only when sin (S.ω * (t₂ - t₁)) ≠ 0. Under this nondegeneracy condition, we prove that the resulting trajectory has velocity v_t₁ at t₁ and v_t₂ at t₂.

The trajectory from toInitialConditions has velocity v_t₁ at time t₁, provided sin (S.ω * (t₂ - t₁)) ≠ 0.

S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0⊢ (fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.v₀) IC.t₁ = IC.v_t₁ S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ ((fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.v₀) IC.t₁).ofLp i = IC.v_t₁.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ -(S.ω * (Real.sin (S.ω * IC.t₁.val) * (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) * IC.v_t₁.ofLp i - Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) * IC.v_t₂.ofLp i))) + Real.cos (S.ω * IC.t₁.val) * (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₂.ofLp i) = IC.v_t₁.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ -(Real.sin (S.ω * IC.t₁.val) * (Real.cos (S.ω * IC.t₂.val) * IC.v_t₁.ofLp i - Real.cos (S.ω * IC.t₁.val) * IC.v_t₂.ofLp i)) + Real.cos (S.ω * IC.t₁.val) * (IC.v_t₁.ofLp i * Real.sin (S.ω * IC.t₂.val) - Real.sin (S.ω * IC.t₁.val) * IC.v_t₂.ofLp i) = Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₁.ofLp i All goals completed! 🐙

The trajectory from toInitialConditions has velocity v_t₂ at time t₂, provided sin (S.ω * (t₂ - t₁)) ≠ 0.

S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0⊢ (fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.v₀) IC.t₂ = IC.v_t₂ S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ ((fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.x₀ + Real.cos (S.ω * t.val) • { x₀ := (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₁ - (Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)))) • IC.v_t₂, v₀ := (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₁ - (Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) • IC.v_t₂ }.v₀) IC.t₂).ofLp i = IC.v_t₂.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ -(S.ω * (Real.sin (S.ω * IC.t₂.val) * (Real.cos (S.ω * IC.t₂.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) * IC.v_t₁.ofLp i - Real.cos (S.ω * IC.t₁.val) / (S.ω * Real.sin (S.ω * (IC.t₂.val - IC.t₁.val))) * IC.v_t₂.ofLp i))) + Real.cos (S.ω * IC.t₂.val) * (Real.sin (S.ω * IC.t₂.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₁.ofLp i - Real.sin (S.ω * IC.t₁.val) / Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₂.ofLp i) = IC.v_t₂.ofLp i S:HarmonicOscillatorIC:InitialConditionsFromTwoVelocitieshΔ:Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) ≠ 0i:Fin 1⊢ -(Real.sin (S.ω * IC.t₂.val) * (Real.cos (S.ω * IC.t₂.val) * IC.v_t₁.ofLp i - Real.cos (S.ω * IC.t₁.val) * IC.v_t₂.ofLp i)) + Real.cos (S.ω * IC.t₂.val) * (Real.sin (S.ω * IC.t₂.val) * IC.v_t₁.ofLp i - IC.v_t₂.ofLp i * Real.sin (S.ω * IC.t₁.val)) = Real.sin (S.ω * (IC.t₂.val - IC.t₁.val)) * IC.v_t₂.ofLp i All goals completed! 🐙

E. Amplitude–phase parametrization

The state of the harmonic oscillator at t = 0 is captured by InitialConditions as a position x₀ and a velocity v₀. An equivalent and often more physical description writes the solution as a single shifted cosine of amplitude A and phase φ: x(t) = A cos (ω t - φ).

Expanding with the angle-subtraction identity, A cos (ω t - φ) = (A cos φ) cos (ω t) + (A sin φ) sin (ω t), and matching coefficients against the standard solution x(t) = cos (ω t) x₀ + (sin (ω t) / ω) v₀ gives the change of coordinates x₀ = A cos φ, v₀ = A ω sin φ.

We implement the forward map (A, φ) ↦ (x₀, v₀) as toInitialConditions, prove the resulting trajectory is the cosine normal form above (with velocity -A ω sin (ω t - φ)), and implement the inverse map (x₀, v₀) ↦ (A, φ) as fromInitialConditions, recovering A and φ as the polar coordinates of the phase vector (x₀, v₀ / ω).

E.1. The amplitude–phase initial conditions

We define a type for initial conditions specified by an amplitude A and a phase angle φ. Being an amplitude and an angle, these are stored as scalars, rather than as vectors as for the other initial-condition types.

Initial conditions for the harmonic oscillator specified by an amplitude A and a phase offset φ, describing the solution x(t) = A cos (ω t - φ).

The conditions can be converted to the standard InitialConditions format using the toInitialConditions function.

The amplitude of the oscillation.

The phase offset of the oscillation.

@[ext] structure AmplitudePhase where A : ℝ φ : ℝ

E.2. Conversion to standard initial conditions

Using x₀ = A cos φ and v₀ = A ω sin φ, we convert amplitude–phase data to the standard initial position and velocity at t = 0.

E.3. The trajectory in normal form

The trajectory built from amplitude–phase data is exactly the single cosine x(t) = A cos (ω t - φ), with velocity v(t) = -A ω sin (ω t - φ). In the position identity the factor 1 / ω of the standard solution cancels the ω in v₀ = A ω sin φ, which uses ω ≠ 0.

The trajectory of amplitude–phase initial conditions is the cosine normal form x(t) = A cos (ω t - φ).

S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ (fun t => Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t = EuclideanSpace.single 0 (IC.A * Real.cos (S.ω * t.val - IC.φ)) S:HarmonicOscillatorIC:AmplitudePhaset:Timei:Fin 1⊢ ((fun t => Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t).ofLp i = (EuclideanSpace.single 0 (IC.A * Real.cos (S.ω * t.val - IC.φ))).ofLp i S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ ((fun t => Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + (Real.sin (S.ω * t.val) / S.ω) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t).ofLp ((fun i => i) ⟨0, ⋯⟩) = (EuclideanSpace.single 0 (IC.A * Real.cos (S.ω * t.val - IC.φ))).ofLp ((fun i => i) ⟨0, ⋯⟩) S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ Real.cos (S.ω * t.val) * (IC.A * Real.cos IC.φ) + Real.sin (S.ω * t.val) / S.ω * (IC.A * S.ω * Real.sin IC.φ) = IC.A * (Real.cos (S.ω * t.val) * Real.cos IC.φ + Real.sin (S.ω * t.val) * Real.sin IC.φ) All goals completed! 🐙

The velocity of the amplitude–phase trajectory is v(t) = -A ω sin (ω t - φ).

S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ (fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t = EuclideanSpace.single 0 (-(IC.A * S.ω * Real.sin (S.ω * t.val - IC.φ))) S:HarmonicOscillatorIC:AmplitudePhaset:Timei:Fin 1⊢ ((fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t).ofLp i = (EuclideanSpace.single 0 (-(IC.A * S.ω * Real.sin (S.ω * t.val - IC.φ)))).ofLp i S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ ((fun t => -S.ω • Real.sin (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.x₀ + Real.cos (S.ω * t.val) • { x₀ := EuclideanSpace.single 0 (IC.A * Real.cos IC.φ), v₀ := EuclideanSpace.single 0 (IC.A * S.ω * Real.sin IC.φ) }.v₀) t).ofLp ((fun i => i) ⟨0, ⋯⟩) = (EuclideanSpace.single 0 (-(IC.A * S.ω * Real.sin (S.ω * t.val - IC.φ)))).ofLp ((fun i => i) ⟨0, ⋯⟩) S:HarmonicOscillatorIC:AmplitudePhaset:Time⊢ -(S.ω * (Real.sin (S.ω * t.val) * (IC.A * Real.cos IC.φ))) + Real.cos (S.ω * t.val) * (IC.A * S.ω * Real.sin IC.φ) = -(IC.A * S.ω * (Real.sin (S.ω * t.val) * Real.cos IC.φ - Real.cos (S.ω * t.val) * Real.sin IC.φ)) All goals completed! 🐙

E.4. Recovering the amplitude and phase

The inverse map (x₀, v₀) ↦ (A, φ) must solve x₀ = A cos φ and v₀ / ω = A sin φ. Recovering the angle with the real arctan covers only (-π/2, π/2) and forces a case split at x₀ = 0; we instead embed the phase vector as the complex number z = x₀ + (v₀ / ω) i and read off A = ‖z‖ and φ = Complex.arg z, with arg in the canonical range (-π, π]. The degenerate state x₀ = v₀ = 0 is covered by the convention arg 0 = 0, so no case split is needed.

We prove that converting initial conditions to amplitude–phase form and back returns the original initial conditions.

fromInitialConditions is a right inverse of toInitialConditions: converting initial conditions to amplitude–phase form and back recovers them exactly.

S:HarmonicOscillatorIC:InitialConditionshω:S.ω ≠ 0z:ℂ := { re := IC.x₀.ofLp 0, im := IC.v₀.ofLp 0 / S.ω }hcos:‖z‖ * Real.cos z.arg = z.rehsin:‖z‖ * Real.sin z.arg = z.imhre:z.re = IC.x₀.ofLp 0him:z.im = IC.v₀.ofLp 0 / S.ωhv:‖z‖ * S.ω * Real.sin z.arg = IC.v₀.ofLp 0⊢ EuclideanSpace.single 0 (IC.v₀.ofLp 0) = IC.v₀ S:HarmonicOscillatorIC:InitialConditionshω:S.ω ≠ 0z:ℂ := { re := IC.x₀.ofLp 0, im := IC.v₀.ofLp 0 / S.ω }hcos:‖z‖ * Real.cos z.arg = z.rehsin:‖z‖ * Real.sin z.arg = z.imhre:z.re = IC.x₀.ofLp 0him:z.im = IC.v₀.ofLp 0 / S.ωhv:‖z‖ * S.ω * Real.sin z.arg = IC.v₀.ofLp 0i:Fin 1⊢ (EuclideanSpace.single 0 (IC.v₀.ofLp 0)).ofLp i = IC.v₀.ofLp i; S:HarmonicOscillatorIC:InitialConditionshω:S.ω ≠ 0z:ℂ := { re := IC.x₀.ofLp 0, im := IC.v₀.ofLp 0 / S.ω }hcos:‖z‖ * Real.cos z.arg = z.rehsin:‖z‖ * Real.sin z.arg = z.imhre:z.re = IC.x₀.ofLp 0him:z.im = IC.v₀.ofLp 0 / S.ωhv:‖z‖ * S.ω * Real.sin z.arg = IC.v₀.ofLp 0⊢ (EuclideanSpace.single 0 (IC.v₀.ofLp 0)).ofLp ((fun i => i) ⟨0, ⋯⟩) = IC.v₀.ofLp ((fun i => i) ⟨0, ⋯⟩); All goals completed! 🐙

F. Special conditions of the trajectory

We use the amplitude-phase parametrization from section E to describe the special times of a trajectory. After converting arbitrary initial conditions to amplitude and phase, every trajectory has the form x(t) = A cos (ω t - φ) and its velocity has the form v(t) = -Aω sin (ω t - φ).

Thus the turning points of the motion are controlled by the zeros of sin (ω t - φ), while the times at which the trajectory passes through the origin are controlled by the zeros of cos (ω t - φ).

F.1. Normal form for standard initial conditions

The amplitude-phase normal form was first proved for data already expressed as an AmplitudePhase. We now transport those identities back to ordinary InitialConditions using AmplitudePhase.fromInitialConditions.

Every trajectory of the harmonic oscillator is a single shifted cosine after converting its initial conditions to amplitude-phase form.

lemma trajectory_eq_cos (IC : InitialConditions) (t : Time) : IC.trajectory S t = EuclideanSpace.single 0 ((AmplitudePhase.fromInitialConditions S IC).A * cos (S.ω * t - (AmplitudePhase.fromInitialConditions S IC).φ)) := S:HarmonicOscillatorIC:InitialConditionst:Time⊢ trajectory S IC t = EuclideanSpace.single 0 ((AmplitudePhase.fromInitialConditions S IC).A * Real.cos (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ)) conv_lhs => S:HarmonicOscillatorIC:InitialConditionst:Time| trajectory S (AmplitudePhase.toInitialConditions S (AmplitudePhase.fromInitialConditions S IC)) t All goals completed! 🐙

The velocity of every trajectory is the corresponding shifted sine in amplitude-phase form.

lemma trajectory_velocity_eq_sin (IC : InitialConditions) (t : Time) : ∂ₜ (IC.trajectory S) t = EuclideanSpace.single 0 (-((AmplitudePhase.fromInitialConditions S IC).A * S.ω * sin (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ))) := S:HarmonicOscillatorIC:InitialConditionst:Time⊢ ∂ₜ (trajectory S IC) t = EuclideanSpace.single 0 (-((AmplitudePhase.fromInitialConditions S IC).A * S.ω * Real.sin (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ))) conv_lhs => S:HarmonicOscillatorIC:InitialConditionst:Time| ∂ₜ (trajectory S (AmplitudePhase.toInitialConditions S (AmplitudePhase.fromInitialConditions S IC))) t All goals completed! 🐙

F.2. Times at which the velocity is zero

In amplitude-phase form the velocity is v(t) = -Aω sin (ω t - φ). For nonzero amplitude this vanishes exactly when sin (ω t - φ) = 0, equivalently when ω t - φ is an integer multiple of π.

For nonzero amplitude, the velocity vanishes exactly when the sine factor in amplitude-phase form vanishes.

S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Time⊢ EuclideanSpace.single 0 (-((AmplitudePhase.fromInitialConditions S IC).A * S.ω * Real.sin (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ))) = 0 ↔ Real.sin (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ) = 0 All goals completed! 🐙

For nonzero amplitude, the velocity is zero exactly at phase times φ + nπ.

S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π) / S.ω⊢ ∃ n_1, ↑n_1 * π = S.ω * (((AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π) / S.ω) - (AmplitudePhase.fromInitialConditions S IC).φ S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π) / S.ω⊢ ↑n * π = S.ω * (((AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π) / S.ω) - (AmplitudePhase.fromInitialConditions S IC).φ S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π) / S.ω⊢ ↑n * π = (AmplitudePhase.fromInitialConditions S IC).φ + ↑n * π - (AmplitudePhase.fromInitialConditions S IC).φ All goals completed! 🐙

F.3. The position when the velocity is zero

The zeros of the velocity are the turning points of the oscillator. In amplitude-phase form, these are the times when sin (ω t - φ) = 0; equivalently, cos (ω t - φ) is 1 or -1. At exactly those times the trajectory has maximal norm, equal to the amplitude A.

The statement also covers the degenerate case A = 0: then the trajectory and its velocity are identically zero, so both sides of the equivalence hold at every time.

The velocity vanishes exactly when the trajectory has norm equal to the amplitude.

S:HarmonicOscillatorIC:InitialConditionst:TimeA:ℝ := (AmplitudePhase.fromInitialConditions S IC).AhA:¬A = 0θ:ℝ := S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φhA':A ≠ 0hA_nonneg:0 ≤ AhA_pos:0 < Ahnorm:‖EuclideanSpace.single 0 (A * Real.cos θ)‖ = Ahnorm':|A * Real.cos θ| = Ahcos_abs:|Real.cos θ| = 1⊢ Real.sin θ = 0 S:HarmonicOscillatorIC:InitialConditionst:TimeA:ℝ := (AmplitudePhase.fromInitialConditions S IC).AhA:¬A = 0θ:ℝ := S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φhA':A ≠ 0hA_nonneg:0 ≤ AhA_pos:0 < Ahnorm:‖EuclideanSpace.single 0 (A * Real.cos θ)‖ = Ahnorm':|A * Real.cos θ| = Ahcos_abs:|Real.cos θ| = 1n:ℤhn:↑n * π = θ⊢ Real.sin θ = 0 All goals completed! 🐙

F.4. Times at which the trajectory passes through zero

In amplitude-phase form the trajectory is x(t) = A cos (ω t - φ). For nonzero amplitude this vanishes exactly when cos (ω t - φ) = 0, equivalently when the phase is an odd multiple of π / 2.

For nonzero amplitude, the trajectory passes through zero exactly when the cosine factor in amplitude-phase form vanishes.

S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Time⊢ EuclideanSpace.single 0 ((AmplitudePhase.fromInitialConditions S IC).A * Real.cos (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ)) = 0 ↔ Real.cos (S.ω * t.val - (AmplitudePhase.fromInitialConditions S IC).φ) = 0 All goals completed! 🐙

For nonzero amplitude, the trajectory passes through zero exactly at phase times φ + (2n + 1)π / 2.

S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + (2 * ↑n + 1) * π / 2) / S.ω⊢ ∃ k, S.ω * (((AmplitudePhase.fromInitialConditions S IC).φ + (2 * ↑n + 1) * π / 2) / S.ω) - (AmplitudePhase.fromInitialConditions S IC).φ = (2 * ↑k + 1) * π / 2 S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + (2 * ↑n + 1) * π / 2) / S.ω⊢ S.ω * (((AmplitudePhase.fromInitialConditions S IC).φ + (2 * ↑n + 1) * π / 2) / S.ω) - (AmplitudePhase.fromInitialConditions S IC).φ = (2 * ↑n + 1) * π / 2 S:HarmonicOscillatorIC:InitialConditionshA:(AmplitudePhase.fromInitialConditions S IC).A ≠ 0t:Timen:ℤhn:t.val = ((AmplitudePhase.fromInitialConditions S IC).φ + (2 * ↑n + 1) * π / 2) / S.ω⊢ (AmplitudePhase.fromInitialConditions S IC).φ * 2 + (2 * ↑n + 1) * π - (AmplitudePhase.fromInitialConditions S IC).φ * 2 = (2 * ↑n + 1) * π All goals completed! 🐙

G. Periodicity and recurrence

Every trajectory is a shifted cosine of angular frequency ω, so it repeats after a fixed period T = 2π / ω. We record the period, show the trajectory is periodic, and prove that — for non-trivial initial data — the trajectory returns to its initial position and velocity exactly at integer multiples of the period.

G.1. The period

The period T = 2π / ω is the time for one complete oscillation; it is positive since ω > 0.

@[inherit_doc period] scoped notation "T" => HarmonicOscillator.periodlemma period_eq : T S = 2 * π / S.ω := rfllemma period_pos : 0 < T S := div_pos (S:HarmonicOscillator⊢ 0 < 2 * π All goals completed! 🐙) S.ω_pos

G.2. Periodicity of the trajectory

The trajectory satisfies x(t + T) = x(t): advancing time by one period shifts the phase ω t by 2π, leaving cos and sin unchanged.

The trajectory of the harmonic oscillator is periodic with period of 2 * π / ω.

S:HarmonicOscillatorIC:InitialConditionst:Timeh:S.ω * (t.val + 2 * π / S.ω) = S.ω * t.val + 2 * π⊢ Real.cos (S.ω * t.val) • IC.x₀ + (Real.sin (S.ω * t.val) / S.ω) • IC.v₀ = InitialConditions.trajectory S IC t All goals completed! 🐙

G.3. Return to the initial state

For non-trivial initial data, the trajectory returns to its initial position and velocity only at integer multiples of the period.

Assuming that the initial coordinate and velocity are not simultaneously zero, the time stamps when the harmonic oscillator returns to its initial coordinate and velocity is a multiple of its period

S:HarmonicOscillatorIC:InitialConditionsnon_trivial:IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0t:Timeht:InitialConditions.trajectory S IC t = IC.x₀ ∧ ∂ₜ (InitialConditions.trajectory S IC) t = IC.v₀c:ℝ := Real.cos (S.ω * t.val)s:ℝ := Real.sin (S.ω * t.val)htx:c • IC.x₀ + (s / S.ω) • IC.v₀ = IC.x₀htv:-(S.ω • s • IC.x₀) + c • IC.v₀ = IC.v₀xx:ℝ := Inner.inner ℝ IC.x₀ IC.x₀vv:ℝ := Inner.inner ℝ IC.v₀ IC.v₀xv:ℝ := Inner.inner ℝ IC.x₀ IC.v₀det:ℝ := vv + xx * S.ω ^ 2hxx0:0 ≤ xxhvv0:0 ≤ vvhω2:0 < S.ω ^ 2zero_lt_det:0 < detdet_ne_zero:det ≠ 0hxx:c * xx + s / S.ω * xv = xxhvv:-S.ω * s * xv + c * vv = vvhcos:1 = Real.cos (S.ω * t.val)n:ℤhn:↑n * (2 * π) = S.ω * t.val⊢ ↑n * (2 * π / S.ω) = t.val S:HarmonicOscillatorIC:InitialConditionsnon_trivial:IC.x₀ ≠ 0 ∨ IC.v₀ ≠ 0t:Timeht:InitialConditions.trajectory S IC t = IC.x₀ ∧ ∂ₜ (InitialConditions.trajectory S IC) t = IC.v₀c:ℝ := Real.cos (S.ω * t.val)s:ℝ := Real.sin (S.ω * t.val)htx:c • IC.x₀ + (s / S.ω) • IC.v₀ = IC.x₀htv:-(S.ω • s • IC.x₀) + c • IC.v₀ = IC.v₀xx:ℝ := Inner.inner ℝ IC.x₀ IC.x₀vv:ℝ := Inner.inner ℝ IC.v₀ IC.v₀xv:ℝ := Inner.inner ℝ IC.x₀ IC.v₀det:ℝ := vv + xx * S.ω ^ 2hxx0:0 ≤ xxhvv0:0 ≤ vvhω2:0 < S.ω ^ 2zero_lt_det:0 < detdet_ne_zero:det ≠ 0hxx:c * xx + s / S.ω * xv = xxhvv:-S.ω * s * xv + c * vv = vvhcos:1 = Real.cos (S.ω * t.val)n:ℤhn:↑n * (2 * π) = S.ω * t.val⊢ ↑n * 2 * π = S.ω * t.val All goals completed! 🐙