docs(classical-mechanics): add configuration API maps

Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml

@@ -0,0 +1,94 @@
+version: v0.1
+
+Title: Configuration space of the harmonic oscillator
+
+Overview: |
+    The one-dimensional harmonic oscillator is a mass on a spring: a single particle
+    moving on a line under a restoring force proportional to its displacement. Its
+    configuration is one real coordinate, so its configuration space `Q` is a
+    one-dimensional smooth manifold; trajectories are curves from `Time` into `Q`,
+    and the kinetic energy comes from the mass metric, the mass-scaled Euclidean
+    inner product on tangent vectors.
+
+    The API formalises this geometrically. `ConfigurationSpace` wraps a global
+    coordinate valued in `EuclideanSpace ℝ (Fin 1)` and carries the induced
+    topology, a coordinate homeomorphism and analytic diffeomorphism, charted-space
+    and manifold instances, tangent-coordinate infrastructure, and a map to physical
+    `Space 1`. Smoothness of a trajectory reduces to smoothness of its coordinate
+    curve, the velocity is a tangent vector recovered as the coordinate derivative,
+    and the geometric kinetic energy recovers the standard mass-scaled expression.
+
+ParentAPIs:
+  - Harmonic oscillator (Physlib/ClassicalMechanics/HarmonicOscillator)
+  - Space (Physlib/SpaceAndTime/Space)
+  - Time (Physlib/SpaceAndTime/Time)
+
+References:
+  - Ivo Terek, Introductory Variational Calculus on Manifolds, Section 1 (pages 1-2), Basic definitions and examples.
+
+Requirements:
+
+  - description: >
+      The key data structure of the API, the configuration space of the classical
+      harmonic oscillator, is defined as a structure carrying a single global
+      coordinate (a one-dimensional Euclidean value), with extensionality in that
+      coordinate and function-like coordinate access.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (ConfigurationSpace, val, ext, coe_apply)
+
+  - description: >
+      The API equips the configuration space with the topology induced by its global
+      coordinate and the coordinate equivalence and homeomorphism to the Euclidean
+      model, transporting Hausdorffness and second countability across it.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (valEquiv, valHomeomorphism)
+
+  - description: >
+      The API provides the smooth-manifold structure on the configuration space: the
+      charted-space and analytic manifold instances via a single global chart, together
+      with the global coordinate chart as an analytic diffeomorphism to the Euclidean
+      model.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (valDiffeomorph, ChartedSpace instance, IsManifold instance)
+
+  - description: >
+      The API provides the tangent-coordinate infrastructure: the normed real
+      vector-space and finite-dimensionality structures on each tangent space and the
+      chart-induced continuous linear equivalence from the tangent space to the
+      Euclidean coordinate model.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (tangentCoord, instNormedAddCommGroupTangent, instNormedSpaceTangent, instFiniteDimensionalTangent)
+
+  - description: >
+      The API provides a map from the configuration space to the actual position of the
+      particle in physical `Space 1`, obtained by reading off the underlying coordinate.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (toSpace, toSpace_apply)
+
+  - description: >
+      Trajectories of the oscillator are defined using the configuration space, as
+      time-parametrised curves into `Q`, with a global-coordinate projection curve and a
+      physical-space position curve.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean (Trajectory, coord, toSpace, coord_apply)
+
+  - description: >
+      The API gives a well-defined notion of smooth trajectory, characterising manifold
+      smoothness and differentiability of a trajectory in terms of ordinary smoothness
+      and differentiability of its coordinate curve, and defines the geometric velocity
+      as a tangent vector, shown to be the time derivative of the coordinate curve.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean (contMDiff_iff_contDiff_coord, mdifferentiableAt_iff_differentiableAt_coord, velocity, velocity_eq_deriv_coord)
+
+  - description: >
+      The API defines the oscillator mass Riemannian metric on the configuration space
+      as the mass-scaled Euclidean inner product in global tangent coordinates, with its
+      positive-definiteness and coordinate evaluation.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean (massMetricVal, massMetricVal_apply, massMetricVal_pos, massRiemannianMetric, massRiemannianMetric_pos, massRiemannianMetric_inner_apply)
+
+  - description: >
+      The API defines the geometric kinetic energy from the mass Riemannian metric and
+      proves it recovers the standard mass-scaled coordinate expression.
+    done: true
+    location: Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean (geometricKineticEnergy, geometricKineticEnergy_eq, geometricKineticEnergy_massMetric_eq)

Physlib/ClassicalMechanics/Lagrangian/API-map.yaml

@@ -0,0 +1,37 @@
+version: v0.1
+
+Title: Configuration Space
+
+Overview: |
+    The configuration space `Q` of a mechanical system is the manifold of its
+    possible instantaneous configurations, coordinatised by generalized coordinates.
+    It is the base space of the Lagrangian formulation of mechanics: a Lagrangian is
+    a function on the tangent bundle `TQ` of positions and velocities, and the
+    Euler-Lagrange equations describe physical motions as curves in `Q`.
+
+    The library does not yet have a general, system-agnostic configuration-space
+    abstraction, nor a Lagrangian built over one; those are the requirements below.
+    Concrete per-system configuration spaces exist and are tracked in their own API
+    maps (the geometric harmonic oscillator and the pendulum).
+
+ParentAPIs:
+  - Space (Physlib/SpaceAndTime/Space)
+
+References:
+  - Ivo Terek, Introductory Variational Calculus on Manifolds, Section 1
+  - Landau and Lifshitz, Mechanics, 3rd ed., Chapter 1 (generalised coordinates, the principle of least action, the Lagrangian)
+
+Requirements:
+
+  - description: >
+      A general, system-agnostic `ConfigurationSpace` construction (a configuration manifold
+      abstracting over the choice of mechanical system) usable across the Lagrangian API.
+    done: false
+    location: N/A
+
+  - description: >
+      A general treatment of generalized coordinates and the velocity phase space (tangent
+      bundle `TQ`) built over a shared configuration-space abstraction, on which a Lagrangian
+      is defined for the Euler-Lagrange API.
+    done: false
+    location: N/A

Physlib/ClassicalMechanics/Pendulum/API-map.yaml

@@ -0,0 +1,52 @@
+version: v0.1
+
+Title: Configuration space for pendulum
+
+Overview: |
+    A pendulum is a mass swinging under gravity on a string or rod; its
+    configuration is set by angles and, for a moving support, the support position,
+    so its configuration space is naturally a product of circles and lines. This API
+    covers the pendulum problems of Landau and Lifshitz, Mechanics, 3rd ed.,
+    Chapter 1, Section 5.
+
+    At present only the sliding pendulum has a defined configuration space, with
+    the horizontal support position and the string angle as its generalized
+    coordinates. The coplanar double pendulum's configuration space is declared but
+    not yet defined, and the miscellaneous pivot-motion problems have documentation
+    only. The remaining requirements, a manifold structure on the configuration
+    space, a map into real space, trajectories, and the lagrangian, are open and
+    recorded below with location N/A.
+
+ParentAPIs:
+  - Classical mechanics Lagrangian (Physlib/ClassicalMechanics/Lagrangian)
+  - Space (Physlib/SpaceAndTime/Space)
+
+References:
+  - Landau & Lifshitz, Mechanics, 3rd Edition, Chapter 1 (The Equations of motion), Section 5 (The Lagrangian for a system of particles).
+
+Requirements:
+
+  - description: >
+      The key data structure, the configuration space of the pendulum, is defined
+      (chosen here as generalized coordinates, the support position and the string
+      angle for the sliding pendulum).
+    done: true
+    location: Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean (ConfigurationSpace)
+
+  - description: The API shall contain the structure of a manifold on the configuration space.
+    done: false
+    location: "N/A"
+
+  - description: >
+      The API shall contain a map from the configuration space to `Space`, giving the
+      position of the pendulum in real space.
+    done: false
+    location: "N/A"
+
+  - description: The API shall contain the definition of a trajectory based on the configuration space.
+    done: false
+    location: "N/A"
+
+  - description: The API shall subsequently contain the definition of the lagrangian.
+    done: false
+    location: "N/A"