auto-task(HarmonicOscillator): add API-map.yaml tracking the Harmonic oscillator API

[ShlokVaibhav]

Summary

Adds Physlib/ClassicalMechanics/HarmonicOscillator/API-map.yaml, a new in-repo tracker for the
Harmonic oscillator API (Physlib/ClassicalMechanics/HarmonicOscillator/). The map is
generated from the directory's Lean files (Basic.lean, ConfigurationSpace.lean,
Solution.lean), with GitHub issue
#846 "API: Configuration space of harmonic oscillator"
used only as a reference for the intended scope. No Lean source is touched; lake build stays
green (a YAML-only change).

The directory has no API-map.yaml yet, and no open PR is adding one anywhere in the repository
(gh pr list --state open --limit 1000 filtered on API-map.yaml returns nothing). Two open PRs
touch this API but neither adds a map: #1329 adds a new HarmonicOscillator/Geometric/
subdirectory, and #1004 edits ConfigurationSpace.lean (a diffeomorphism feature).

Links below pin commit 843373266f73adaccb4db401c545fdef9810f78e so line numbers are stable.

A note on the issue vs. the code

Issue #846 is scoped to the configuration space of the oscillator, whereas the directory is the
full harmonic-oscillator API, so the map covers the whole directory and uses #846 as the reference
for the configuration-space portion. Per the task rules, every done flag was decided by reading
the code, not by trusting the issue's checkboxes:

• The issue's "Key data structure" asks for the configuration space as "a structure with a single
  value of type Real". The code defines it with a single value of type EuclideanSpace ℝ (Fin 1)
  (a one-dimensional real coordinate). Marked done: true with the type discrepancy recorded.
• The issue requirement "Trajectories should be defined using the configuration space" is not
  met: trajectories are valued in the coordinate model EuclideanSpace ℝ (Fin 1), not in
  ConfigurationSpace. Marked done: false.
• A well-defined notion of trajectories does exist (in the coordinate model), so that half of the
  issue's last requirement is captured by a separate done: true item; the geometric /
  Space-API-integrated version it hints at is done: false, corroborated by two TODOs.
• The directory provides substantially more than the issue lists (energies, Lagrangian and
  Hamiltonian formulations, the TFAE of equations of motion, uniqueness, alternative
  initial-condition parametrizations, amplitude-phase normal form, periodicity). These are marked
  done: true, each grounded in the module "Key results" docstrings.

---

Field-by-field justification (reviewer tick-box)

Title / Overview

Title: Harmonic oscillator

Overview: |
    The key data structure is `HarmonicOscillator`, the classical mechanical system of a mass
    `m` under a linear restoring force `-k x` (spring constant `k`), with position and velocity
    modelled in `EuclideanSpace ℝ (Fin 1)`. The API develops its energies, Lagrangian and
    Hamiltonian formulations, the equivalence of the resulting equations of motion
    (Euler-Lagrange, Newton's second law, Hamilton's equations and the variational principles),
    the explicit solution trajectories for given initial conditions, and a one-dimensional
    `ConfigurationSpace` manifold with a map to physical `Space 1`.

Grounded in the Basic.lean module docstring
Basic.lean#L17-L24:

The classical harmonic oscillator is a classical mechanical system corresponding to a
mass `m` under a force `- k x` where `k` is the spring constant and `x` is the position.

In this file, a coordinate system is assumed where position and velocity both have type
`EuclideanSpace ℝ (Fin 1)`.

and in the Basic.lean "Key results"
Basic.lean#L30-L44
(input data, equation of motion, energy conservation, TFAE) and Solution.lean "Key results"
Solution.lean#L20-L23
(initial conditions, trajectories). The configuration-space clause is grounded in
ConfigurationSpace.lean#L14-L20.

ParentAPIs

ParentAPIs:
  - Euler-Lagrange equations (Physlib/ClassicalMechanics/EulerLagrange.lean)
  - Hamilton's equations (Physlib/ClassicalMechanics/HamiltonsEquations.lean)
  - Space (Physlib/SpaceAndTime/Space)

Determined from the direct public imports and their usages:

Basic.lean imports both classical-mechanics APIs
(Basic.lean#L8-L9):

public import Physlib.ClassicalMechanics.EulerLagrange
public import Physlib.ClassicalMechanics.HamiltonsEquations

Both are actually used: eulerLagrangeOp
(Basic.lean#L488-L492,
defined at
EulerLagrange.lean#L31)
and hamiltonEqOp
(Basic.lean#L865-L869,
defined at
HamiltonsEquations.lean#L39).

ConfigurationSpace.lean imports the Space API
(ConfigurationSpace.lean#L8)
and uses Space 1 in toSpace
(ConfigurationSpace.lean#L173-L174):

public import Physlib.SpaceAndTime.Space.Basic

This matches issue #846's declared parent APIs #854 ("API: Space"); #863 ("API: Configuration
Space") is not imported as an external API since the configuration space is defined within this
directory.

References

References:
  - Landau & Lifshitz, Mechanics, page 58, section 21.
  - Ivo Terek, Introductory Variational Calculus on Manifolds, Section 1 (Basic definitions
    and examples).

Both are real citations taken from the directory's own docstrings (no reference is invented):

• Basic.lean#L84-L88
  and identically Solution.lean#L64-L67:

  References for the classical harmonic oscillator include:
  - Landau & Lifshitz, Mechanics, page 58, section 21.

• ConfigurationSpace.lean#L42-L44:

  - Ivo Terek, Introductory Variational Calculus on Manifolds, page 1 (Section 1, Basic
    definitions and examples).

---

Requirements

✅ HarmonicOscillator input data is defined

- description: >
    The key input-data structure `HarmonicOscillator`, specifying a positive mass `m` and a
    positive spring constant `k`, is defined.
  done: true
  location: Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean (HarmonicOscillator)

Basic.lean#L114-L122

structure HarmonicOscillator where
  m : ℝ
  k : ℝ
  m_pos : 0 < m
  k_pos : 0 < k

✅ Configuration space is defined (issue #846 "Key data structure")

- description: >
    The configuration space of the oscillator is defined as a structure wrapping a single
    chosen global coordinate ... The issue asks for a single value of type `Real`; the code
    stores it as `EuclideanSpace ℝ (Fin 1)`.
  done: true
  location: >
    Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean (ConfigurationSpace)

ConfigurationSpace.lean#L65-L71

structure ConfigurationSpace where
  /-- The chosen global coordinate of the configuration, valued in
  `EuclideanSpace ℝ (Fin 1)`. -/
  val : EuclideanSpace ℝ (Fin 1)

Issue #846: "The key data structure ... is the configuration space ... should be defined as a
structure with a single value of type Real. - [ ] Is defined". Confirmed present; the reviewer
should note the coordinate is EuclideanSpace ℝ (Fin 1) rather than a bare ℝ.

✅ Smooth-manifold structure on the configuration space (issue #846 requirement)

- description: >
    The configuration space carries the structure of a smooth (analytic) manifold modelled on
    `EuclideanSpace ℝ (Fin 1)` via a single global chart ...
  done: true
  location: >
    Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
    (ChartedSpace, IsManifold instances; valHomeomorphism)

ConfigurationSpace.lean#L144-L163

instance : ChartedSpace (EuclideanSpace ℝ (Fin 1)) ConfigurationSpace where
  atlas := { valHomeomorphism.toOpenPartialHomeomorph }
  ...
instance : IsManifold 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) ω ConfigurationSpace where

Issue #846: "- [ ] the structure of a smooth manifold on the configuration space".

✅ Map from configuration space to physical Space (issue #846 requirement)

- description: >
    A map from the configuration space to the actual position of the particle in physical
    `Space 1` ...
  done: true
  location: >
    Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean
    (ConfigurationSpace.toSpace)

ConfigurationSpace.lean#L173-L174

/-- The position in one-dimensional space associated to the configuration. -/
def toSpace (q : ConfigurationSpace) : Space 1 := ⟨fun i => q.val i⟩

Issue #846: "- [ ] maps from the configuration space to the actual position of the particle in
Space".

✅ Angular frequency, energies and energy conservation

- description: >
    The angular frequency `ω = √(k/m)` and the kinetic, potential and total energies ...,
    together with the conservation of energy along solutions of the equation of motion.
  done: true
  location: >
    Physlib/.../Basic.lean (ω, kineticEnergy, potentialEnergy, energy,
    energy_conservation_of_equationOfMotion, energy_conservation_of_equationOfMotion')

Energies at
Basic.lean#L193-L203;
conservation at
Basic.lean#L633-L641:

lemma energy_conservation_of_equationOfMotion (xₜ : Time → EuclideanSpace ℝ (Fin 1))
    (hx : ContDiff ℝ ∞ xₜ) (h : S.EquationOfMotion xₜ) : ∂ₜ (S.energy xₜ) = 0 := by

Grounded in Basic.lean "Key results"
(Basic.lean#L33-L34).

✅ Lagrangian and equation of motion

- description: >
    The Lagrangian of the oscillator, its variational (Euler-Lagrange) gradient, and the
    equation of motion defined as the vanishing of that gradient.
  done: true
  location: Physlib/.../Basic.lean (lagrangian, gradLagrangian, EquationOfMotion)

lagrangian
Basic.lean#L336-L340,
gradLagrangian
Basic.lean#L475-L478,
EquationOfMotion
Basic.lean#L503-L505:

def EquationOfMotion (xₜ : Time → EuclideanSpace ℝ (Fin 1)) : Prop :=
  S.gradLagrangian xₜ = 0

✅ Hamiltonian formulation

- description: >
    The Hamiltonian formulation: the canonical momentum, the Hamiltonian, and the
    Hamilton-equation operator whose vanishing is equivalent to Hamilton's equations.
  done: true
  location: Physlib/.../Basic.lean (toCanonicalMomentum, hamiltonian, hamiltonEqOp)

toCanonicalMomentum
Basic.lean#L687-L700,
hamiltonian
Basic.lean#L727-L730,
hamiltonEqOp
Basic.lean#L850-L854:

noncomputable def hamiltonian (t : Time) (p : EuclideanSpace ℝ (Fin 1))
    (x : EuclideanSpace ℝ (Fin 1)) : ℝ := ...

✅ Equivalence (TFAE) of the equations of motion

- description: >
    The equation of motion is proved equivalent (TFAE) to Newton's second law, Hamilton's
    equations, the variational principle for the action, and the Hamilton variational principle.
  done: true
  location: Physlib/.../Basic.lean (equationOfMotion_tfae)

Basic.lean#L896-L902

lemma equationOfMotion_tfae (xₜ : Time → EuclideanSpace ℝ (Fin 1)) (hx : ContDiff ℝ ∞ xₜ) :
    List.TFAE [S.EquationOfMotion xₜ,
      (∀ t, S.m • ∂ₜ (∂ₜ xₜ) t = force S (xₜ t)),
      hamiltonEqOp S ... = 0, ...] := by

✅ InitialConditions is defined

- description: The structure `InitialConditions` (initial position `x₀` and initial velocity `v₀`) is defined.
  done: true
  location: Physlib/.../Solution.lean (InitialConditions)

Solution.lean#L112-L116

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

✅ Trajectory defined and satisfies the equation of motion

- description: >
    The trajectory associated with a set of initial conditions is defined and proved to
    satisfy the equation of motion.
  done: true
  location: Physlib/.../Solution.lean (InitialConditions.trajectory, trajectory_equationOfMotion)

trajectory
Solution.lean#L365-L367,
trajectory_equationOfMotion
Solution.lean#L500-L515:

noncomputable def trajectory (IC : InitialConditions) : Time → EuclideanSpace ℝ (Fin 1) := fun t =>
  cos (S.ω * t) • IC.x₀ + (sin (S.ω * t)/S.ω) • IC.v₀
...
lemma trajectory_equationOfMotion (IC : InitialConditions) :
    EquationOfMotion S (IC.trajectory S) := by

(The docstring names these trajectories / trajectories_equationOfMotion; the actual
declarations are InitialConditions.trajectory / trajectory_equationOfMotion.)

✅ Uniqueness of trajectories

- description: >
    Uniqueness of the trajectory: any smooth solution of the equation of motion with the same
    initial position and velocity equals the trajectory.
  done: true
  location: Physlib/.../Solution.lean (trajectories_unique)

Solution.lean#L532-L536

lemma trajectories_unique (IC : InitialConditions) (x : Time → EuclideanSpace ℝ (Fin 1))
    (hx : ContDiff ℝ ∞ x) :
    S.EquationOfMotion x ∧ x 0 = IC.x₀ ∧ ∂ₜ x 0 = IC.v₀ →
    x = IC.trajectory S := by

✅ Alternative initial-condition parametrizations

- description: >
    Alternative parametrizations of the initial conditions - at an arbitrary time, from two
    positions, from two velocities, and in amplitude-phase form - each with correctness proofs ...
  done: true
  location: >
    Physlib/.../Solution.lean (InitialConditionsAtTime, InitialConditionsFromTwoPositions,
    InitialConditionsFromTwoVelocities, AmplitudePhase)

Types at
Solution.lean#L172-L178
(at time),
#L231-L239
(two positions),
#L286-L294
(two velocities),
#L782-L786
(amplitude-phase). Correctness proofs e.g. toInitialConditions_trajectory_at_t₀
(#L617-L629).

✅ Periodicity and recurrence

- description: >
    Periodicity and recurrence: the period `T = 2π/ω`, periodicity of the trajectory, and the
    return time to the initial state for non-trivial initial data.
  done: true
  location: Physlib/.../Solution.lean (period, trajectory_periodic, return_time)

period
Solution.lean#L1153-L1159,
trajectory_periodic
#L1180-L1186,
return_time
#L1202-L1204:

noncomputable def period (S : HarmonicOscillator) : ℝ := 2 * π / S.ω

❌ Trajectories defined using the configuration space (issue checked-scope, not met)

- description: >
    Trajectories should be defined using the configuration space ... Currently trajectories are
    valued in the coordinate model `EuclideanSpace ℝ (Fin 1)`, not in `ConfigurationSpace`.
  done: false
  location: N/A

Issue #846: "- [ ] Trajectories should be defined using the configuration space". The only
trajectory definition is valued in EuclideanSpace ℝ (Fin 1), with no ConfigurationSpace in its
signature
(Solution.lean#L365-L367),
and ConfigurationSpace is never used in Solution.lean (a grep for ConfigurationSpace in that
file returns nothing).

❌ Geometric model / interaction with the Space API (issue + TODOs)

- description: >
    A proper geometric model treating position as the configuration space and velocity as its
    tangent space ... and tying trajectories to the Space API ...
  done: false
  location: N/A

Issue #846: "- [ ] Well defined notion for trajectories, may need interaction with 5e Space
API". Corroborated by two TODOs:
Basic.lean#L98-L102

TODO "Create a new file for the geometric model which properly models the position as a
    configuration space and velocity as its tangent space, then show explicitly how this
    coordinate model is a simplification of the geometric model. ..."

and
ConfigurationSpace.lean#L53-L55

TODO "The API around the configuration space
    should be improved to allow further development of a proper
    geometric model of the Harmonic Oscillator."

❌ Split Solution.lean into smaller modules (TODO)

- description: >
    Split `Solution.lean` into smaller modules (`Solution.Basic`, `Solution.Energy`,
    `Solution.InitialData`, `Solution.AmplitudePhase`, `Solution.SpecialTimes`,
    `Solution.Periodicity`) with `Solution.lean` kept as an umbrella import (TODO).
  done: false
  location: N/A

Solution.lean#L71-L78

TODO "Split this file into smaller modules, keeping `Solution.lean` as an umbrella import. ..."

---

Verification

• ruby -e 'require "yaml"; d=YAML.safe_load(File.read(ARGV[0])); raise "bad keys" unless (%w[version Title Overview ParentAPIs References Requirements]-d.keys).empty?' → passes; the
  top-level keys are exactly version, Title, Overview, ParentAPIs, References, Requirements.
• A follow-up Ruby check confirms 16 requirements (13 done: true, 3 done: false), every
  done: true has a non-N/A location, and every done: false has location: N/A.
• Every done: true declaration was confirmed to exist by reading the source at commit
  843373266f73adaccb4db401c545fdef9810f78e (line numbers above); every done: false item was
  confirmed absent (no ConfigurationSpace usage in Solution.lean; no geometric-model file;
  Solution.lean not yet split), grounded in issue API: Configuration space of harmonic oscillator #846 and the in-file TODOs.
• lake build is expected to stay green: this is a YAML-only addition and cannot affect the Lean
  build graph. No .lean file, other map, docstring, or the GitHub issue was modified.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Closing this one as there has been an update to this directory, so some of the references are wrong.