Improve how references are used throughout Physlib

Physlib/ClassicalFieldTheory/Local/Variation.lean

@@ -28,6 +28,7 @@ predicate rather than introducing a second support calculus.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -80,13 +80,15 @@ In the `Solution` module:
 ## iv. References
 
 References for the damped harmonic oscillator include:
-- Landau & Lifshitz, Mechanics, page 76, section 25.
-- Goldstein, Classical Mechanics, Chapter 2.
+
+* Landau & Lifshitz, Mechanics, page 76, section 25. [ref: landau_mechanics]
+* Goldstein, Classical Mechanics, Chapter 6, Section 6.5 (Forced Vibrations and the Effect of
+  Dissipative Forces). [ref: goldstein_classicalmechanics]
 
 References for the Caldirola–Kanai lagrangian include:
-- Caldirola, Nuovo Cimento 18 (1941) 393.
-- Kanai, Progress of Theoretical Physics 3 (1948) 440.
 
+* Caldirola, Nuovo Cimento 18 (1941) 393. [ref: caldirola_1941]
+* Kanai, Progress of Theoretical Physics 3 (1948) 440. [ref: kanai_1948]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean

@@ -49,9 +49,10 @@ case, polynomial for the critically damped case, and hyperbolic for the overdamp
 ## iv. References
 
 References for the damped harmonic oscillator include:
-- Landau & Lifshitz, Mechanics, page 76, section 25.
-- Goldstein, Classical Mechanics, Chapter 2.
 
+* Landau & Lifshitz, Mechanics, page 76, section 25. [ref: landau_mechanics]
+* Goldstein, Classical Mechanics, Chapter 6, Section 6.5 (Forced Vibrations and the Effect of
+  Dissipative Forces). [ref: goldstein_classicalmechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/FreeParticle/Basic.lean

@@ -52,6 +52,7 @@ Newton’s law → zero acceleration → constant velocity → constant momentum
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/HamiltonsEquations.lean

@@ -21,9 +21,9 @@ applied to `(p, q)`.
 
 ## References
 
-- G. J. Sussman and J. Wisdom, "Structure and Interpretation of Classical Mechanics", Section 3.1.2.
-<https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/book-Z-H-36.html#%_sec_3.1.2>
-
+* G. J. Sussman and J. Wisdom, "Structure and Interpretation of Classical Mechanics", Section 3.1.2.
+  <https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/book-Z-H-36.html#%_sec_3.1.2>.
+  [ref: sussman_wisdom_sicm]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -85,8 +85,13 @@ In the `Solution` module:
 ## iv. References
 
 References for the classical harmonic oscillator include:
-- Landau & Lifshitz, Mechanics, page 58, section 21.
 
+* Landau & Lifshitz, Mechanics, page 58, section 21. [ref: landau_mechanics]
+
+A reference for the geometric model of position/velocity discussed in a TODO below:
+
+* https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf.
+  [ref: terek_variational_manifolds]
 -/
 
 @[expose] public section
@@ -100,7 +105,7 @@ TODO "Create a new file for the geometric model which properly models the positi
     configuration space and velocity as its tangent space, then show explicitly how this
     coordinate model is a simplification of the geometric model.
     A nice reference for such an analysis is:
-    https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf"
+    https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf [ref: terek_variational_manifolds]"
 
 /-!
 

Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean

@@ -57,8 +57,8 @@ tangent-coordinate infrastructure is used by later geometric constructions on th
 
 ## iv. References
 
-- Ivo Terek, Introductory Variational Calculus on Manifolds, page 1 (Section 1, Basic
-  definitions and examples).
+* Ivo Terek, Introductory Variational Calculus on Manifolds, page 1 (Section 1, Basic definitions
+  and examples). [ref: terek_variational_manifolds]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean

@@ -48,7 +48,8 @@ In coordinates this gives the standard expression
 
 ## iv. References
 
-- Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2.
+* Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2.
+  [ref: terek_variational_manifolds]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean

@@ -40,8 +40,8 @@ trajectory be tested as ordinary smoothness of its coordinate curve.
 
 ## iv. References
 
-- Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2 (Section 1, Basic
-  definitions and examples).
+* Ivo Terek, Introductory Variational Calculus on Manifolds, pages 1-2 (Section 1, Basic definitions
+  and examples). [ref: terek_variational_manifolds]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -64,8 +64,8 @@ prove that they satisfy the equation of motion, and prove some properties of the
 ## iv. References
 
 References for the classical harmonic oscillator include:
-- Landau & Lifshitz, Mechanics, page 58, section 21.
 
+* Landau & Lifshitz, Mechanics, page 58, section 21. [ref: landau_mechanics]
 -/
 
 TODO "Split this file into smaller modules, keeping `Solution.lean` as an umbrella import.

Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean

@@ -54,9 +54,8 @@ This is because:
 
 ## iv. References
 
-- Landau & Lifshitz, "Mechanics", §2 (The principle of least action)
-- Landau & Lifshitz, "Mechanics", §4 (The Lagrangian for a free particle)
-
+* Landau & Lifshitz, "Mechanics", §2 (The principle of least action). [ref: landau_mechanics]
+* Landau & Lifshitz, "Mechanics", §4 (The Lagrangian for a free particle). [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Mass/MassUnit.lean

@@ -23,6 +23,10 @@ To define specific mass units, we first state the existence of a
 a given mass unit, and then construct all other mass units from it. We choose to state the
 existence of the mass unit of kilograms, and construct all other mass units from that.
 
+## References
+
+* The numerical value used for the nominal solar mass. [ref: nominal_solar_mass_article]
+
 -/
 
 @[expose] public section
@@ -181,7 +185,7 @@ noncomputable def metricTons : MassUnit := scale (1000) kilograms
 noncomputable def longTons : MassUnit := scale (2240) pounds
 
 /-- The mass unit of nominal solar masses (1.988416 × 10 ^ 30 kilograms).
-  See: https://iopscience.iop.org/article/10.3847/0004-6256/152/2/41 -/
+  See: https://iopscience.iop.org/article/10.3847/0004-6256/152/2/41 [ref: nominal_solar_mass_article] -/
 noncomputable def nominalSolarMasses : MassUnit := scale (1.988416e30) kilograms
 
 /-!

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean

@@ -101,9 +101,9 @@ energy bounds characteristic of libration and rotation — follow in `SimplePend
 ## iv. References
 
 References for the simple gravity pendulum include:
-- Landau & Lifshitz, Mechanics, 3rd ed., §5 and §21.
-- Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4.
 
+* Landau & Lifshitz, Mechanics, 3rd ed., §5 and §21. [ref: landau_mechanics]
+* Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4. [ref: arnold_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Equilibria.lean

@@ -62,11 +62,11 @@ this module.
 ## iv. References
 
 References for the equilibria and the energy regimes of the simple pendulum include:
-- Landau & Lifshitz, Mechanics, 3rd ed., §11 (motion in one dimension: the turning points, and
-  finite and infinite motion according to the energy).
-- Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4 (the phase portrait of the
-  pendulum).
 
+* Landau & Lifshitz, Mechanics, 3rd ed., §11 (motion in one dimension: the turning points, and
+  finite and infinite motion according to the energy). [ref: landau_mechanics]
+* Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4 (the phase portrait of the
+  pendulum). [ref: arnold_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean

@@ -55,9 +55,9 @@ points upwards.
 
 ## iv. References
 
-- Landau & Lifshitz, Mechanics, 3rd ed., §5, Problems 1–3 (pendulum configurations).
-- Mathlib, `Mathlib.Geometry.Manifold.Instances.Sphere` (the manifold structure on `Circle`).
-
+* Landau & Lifshitz, Mechanics, 3rd ed., §5, Problems 1–3 (pendulum configurations).
+  [ref: landau_mechanics]
+* Mathlib, `Mathlib.Geometry.Manifold.Instances.Sphere` (the manifold structure on `Circle`).
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/PhysicalSpace.lean

@@ -45,12 +45,12 @@ the trajectory module.
 
 ## iv. References
 
-- `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic` (the lifted dynamics: the
-  energies and the Lagrangian on the Euclidean lift of the angle).
-- `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Trajectory` (trajectories on
-  the configuration circle and the position of the bob along them).
-- Landau & Lifshitz, Mechanics, 3rd ed., §5, Problems 1–3 (pendulum configurations).
-
+* `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic` (the lifted dynamics: the energies and
+  the Lagrangian on the Euclidean lift of the angle).
+* `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Trajectory` (trajectories on the
+  configuration circle and the position of the bob along them).
+* Landau & Lifshitz, Mechanics, 3rd ed., §5, Problems 1–3 (pendulum configurations).
+  [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean

@@ -46,11 +46,10 @@ physical space, on the position of the bob in the plane.
 
 ## iv. References
 
-- `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Basic` (the configuration
-  circle, the angular lift `ofAngle` and the map to physical space).
-- `Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Trajectory` (the corresponding
-  trajectory module of the harmonic oscillator, whose structure this module follows).
-
+* `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Basic` (the configuration circle,
+  the angular lift `ofAngle` and the map to physical space).
+* `Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Trajectory` (the corresponding trajectory
+  module of the harmonic oscillator, whose structure this module follows).
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean

@@ -60,11 +60,11 @@ lift of the angle they are equivalent to the equation of motion of `SimplePendul
 ## iv. References
 
 References for the Hamiltonian formulation of the simple pendulum include:
-- Landau & Lifshitz, Mechanics, 3rd ed., §40, for the canonical momentum, the Hamiltonian as
-  the Legendre transform of the Lagrangian, and Hamilton's equations.
-- The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic`, whose Lagrangian,
-  energy and equation of motion this module reformulates.
 
+* Landau & Lifshitz, Mechanics, 3rd ed., §40, for the canonical momentum, the Hamiltonian as the
+  Legendre transform of the Lagrangian, and Hamilton's equations. [ref: landau_mechanics]
+* The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic`, whose Lagrangian, energy
+  and equation of motion this module reformulates.
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/LiftInvariance.lean

@@ -49,9 +49,9 @@ level of configuration-space trajectories comes with the geometric bridge in a l
 ## iv. References
 
 References for the simple gravity pendulum include:
-- Landau & Lifshitz, Mechanics, 3rd ed., §5 and §21.
-- Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4.
 
+* Landau & Lifshitz, Mechanics, 3rd ed., §5 and §21. [ref: landau_mechanics]
+* Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4. [ref: arnold_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean

@@ -82,15 +82,14 @@ integral.
 
 ## iv. References
 
-- Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1: `T = 4 √(l/g) K(sin ½φ₀)`, in the
-  modulus convention `K(k) = ∫ φ in 0..π/2, (1 - k² sin² φ)^(-1/2)`.
-- M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, 17.3.1 (the parameter
-  convention `K(m)`, `m = k²`, used by `Real.completeEllipticK`).
-- The module `Physlib.Mathematics.SpecialFunctions.EllipticIntegral`, for `completeEllipticK`
-  and its theory on the domain `m < 1`.
-- The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.SmallAngle`, for the
-  small-angle period `smallAnglePeriod = 2π √(ℓ/g)`.
-
+* Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1: `T = 4 √(l/g) K(sin ½φ₀)`, in the modulus
+  convention `K(k) = ∫ φ in 0..π/2, (1 - k² sin² φ)^(-1/2)`. [ref: landau_mechanics]
+* M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, 17.3.1 (the parameter convention
+  `K(m)`, `m = k²`, used by `Real.completeEllipticK`). [ref: abramowitz_stegun_1964]
+* The module `Physlib.Mathematics.SpecialFunctions.EllipticIntegral`, for `completeEllipticK` and
+  its theory on the domain `m < 1`.
+* The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.SmallAngle`, for the small-angle
+  period `smallAnglePeriod = 2π √(ℓ/g)`.
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/SmallAngle.lean

@@ -111,11 +111,11 @@ cubically small in the angle.
 ## iv. References
 
 References for the small-angle motion of the simple pendulum include:
-- Huygens, Horologium Oscillatorium (1673).
-- Landau & Lifshitz, Mechanics, 3rd ed., §21.
-- The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic`, whose equation of
-  motion this module linearizes.
 
+* Huygens, Horologium Oscillatorium (1673). [ref: huygens_1673]
+* Landau & Lifshitz, Mechanics, 3rd ed., §21. [ref: landau_mechanics]
+* The module `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic`, whose equation of motion
+  this module linearizes.
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Solution.lean

@@ -75,15 +75,15 @@ the time since release.
 
 References for the motion of the pendulum, its phase plane, and the existence and uniqueness
 theorem for ordinary differential equations include:
-- Landau & Lifshitz, Mechanics, 3rd ed., §11, for motion in one dimension.
-- Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4, for the phase plane of the
-  pendulum.
-- Arnold, Ordinary Differential Equations, Chapter 4 (Proofs of the main theorems), for the
-  existence and uniqueness theorem by Picard iteration.
+
+* Landau & Lifshitz, Mechanics, 3rd ed., §11, for motion in one dimension. [ref: landau_mechanics]
+* Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., §4, for the phase plane of the
+  pendulum. [ref: arnold_mechanics]
+* Arnold, Ordinary Differential Equations, Chapter 4 (Proofs of the main theorems), for the
+  existence and uniqueness theorem by Picard iteration. [ref: arnold_ode]
 
 The reduction to a first-order system on the phase space follows
 `DampedHarmonicOscillator.equationOfMotion_unique`.
-
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean

@@ -18,7 +18,8 @@ position `r` moves with velocity `ω × r`, so the body's angular momentum about
 `L = I ω`.
 
 ## References
-- Landau and Lifshitz, Mechanics, Section 32.
+
+* Landau and Lifshitz, Mechanics, Section 32. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean

@@ -45,7 +45,8 @@ dimensions its dual is the *body-frame angular velocity vector* `ω_body = Ω_bo
 velocity `ω` resolved along the body-fixed axes, `ω_body = Rᵀ ω`.
 
 ## References
-- Landau and Lifshitz, Mechanics, Sections 31 and 32.
+
+* Landau and Lifshitz, Mechanics, Sections 31 and 32. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/RigidBody/Basic.lean

@@ -26,7 +26,8 @@ reference frame. The parallel-axis theorem expresses it in terms of the inertia
 centre of mass.
 
 ## References
-- Landau and Lifshitz, Mechanics, page 100, Section 32
+
+* Landau and Lifshitz, Mechanics, page 100, Section 32. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean

@@ -31,7 +31,8 @@ smooth for any motion; for differentiable motions it agrees with the honest poin
 `∂ₜ (displacement · y)`, recovering `T = ½ ∫ ⟪v, v⟫ dm` (`kineticEnergy_eq_integral_velocity`).
 
 ## References
-- Landau and Lifshitz, Mechanics, Section 32.
+
+* Landau and Lifshitz, Mechanics, Section 32. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/RigidBody/Motion.lean

@@ -22,7 +22,8 @@ momentum. The reference point is taken to be the centre of mass, following the d
 a rigid motion into a translation of the centre of mass plus a rotation about it.
 
 ## References
-- Landau and Lifshitz, Mechanics, Section 32.
+
+* Landau and Lifshitz, Mechanics, Section 32. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Scattering/RigidSphere.lean

@@ -12,7 +12,7 @@ public import Physlib.Meta.TODO.Basic
 
 ## References
 
-- Landau and Lifshitz, Mechanics, page 50, Section 18, Problem 1
+* Landau and Lifshitz, Mechanics, page 50, Section 18, Problem 1. [ref: landau_mechanics]
 -/
 
 @[expose] public section

Physlib/ClassicalMechanics/Vibrations/LinearTriatomic.lean

@@ -12,7 +12,7 @@ public import Physlib.Meta.TODO.Basic
 
 ## References
 
-- Landau and Lifshitz, Mechanics, page 72, Section 24, Problem 1
+* Landau and Lifshitz, Mechanics, page 72, Section 24, Problem 1. [ref: landau_mechanics]
 -/
 
 @[expose] public section