From fa1de6051622739a4578685f18a8073e74867898 Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Thu, 16 Jul 2026 11:24:07 -0500 Subject: [PATCH 1/4] docs(classical-mechanics): add configuration API maps --- .../HarmonicOscillator/Geometric/API-map.yaml | 91 +++++++++++++++++ .../Lagrangian/API-map.yaml | 99 +++++++++++++++++++ .../ClassicalMechanics/Pendulum/API-map.yaml | 57 +++++++++++ 3 files changed, 247 insertions(+) create mode 100644 Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml create mode 100644 Physlib/ClassicalMechanics/Lagrangian/API-map.yaml create mode 100644 Physlib/ClassicalMechanics/Pendulum/API-map.yaml diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml new file mode 100644 index 000000000..e115b5aed --- /dev/null +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml @@ -0,0 +1,91 @@ +version: v0.1 + +Title: Configuration space of the harmonic oscillator + +Overview: | + The geometric API for the one-dimensional harmonic oscillator formalises its + configuration space `Q` as a one-dimensional smooth (analytic) manifold. The key + data structure `ConfigurationSpace` wraps a single chosen global coordinate valued + in `EuclideanSpace ℝ (Fin 1)`; the required structure carrying a single real + value is realised by this one-dimensional Euclidean coordinate. This coordinate + supplies the induced topology, a global coordinate homeomorphism and diffeomorphism, + the charted-space and manifold instances, the tangent-coordinate infrastructure, and + a map to physical `Space 1`. Trajectories are curves from `Time` into `Q`, with a + coordinate projection, a smoothness characterisation reducing manifold smoothness to + ordinary smoothness of the coordinate curve, and a geometric velocity in the tangent + bundle. A companion mass Riemannian metric gives the geometric kinetic energy. + +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) diff --git a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml new file mode 100644 index 000000000..897dd0261 --- /dev/null +++ b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml @@ -0,0 +1,99 @@ +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: a Lagrangian is a function on the tangent bundle + `TQ` (positions and velocities), and the Euler-Lagrange equations describe curves in `Q`. + + There is at present no single general `ConfigurationSpace` construction shared across the + Lagrangian API; the notion exists only as concrete, per-system types. The most developed + instance is the geometric harmonic oscillator, whose `ConfigurationSpace` is built up as a + genuine one-dimensional analytic manifold: a wrapper around a single global coordinate in + `EuclideanSpace ℝ (Fin 1)`, carrying an induced topology, a coordinate homeomorphism and + analytic diffeomorphism, charted-space and manifold instances, tangent-coordinate + infrastructure, and a map to physical `Space 1`. Lighter per-system configuration-space + types exist for the sliding pendulum (support position and string angle) and, as a + `sorry` stub only, for the coplanar double 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 co-ordinates, 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 concrete configuration-space type for the geometric harmonic oscillator is defined, + wrapping a single chosen global coordinate valued in `EuclideanSpace ℝ (Fin 1)`, with + extensionality and a function-like coordinate accessor. + done: true + location: > + Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean + (ConfigurationSpace, ConfigurationSpace.ext, ConfigurationSpace.coe_apply) + + - description: > + The configuration space of the geometric harmonic oscillator carries a topology induced + by its chosen coordinate, and a coordinate equivalence and homeomorphism to its + `EuclideanSpace ℝ (Fin 1)` model. + done: true + location: > + Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean + (ConfigurationSpace.valEquiv, ConfigurationSpace.valHomeomorphism) + + - description: > + The configuration space of the geometric harmonic oscillator is equipped with a + charted-space and analytic-manifold structure, and the global chart is upgraded to an + analytic diffeomorphism onto `EuclideanSpace ℝ (Fin 1)`. + done: true + location: > + Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean + (ConfigurationSpace.valDiffeomorph) + + - description: > + Tangent-coordinate infrastructure on the geometric harmonic oscillator configuration + space: normed-vector-space structure on tangent spaces and the chart-induced continuous + linear equivalence `tangentCoord` from each tangent space to the coordinate model. + done: true + location: > + Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (tangentCoord) + + - description: > + A map from the geometric harmonic oscillator configuration space to physical + one-dimensional space `Space 1`, reading off the underlying coordinate. + done: true + location: > + Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean + (ConfigurationSpace.toSpace, ConfigurationSpace.toSpace_apply) + + - description: > + A configuration-space type for the sliding pendulum, whose generalized coordinates are + the horizontal support position and the angle of the string from the vertical. + done: true + location: > + Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean + (ConfigurationSpace, ConfigurationSpace.supportPosition, ConfigurationSpace.angle) + + - description: > + A configuration-space type for the coplanar double pendulum. Present only as a + `sorry`-backed stub (`def ConfigurationSpace : Type := sorry`), so not counted as + implemented. + 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 diff --git a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml new file mode 100644 index 000000000..8917afd0b --- /dev/null +++ b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml @@ -0,0 +1,57 @@ +version: v0.1 + +Title: Configuration space for pendulum + +Overview: | + The pendulum is a simple example of a classical-mechanical system whose key data + structure is its configuration space. This API covers the pendulum problems from + Landau & Lifshitz, Mechanics, Chapter 1, Section 5. + + Current state (partial): the sliding pendulum (`SlidingPendulum.lean`) has a genuine + configuration space `structure ConfigurationSpace` with generalized coordinates + `supportPosition : ℝ` (the horizontal position of the support mass) and + `angle : Real.Angle` (the angle the string makes with the vertical). The coplanar + double pendulum (`CoplanarDoublePendulum.lean`) declares `ConfigurationSpace` but it + is still `sorry` (`@[sorryful] def ConfigurationSpace : Type := sorry`), so it is not + treated as defined here. The miscellaneous pivot-motion file + (`MiscellaneousPendulumPivotMotions.lean`) contains only documentation and no + declarations. + + The remaining requirements (a manifold structure on the configuration + space, a map to `Space` giving the position in real space, a trajectory based on the + configuration space, and the lagrangian) are not yet implemented in the Pendulum + directory and are marked undone below. + +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" From 0cad8680df27cbd7bb3892b52f544b618334c9d1 Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Sun, 19 Jul 2026 15:17:00 -0500 Subject: [PATCH 2/4] docs: fix spelling in Lagrangian map reference --- Physlib/ClassicalMechanics/Lagrangian/API-map.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml index 897dd0261..892893765 100644 --- a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml +++ b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml @@ -23,7 +23,7 @@ ParentAPIs: References: - Ivo Terek, Introductory Variational Calculus on Manifolds, Section 1 - - Landau and Lifshitz, Mechanics, 3rd ed., Chapter 1 (generalised co-ordinates, the principle of least action, the Lagrangian) + - Landau and Lifshitz, Mechanics, 3rd ed., Chapter 1 (generalised coordinates, the principle of least action, the Lagrangian) Requirements: From 5d794df327c96e76908f46343ab047b86ca2d851 Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Wed, 22 Jul 2026 08:17:28 -0500 Subject: [PATCH 3/4] docs(classical-mechanics): physics-first overviews, focus the configuration-space map --- .../HarmonicOscillator/Geometric/API-map.yaml | 25 +++--- .../Lagrangian/API-map.yaml | 80 +++---------------- .../ClassicalMechanics/Pendulum/API-map.yaml | 35 ++++---- 3 files changed, 41 insertions(+), 99 deletions(-) diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml index e115b5aed..dbc405fea 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml +++ b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml @@ -3,17 +3,20 @@ version: v0.1 Title: Configuration space of the harmonic oscillator Overview: | - The geometric API for the one-dimensional harmonic oscillator formalises its - configuration space `Q` as a one-dimensional smooth (analytic) manifold. The key - data structure `ConfigurationSpace` wraps a single chosen global coordinate valued - in `EuclideanSpace ℝ (Fin 1)`; the required structure carrying a single real - value is realised by this one-dimensional Euclidean coordinate. This coordinate - supplies the induced topology, a global coordinate homeomorphism and diffeomorphism, - the charted-space and manifold instances, the tangent-coordinate infrastructure, and - a map to physical `Space 1`. Trajectories are curves from `Time` into `Q`, with a - coordinate projection, a smoothness characterisation reducing manifold smoothness to - ordinary smoothness of the coordinate curve, and a geometric velocity in the tangent - bundle. A companion mass Riemannian metric gives the geometric kinetic energy. + 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) diff --git a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml index 892893765..3594e3f74 100644 --- a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml +++ b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml @@ -3,20 +3,16 @@ 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: a Lagrangian is a function on the tangent bundle - `TQ` (positions and velocities), and the Euler-Lagrange equations describe curves in `Q`. + 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`. - There is at present no single general `ConfigurationSpace` construction shared across the - Lagrangian API; the notion exists only as concrete, per-system types. The most developed - instance is the geometric harmonic oscillator, whose `ConfigurationSpace` is built up as a - genuine one-dimensional analytic manifold: a wrapper around a single global coordinate in - `EuclideanSpace ℝ (Fin 1)`, carrying an induced topology, a coordinate homeomorphism and - analytic diffeomorphism, charted-space and manifold instances, tangent-coordinate - infrastructure, and a map to physical `Space 1`. Lighter per-system configuration-space - types exist for the sliding pendulum (support position and string angle) and, as a - `sorry` stub only, for the coplanar double pendulum. + 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) @@ -33,64 +29,6 @@ Requirements: done: false location: N/A - - description: > - A concrete configuration-space type for the geometric harmonic oscillator is defined, - wrapping a single chosen global coordinate valued in `EuclideanSpace ℝ (Fin 1)`, with - extensionality and a function-like coordinate accessor. - done: true - location: > - Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean - (ConfigurationSpace, ConfigurationSpace.ext, ConfigurationSpace.coe_apply) - - - description: > - The configuration space of the geometric harmonic oscillator carries a topology induced - by its chosen coordinate, and a coordinate equivalence and homeomorphism to its - `EuclideanSpace ℝ (Fin 1)` model. - done: true - location: > - Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean - (ConfigurationSpace.valEquiv, ConfigurationSpace.valHomeomorphism) - - - description: > - The configuration space of the geometric harmonic oscillator is equipped with a - charted-space and analytic-manifold structure, and the global chart is upgraded to an - analytic diffeomorphism onto `EuclideanSpace ℝ (Fin 1)`. - done: true - location: > - Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean - (ConfigurationSpace.valDiffeomorph) - - - description: > - Tangent-coordinate infrastructure on the geometric harmonic oscillator configuration - space: normed-vector-space structure on tangent spaces and the chart-induced continuous - linear equivalence `tangentCoord` from each tangent space to the coordinate model. - done: true - location: > - Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean (tangentCoord) - - - description: > - A map from the geometric harmonic oscillator configuration space to physical - one-dimensional space `Space 1`, reading off the underlying coordinate. - done: true - location: > - Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean - (ConfigurationSpace.toSpace, ConfigurationSpace.toSpace_apply) - - - description: > - A configuration-space type for the sliding pendulum, whose generalized coordinates are - the horizontal support position and the angle of the string from the vertical. - done: true - location: > - Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean - (ConfigurationSpace, ConfigurationSpace.supportPosition, ConfigurationSpace.angle) - - - description: > - A configuration-space type for the coplanar double pendulum. Present only as a - `sorry`-backed stub (`def ConfigurationSpace : Type := sorry`), so not counted as - implemented. - 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 diff --git a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml index 8917afd0b..303a96ff0 100644 --- a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml +++ b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml @@ -3,24 +3,25 @@ version: v0.1 Title: Configuration space for pendulum Overview: | - The pendulum is a simple example of a classical-mechanical system whose key data - structure is its configuration space. This API covers the pendulum problems from - Landau & Lifshitz, Mechanics, Chapter 1, Section 5. - - Current state (partial): the sliding pendulum (`SlidingPendulum.lean`) has a genuine - configuration space `structure ConfigurationSpace` with generalized coordinates - `supportPosition : ℝ` (the horizontal position of the support mass) and - `angle : Real.Angle` (the angle the string makes with the vertical). The coplanar - double pendulum (`CoplanarDoublePendulum.lean`) declares `ConfigurationSpace` but it - is still `sorry` (`@[sorryful] def ConfigurationSpace : Type := sorry`), so it is not - treated as defined here. The miscellaneous pivot-motion file - (`MiscellaneousPendulumPivotMotions.lean`) contains only documentation and no - declarations. - - The remaining requirements (a manifold structure on the configuration - space, a map to `Space` giving the position in real space, a trajectory based on the + 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. + + Current state (partial): the sliding pendulum (`SlidingPendulum.lean`) has a + genuine configuration space `structure ConfigurationSpace` with generalized + coordinates `supportPosition : ℝ` (the horizontal position of the support mass) + and `angle : Real.Angle` (the angle the string makes with the vertical). The + coplanar double pendulum (`CoplanarDoublePendulum.lean`) declares + `ConfigurationSpace` but it is still a placeholder stub, so it is not treated as + defined here. The miscellaneous pivot-motion file contains only documentation + and no declarations. + + The remaining requirements (a manifold structure on the configuration space, a + map to `Space` giving the position in real space, a trajectory based on the configuration space, and the lagrangian) are not yet implemented in the Pendulum - directory and are marked undone below. + directory; they are recorded below with location N/A. ParentAPIs: - Classical mechanics Lagrangian (Physlib/ClassicalMechanics/Lagrangian) From d5e63283b112a6302cbfcd0874179992768e3930 Mon Sep 17 00:00:00 2001 From: Robert Sneiderman Date: Wed, 22 Jul 2026 15:05:32 -0500 Subject: [PATCH 4/4] docs(classical-mechanics): pendulum overview describes the physics coverage, not the files --- .../ClassicalMechanics/Pendulum/API-map.yaml | 20 +++++++------------ 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml index 303a96ff0..cebdc018a 100644 --- a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml +++ b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml @@ -9,19 +9,13 @@ Overview: | covers the pendulum problems of Landau and Lifshitz, Mechanics, 3rd ed., Chapter 1, Section 5. - Current state (partial): the sliding pendulum (`SlidingPendulum.lean`) has a - genuine configuration space `structure ConfigurationSpace` with generalized - coordinates `supportPosition : ℝ` (the horizontal position of the support mass) - and `angle : Real.Angle` (the angle the string makes with the vertical). The - coplanar double pendulum (`CoplanarDoublePendulum.lean`) declares - `ConfigurationSpace` but it is still a placeholder stub, so it is not treated as - defined here. The miscellaneous pivot-motion file contains only documentation - and no declarations. - - The remaining requirements (a manifold structure on the configuration space, a - map to `Space` giving the position in real space, a trajectory based on the - configuration space, and the lagrangian) are not yet implemented in the Pendulum - directory; they are recorded below with location N/A. + 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)