diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/API-map.yaml new file mode 100644 index 000000000..dbc405fea --- /dev/null +++ b/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) diff --git a/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml b/Physlib/ClassicalMechanics/Lagrangian/API-map.yaml new file mode 100644 index 000000000..3594e3f74 --- /dev/null +++ b/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 diff --git a/Physlib/ClassicalMechanics/Pendulum/API-map.yaml b/Physlib/ClassicalMechanics/Pendulum/API-map.yaml new file mode 100644 index 000000000..cebdc018a --- /dev/null +++ b/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"