From 94083ea82d52b392d30707852cc9ef2ae337deff Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Mon, 29 Jun 2026 22:16:32 +0400 Subject: [PATCH 1/2] docs(classical-mechanics): add TODO to split harmonic oscillator solution --- .../HarmonicOscillator/Solution.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index cdb4d754a..5b167a3b8 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -66,8 +66,19 @@ prove that they satisfy the equation of motion, and prove some properties of the References for the classical harmonic oscillator include: - Landau & Lifshitz, Mechanics, page 58, section 21. +## v. TODOs + -/ +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 namespace ClassicalMechanics From b8ddb761e8b354740c73eeb3b9105372b66ec94d Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Tue, 30 Jun 2026 09:16:56 +0400 Subject: [PATCH 2/2] docs(classical-mechanics): remove solution TODO heading --- Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 5b167a3b8..459ab748c 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean @@ -66,8 +66,6 @@ prove that they satisfy the equation of motion, and prove some properties of the References for the classical harmonic oscillator include: - Landau & Lifshitz, Mechanics, page 58, section 21. -## v. TODOs - -/ TODO "Split this file into smaller modules, keeping `Solution.lean` as an umbrella import.