diff --git a/Physlib/ClassicalFieldTheory/Local/Variation.lean b/Physlib/ClassicalFieldTheory/Local/Variation.lean
index 942899ddbf..bbf9a87ae3 100644
--- a/Physlib/ClassicalFieldTheory/Local/Variation.lean
+++ b/Physlib/ClassicalFieldTheory/Local/Variation.lean
@@ -28,6 +28,7 @@ predicate rather than introducing a second support calculus.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
index 2f7b49fbff..19fd33ab1f 100644
--- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean
index dae7a7bf10..d4019935bf 100644
--- a/Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean
index 7609b89b3f..d9acf9d1e9 100644
--- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean
+++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean
@@ -52,6 +52,7 @@ Newton’s law → zero acceleration → constant velocity → constant momentum
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/ClassicalMechanics/HamiltonsEquations.lean b/Physlib/ClassicalMechanics/HamiltonsEquations.lean
index 71d0ed6d01..a1e79b5dde 100644
--- a/Physlib/ClassicalMechanics/HamiltonsEquations.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean
index 4aad8f5a13..8100b914a6 100644
--- a/Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean
+++ b/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]"
 
 /-!
 
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean
index 6c6003aba3..a4392f4028 100644
--- a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Basic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean
index ccdaf6bdd9..f2e492c6ea 100644
--- a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/KineticEnergy.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean
index af6f0d4c53..4b67ff9e74 100644
--- a/Physlib/ClassicalMechanics/HarmonicOscillator/Geometric/Trajectory.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean
index 1fb84c320d..da7ee06119 100644
--- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean
+++ b/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.
diff --git a/Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean b/Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
index 6bc2d46457..356a2561b8 100644
--- a/Physlib/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Mass/MassUnit.lean b/Physlib/ClassicalMechanics/Mass/MassUnit.lean
index 4b1ff71a08..71a7ea4a8a 100644
--- a/Physlib/ClassicalMechanics/Mass/MassUnit.lean
+++ b/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
 
 /-!
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean
index f39faa256c..352ce8bbd1 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Basic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Equilibria.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Equilibria.lean
index a665994e2a..7f98d10765 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Equilibria.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean
index c82f4e8da6..1b28933a1a 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/PhysicalSpace.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/PhysicalSpace.lean
index db5f5c0c6a..1c6abfb821 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/PhysicalSpace.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean
index 5153e05ee8..6f5fe149ab 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Trajectory.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean
index dfe4e6644e..cdab3617d2 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Hamiltonian.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/LiftInvariance.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/LiftInvariance.lean
index a46d04bf4f..6d1e41d3c3 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/LiftInvariance.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean
index 6f12ae4cad..080619d438 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/PeriodFormula.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/SmallAngle.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/SmallAngle.lean
index 4bf9396dda..61395c067d 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/SmallAngle.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Solution.lean b/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Solution.lean
index 3987bb7690..182298cee3 100644
--- a/Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Solution.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean b/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean
index a6bc61f19c..063a3b0380 100644
--- a/Physlib/ClassicalMechanics/RigidBody/AngularMomentum.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean b/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean
index c3c91dec36..0b3b853996 100644
--- a/Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/RigidBody/Basic.lean b/Physlib/ClassicalMechanics/RigidBody/Basic.lean
index 18c4f156a9..80a5b5539f 100644
--- a/Physlib/ClassicalMechanics/RigidBody/Basic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean b/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean
index 906615f498..f7731c7bb2 100644
--- a/Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/RigidBody/Motion.lean b/Physlib/ClassicalMechanics/RigidBody/Motion.lean
index 32f1004db5..02daf1fe80 100644
--- a/Physlib/ClassicalMechanics/RigidBody/Motion.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Scattering/RigidSphere.lean b/Physlib/ClassicalMechanics/Scattering/RigidSphere.lean
index 4d1a8dc640..10113a2cad 100644
--- a/Physlib/ClassicalMechanics/Scattering/RigidSphere.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/Vibrations/LinearTriatomic.lean b/Physlib/ClassicalMechanics/Vibrations/LinearTriatomic.lean
index 569358b8a6..b2f2eab68d 100644
--- a/Physlib/ClassicalMechanics/Vibrations/LinearTriatomic.lean
+++ b/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
diff --git a/Physlib/ClassicalMechanics/WaveEquation/Basic.lean b/Physlib/ClassicalMechanics/WaveEquation/Basic.lean
index 898c9f580b..d5e840e2c0 100644
--- a/Physlib/ClassicalMechanics/WaveEquation/Basic.lean
+++ b/Physlib/ClassicalMechanics/WaveEquation/Basic.lean
@@ -39,6 +39,7 @@ By a plne wave we mean a function of the form `f(t, x) = f₀(⟪x, s⟫_ℝ - c
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/CondensedMatter/Thermoelectric/Basic.lean b/Physlib/CondensedMatter/Thermoelectric/Basic.lean
index 8bbbcf8b6f..fff71ce126 100644
--- a/Physlib/CondensedMatter/Thermoelectric/Basic.lean
+++ b/Physlib/CondensedMatter/Thermoelectric/Basic.lean
@@ -68,11 +68,10 @@ units, following the convention of `Physlib.Thermodynamics.IdealGas.Basic`.
 
 ## iv. References
 
-- Ioffe, A.F., *Semiconductor Thermoelements and Thermoelectric Cooling*,
-  Infosearch (1957).
-- Snyder, G.J., Toberer, E.S., *Complex thermoelectric materials*,
-  Nature Materials 7, 105–114 (2008).
-
+* Ioffe, A.F., Semiconductor Thermoelements and Thermoelectric Cooling, Infosearch (1957).
+  [ref: ioffe_1957]
+* Snyder, G.J., Toberer, E.S., Complex thermoelectric materials, Nature Materials 7, 105–114
+  (2008). [ref: snyder_toberer_2008]
 -/
 
 @[expose] public section
diff --git a/Physlib/CondensedMatter/TightBindingChain/Basic.lean b/Physlib/CondensedMatter/TightBindingChain/Basic.lean
index 9e7328a89b..4a51de07bf 100644
--- a/Physlib/CondensedMatter/TightBindingChain/Basic.lean
+++ b/Physlib/CondensedMatter/TightBindingChain/Basic.lean
@@ -63,8 +63,7 @@ with periodic boundary conditions.
 
 ## iv. References
 
-- https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf
-
+* https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf. [ref: tong_statistical_physics]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Current/CircularCoil.lean b/Physlib/Electromagnetism/Current/CircularCoil.lean
index a1095e8eea..906928a7f5 100644
--- a/Physlib/Electromagnetism/Current/CircularCoil.lean
+++ b/Physlib/Electromagnetism/Current/CircularCoil.lean
@@ -23,14 +23,15 @@ electromagnetic potentials and fields around a circular coil.
 
 ## iv. References
 
-- https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf
-
+* https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf.
+  [ref: nasa_ntrs_20140002333]
 -/
 
 @[expose] public section
 
 TODO "Prove that the magnetic field around a circular current loop is as given
-  in the reference https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf."
+  in the reference https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf
+  [ref: nasa_ntrs_20140002333]."
 
 namespace Electromagnetism
 namespace DistElectromagneticPotential
diff --git a/Physlib/Electromagnetism/Current/InfiniteWire.lean b/Physlib/Electromagnetism/Current/InfiniteWire.lean
index 25367e8ba5..2ef021d562 100644
--- a/Physlib/Electromagnetism/Current/InfiniteWire.lean
+++ b/Physlib/Electromagnetism/Current/InfiniteWire.lean
@@ -37,6 +37,7 @@ carrying a steady current along the x-axis.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/Basic.lean b/Physlib/Electromagnetism/Distributional/Basic.lean
index 2c3004bf60..667a6cd857 100644
--- a/Physlib/Electromagnetism/Distributional/Basic.lean
+++ b/Physlib/Electromagnetism/Distributional/Basic.lean
@@ -36,9 +36,8 @@ spacetime to contravariant Lorentz vectors.
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
+* https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf. [ref: qmul_emt10_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/CurrentDensity.lean b/Physlib/Electromagnetism/Distributional/Dynamics/CurrentDensity.lean
index 38e1ce7e7b..6f1181153e 100644
--- a/Physlib/Electromagnetism/Distributional/Dynamics/CurrentDensity.lean
+++ b/Physlib/Electromagnetism/Distributional/Dynamics/CurrentDensity.lean
@@ -32,6 +32,7 @@ The current density is given in terms of the charge density `ρ` and the current
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean b/Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean
index 1bb99344fa..62cc64c472 100644
--- a/Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean
+++ b/Physlib/Electromagnetism/Distributional/Dynamics/IsExtrema.lean
@@ -32,6 +32,7 @@ Maxwell's equations with sources, i.e. Gauss's law and Ampère's law.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean
index 1cf702cadf..4ceb0f7476 100644
--- a/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean
+++ b/Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean
@@ -35,8 +35,7 @@ In this implementation we have set `μ₀ = 1`. It is a TODO to introduce this c
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean
index e77b0b0355..c837cf7601 100644
--- a/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean
+++ b/Physlib/Electromagnetism/Distributional/Dynamics/Lagrangian.lean
@@ -38,9 +38,8 @@ In this implementation we set `μ₀ = 1`. It is a TODO to introduce this consta
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
+* https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf. [ref: qmul_emt10_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/ElectricField.lean b/Physlib/Electromagnetism/Distributional/ElectricField.lean
index 54867b70df..e94c954447 100644
--- a/Physlib/Electromagnetism/Distributional/ElectricField.lean
+++ b/Physlib/Electromagnetism/Distributional/ElectricField.lean
@@ -31,6 +31,7 @@ In this module we define the electric field, and prove lemmas about it.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/FieldStrength.lean b/Physlib/Electromagnetism/Distributional/FieldStrength.lean
index 4ec6cdb0ae..32f170483e 100644
--- a/Physlib/Electromagnetism/Distributional/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Distributional/FieldStrength.lean
@@ -31,6 +31,7 @@ In this module we define the field strength tensor in terms of the electromagnet
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/MagneticField.lean b/Physlib/Electromagnetism/Distributional/MagneticField.lean
index 90e973906e..20db7b4e05 100644
--- a/Physlib/Electromagnetism/Distributional/MagneticField.lean
+++ b/Physlib/Electromagnetism/Distributional/MagneticField.lean
@@ -30,6 +30,7 @@ in this module for distributions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/ScalarPotential.lean b/Physlib/Electromagnetism/Distributional/ScalarPotential.lean
index 358e7401c4..513f67312a 100644
--- a/Physlib/Electromagnetism/Distributional/ScalarPotential.lean
+++ b/Physlib/Electromagnetism/Distributional/ScalarPotential.lean
@@ -33,6 +33,7 @@ the scalar potential is non-relativistic and is therefore a distribution of `Tim
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Distributional/VectorPotential.lean b/Physlib/Electromagnetism/Distributional/VectorPotential.lean
index 010d08a3bc..8745b411b7 100644
--- a/Physlib/Electromagnetism/Distributional/VectorPotential.lean
+++ b/Physlib/Electromagnetism/Distributional/VectorPotential.lean
@@ -33,6 +33,7 @@ the vector potential is non-relativistic and is therefore a distribution of `Tim
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/Basic.lean b/Physlib/Electromagnetism/Dynamics/Basic.lean
index 513934f8df..6bed1f8916 100644
--- a/Physlib/Electromagnetism/Dynamics/Basic.lean
+++ b/Physlib/Electromagnetism/Dynamics/Basic.lean
@@ -34,6 +34,7 @@ in free space in terms of these constants.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/CurrentDensity.lean b/Physlib/Electromagnetism/Dynamics/CurrentDensity.lean
index 3869cfc866..506109cff7 100644
--- a/Physlib/Electromagnetism/Dynamics/CurrentDensity.lean
+++ b/Physlib/Electromagnetism/Dynamics/CurrentDensity.lean
@@ -41,6 +41,7 @@ The current density is given in terms of the charge density `ρ` and the current
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean b/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean
index f3e69f1341..8911b73d67 100644
--- a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean
+++ b/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean
@@ -38,8 +38,8 @@ in the case of three spatial dimensions.
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
+* https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf. [ref: qmul_emt10_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean b/Physlib/Electromagnetism/Dynamics/IsExtrema.lean
index 338dc5f86f..5ef3227eb8 100644
--- a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean
+++ b/Physlib/Electromagnetism/Dynamics/IsExtrema.lean
@@ -43,6 +43,7 @@ Maxwell's equations with sources, i.e. Gauss's law and Ampère's law.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean
index 681d176df9..c280ebb1b4 100644
--- a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean
+++ b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean
@@ -53,8 +53,7 @@ In this implementation we have set `μ₀ = 1`. It is a TODO to introduce this c
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
index eefd5262db..531f9dc5a2 100644
--- a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
+++ b/Physlib/Electromagnetism/Dynamics/Lagrangian.lean
@@ -55,9 +55,8 @@ In this implementation we set `μ₀ = 1`. It is a TODO to introduce this consta
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
+* https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf. [ref: qmul_emt10_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/Boosts.lean b/Physlib/Electromagnetism/Kinematics/Boosts.lean
index 829b52aabc..fa803dffdb 100644
--- a/Physlib/Electromagnetism/Kinematics/Boosts.lean
+++ b/Physlib/Electromagnetism/Kinematics/Boosts.lean
@@ -38,9 +38,8 @@ boosts in the 'x' direction. We do this in full-generality for `d+1` space dimen
 
 ## iv. References
 
-See e.g.
-- https://en.wikipedia.org/wiki/Classical_electromagnetism_and_special_relativity
-
+* https://en.wikipedia.org/wiki/Classical_electromagnetism_and_special_relativity.
+  [ref: wiki_classical_em_and_sr]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/EMPotential.lean b/Physlib/Electromagnetism/Kinematics/EMPotential.lean
index b9be1350a6..be749eb66d 100644
--- a/Physlib/Electromagnetism/Kinematics/EMPotential.lean
+++ b/Physlib/Electromagnetism/Kinematics/EMPotential.lean
@@ -42,9 +42,8 @@ spacetime to contravariant Lorentz vectors.
 
 ## iv. References
 
-- https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
-- https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf
-
+* https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html. [ref: ucsd_ph130a_node452]
+* https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf. [ref: qmul_emt10_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/ElectricField.lean b/Physlib/Electromagnetism/Kinematics/ElectricField.lean
index fb3696ae45..4236a28154 100644
--- a/Physlib/Electromagnetism/Kinematics/ElectricField.lean
+++ b/Physlib/Electromagnetism/Kinematics/ElectricField.lean
@@ -36,6 +36,7 @@ In this module we define the electric field, and prove lemmas about it.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 649bae9da2..396220cac1 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -41,6 +41,7 @@ We define a tensor version and a matrix version and prover various properties of
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
index c3c1cc6310..bae37cbf51 100644
--- a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
+++ b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean
@@ -55,8 +55,8 @@ the field strength of a bare-gradient potential. The invariance theorem
 
 ## iv. References
 
-- https://en.wikipedia.org/wiki/Mathematical_descriptions_of_the_electromagnetic_field#Gauge_freedom
-
+* https://en.wikipedia.org/wiki/Mathematical_descriptions_of_the_electromagnetic_field#Gauge_freedom.
+  [ref: wiki_em_field_gauge_freedom]
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/MagneticField.lean b/Physlib/Electromagnetism/Kinematics/MagneticField.lean
index 1d88db0dd1..5b6f8486c1 100644
--- a/Physlib/Electromagnetism/Kinematics/MagneticField.lean
+++ b/Physlib/Electromagnetism/Kinematics/MagneticField.lean
@@ -46,6 +46,7 @@ field strength matrix. This is an antisymmetric matrix.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/ScalarPotential.lean b/Physlib/Electromagnetism/Kinematics/ScalarPotential.lean
index ba274ba3df..718b9e4197 100644
--- a/Physlib/Electromagnetism/Kinematics/ScalarPotential.lean
+++ b/Physlib/Electromagnetism/Kinematics/ScalarPotential.lean
@@ -35,6 +35,7 @@ the scalar potential is non-relativistic and is therefore a function of `Time` a
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Kinematics/VectorPotential.lean b/Physlib/Electromagnetism/Kinematics/VectorPotential.lean
index b5edd33d0f..04c32604ba 100644
--- a/Physlib/Electromagnetism/Kinematics/VectorPotential.lean
+++ b/Physlib/Electromagnetism/Kinematics/VectorPotential.lean
@@ -35,6 +35,7 @@ the vector potential is non-relativistic and is therefore a function of `Time` a
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/PointParticle/OneDimension.lean b/Physlib/Electromagnetism/PointParticle/OneDimension.lean
index 127faf8deb..0a2c154ec9 100644
--- a/Physlib/Electromagnetism/PointParticle/OneDimension.lean
+++ b/Physlib/Electromagnetism/PointParticle/OneDimension.lean
@@ -38,6 +38,7 @@ sitting at the origin in 1d space.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean b/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean
index d133ef67c2..55151d0a6f 100644
--- a/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean
+++ b/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean
@@ -40,6 +40,7 @@ sitting at the origin in 3d space.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Vacuum/Constant.lean b/Physlib/Electromagnetism/Vacuum/Constant.lean
index f270df0bd9..78dd0f51d5 100644
--- a/Physlib/Electromagnetism/Vacuum/Constant.lean
+++ b/Physlib/Electromagnetism/Vacuum/Constant.lean
@@ -34,6 +34,7 @@ electromagnetic action.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Vacuum/HarmonicWave.lean b/Physlib/Electromagnetism/Vacuum/HarmonicWave.lean
index dafcdaeee4..1203371fb5 100644
--- a/Physlib/Electromagnetism/Vacuum/HarmonicWave.lean
+++ b/Physlib/Electromagnetism/Vacuum/HarmonicWave.lean
@@ -50,6 +50,7 @@ form of a matrix rather than a vector.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean b/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
index aceb3a626a..b3ec292d39 100644
--- a/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
+++ b/Physlib/Electromagnetism/Vacuum/IsPlaneWave.lean
@@ -51,6 +51,7 @@ in general dimensions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/Basic.lean b/Physlib/FluidDynamics/Basic.lean
index 618b0f3c5a..944629af96 100644
--- a/Physlib/FluidDynamics/Basic.lean
+++ b/Physlib/FluidDynamics/Basic.lean
@@ -32,6 +32,7 @@ The structure-specific APIs are organized in the corresponding `FluidFlow`, `Cau
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/Basic.lean b/Physlib/FluidDynamics/CauchyFlow/Basic.lean
index 96cf572b4c..5004afa1ec 100644
--- a/Physlib/FluidDynamics/CauchyFlow/Basic.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/Basic.lean
@@ -37,6 +37,7 @@ for momentum balance alone.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean b/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean
index 2ae8a5a64c..9a88bc43b1 100644
--- a/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/BodyForce.lean
@@ -28,6 +28,7 @@ This module defines predicates for conservative specific body forces on `CauchyF
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean b/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean
index af0547ef09..954148f4b3 100644
--- a/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/Inviscid.lean
@@ -28,6 +28,7 @@ matrix-divergence identity for pressure stress.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/Momentum.lean b/Physlib/FluidDynamics/CauchyFlow/Momentum.lean
index 1e734f1ae0..2bd41c2270 100644
--- a/Physlib/FluidDynamics/CauchyFlow/Momentum.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/Momentum.lean
@@ -33,6 +33,7 @@ Navier-Stokes.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean b/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean
index 57150a4593..a2cb9ff36c 100644
--- a/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/NavierStokes.lean
@@ -36,6 +36,7 @@ stress law. The Cauchy momentum equation supplies the balance-law layer, while
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean b/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean
index 73d793e6f7..b670dac740 100644
--- a/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean
+++ b/Physlib/FluidDynamics/CauchyFlow/Newtonian.lean
@@ -25,6 +25,7 @@ This module defines the Newtonian constitutive stress law for `CauchyFlow`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/Euler/Basic.lean b/Physlib/FluidDynamics/Euler/Basic.lean
index 93d70b0c97..e23739459a 100644
--- a/Physlib/FluidDynamics/Euler/Basic.lean
+++ b/Physlib/FluidDynamics/Euler/Basic.lean
@@ -31,6 +31,7 @@ the Cauchy stress tensor rather than as a field of the flow data.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Basic.lean b/Physlib/FluidDynamics/FluidFlow/Basic.lean
index f96e1e3465..24202c480b 100644
--- a/Physlib/FluidDynamics/FluidFlow/Basic.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Basic.lean
@@ -33,6 +33,7 @@ only at the layer where it becomes necessary.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Continuity.lean b/Physlib/FluidDynamics/FluidFlow/Continuity.lean
index af461afdb2..b0fd99f14c 100644
--- a/Physlib/FluidDynamics/FluidFlow/Continuity.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Continuity.lean
@@ -32,6 +32,7 @@ equation, so they can be reused by Navier-Stokes, Euler, and other fluid models.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Incompressible.lean b/Physlib/FluidDynamics/FluidFlow/Incompressible.lean
index 0a76699b98..dfa192294f 100644
--- a/Physlib/FluidDynamics/FluidFlow/Incompressible.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Incompressible.lean
@@ -31,6 +31,7 @@ Navier-Stokes, incompressible Euler, and Bernoulli-style developments.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Kinematics.lean b/Physlib/FluidDynamics/FluidFlow/Kinematics.lean
index 009b3d0821..dc0d6f62d0 100644
--- a/Physlib/FluidDynamics/FluidFlow/Kinematics.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Kinematics.lean
@@ -27,6 +27,7 @@ This module defines basic kinematic scalar quantities associated to `FluidFlow`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Momentum.lean b/Physlib/FluidDynamics/FluidFlow/Momentum.lean
index 469a3b9fa6..923b2eb877 100644
--- a/Physlib/FluidDynamics/FluidFlow/Momentum.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Momentum.lean
@@ -33,6 +33,7 @@ force law or stress model, so they can be reused by Navier-Stokes, Euler, and re
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/FluidFlow/Newtonian.lean b/Physlib/FluidDynamics/FluidFlow/Newtonian.lean
index c34033acd8..8659b4f60e 100644
--- a/Physlib/FluidDynamics/FluidFlow/Newtonian.lean
+++ b/Physlib/FluidDynamics/FluidFlow/Newtonian.lean
@@ -28,6 +28,7 @@ This module defines the velocity gradient and Newtonian stress tensor associated
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean
index b63bc45964..01713aa547 100644
--- a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Basic.lean
@@ -31,6 +31,7 @@ unrelated to their statements.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
index 4ee5bcc26f..7883b47a61 100644
--- a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Bernoulli.lean
@@ -31,6 +31,7 @@ than defining a separate Bernoulli-flow structure.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean
index 0d371c7e90..caf45d45c4 100644
--- a/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean
+++ b/Physlib/FluidDynamics/ThermodynamicCauchyFlow/Isentropic.lean
@@ -26,6 +26,7 @@ This module defines the isentropic predicate for thermodynamic Cauchy flows.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/Calculus/Gradient.lean b/Physlib/Mathematics/Calculus/Gradient.lean
index 5eabec0ed2..ece9e748e6 100644
--- a/Physlib/Mathematics/Calculus/Gradient.lean
+++ b/Physlib/Mathematics/Calculus/Gradient.lean
@@ -48,8 +48,7 @@ product space. The file is deliberately real: two of its rules (`gradient_const_
 
 ## iv. References
 
-- Mathlib, `Mathlib.Analysis.Calculus.Gradient.Basic`.
-
+* Mathlib, `Mathlib.Analysis.Calculus.Gradient.Basic`.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean b/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
index 6ba3e9dcc3..31826f3a20 100644
--- a/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
+++ b/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
@@ -132,19 +132,18 @@ of §G.
 
 ## iv. References
 
-- Kreutz-Delgado, *The Complex Gradient Operator and the CR-Calculus*,
-  arXiv:0906.4835 — directional/multivariable formulation and two-term chain
-  rule (§D); second-order theory behind §G–I.
-- Mortini & Rupp, *The Clairaut–Schwarz Theorem for Mixed Wirtinger
-  Derivatives*, Bull. Iranian Math. Soc. 48 (2022), 2643–2647 — the mixed
-  holomorphic/anti-holomorphic symmetry of §I under the same `C²` hypothesis,
-  with the same reduction to real Schwarz used here.
-- Koor, Qiu, Kwek & Rebentrost, *A short tutorial on Wirtinger Calculus with
-  applications in quantum information*, arXiv:2312.04858 — companion
-  exposition of the scalar single/multivariable calculus and sign conventions.
-- *Complex differential form*, Wikipedia (section "The Dolbeault operators") — the
-  `d = ∂ + ∂̄` splitting and the `∂`/`∂̄` notation this module's operators are named after.
-
+* Kreutz-Delgado, The Complex Gradient Operator and the CR-Calculus, arXiv:0906.4835 —
+  directional/multivariable formulation and two-term chain rule (§D); second-order theory behind
+  §G–I. [ref: kreutz_delgado_cr_calculus]
+* Mortini & Rupp, The Clairaut–Schwarz Theorem for Mixed Wirtinger Derivatives, Bull. Iranian
+  Math. Soc. 48 (2022), 2643–2647 — the mixed holomorphic/anti-holomorphic symmetry of §I under the
+  same `C²` hypothesis, with the same reduction to real Schwarz used here. [ref: mortini_rupp_2022]
+* Koor, Qiu, Kwek & Rebentrost, A short tutorial on Wirtinger Calculus with applications in quantum
+  information, arXiv:2312.04858 — companion exposition of the scalar single/multivariable calculus
+  and sign conventions. [ref: koor_et_al_2023_wirtinger]
+* Complex differential form, Wikipedia (section "The Dolbeault operators") — the `d = ∂ + ∂̄`
+  splitting and the `∂`/`∂̄` notation this module's operators are named after.
+  [ref: wiki_complex_differential_form]
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
index 05d05b5cb5..aa6de38d2a 100644
--- a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
+++ b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean
@@ -44,11 +44,12 @@ on tangent spaces, varying smoothly over the manifold. This pragmatic choice all
 development while acknowledging that a more abstract ideal would involve defining metrics as
 sections of a tensor bundle (e.g., `Hom(TM ⊗ TM, ℝ)` or `TM →L[ℝ] TM →L[ℝ] ℝ`.
 
-## Reference
+## References
 
-* Barrett O'Neill, "Semi-Riemannian Geometry With Applications to Relativity" (Academic Press, 1983)
-* [Discussion on Zulip about (Pseudo) Riemannian metrics] https.
-leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric
+* Barrett O'Neill, Semi-Riemannian Geometry With Applications to Relativity, Academic Press, 1983.
+  [ref: oneill_1983_semi_riemannian]
+* Discussion on Zulip about (Pseudo) Riemannian metrics:
+  https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/InnerProductSpace/Gaussian.lean b/Physlib/Mathematics/InnerProductSpace/Gaussian.lean
index e75ad8d4b2..ff9e3f1fe2 100644
--- a/Physlib/Mathematics/InnerProductSpace/Gaussian.lean
+++ b/Physlib/Mathematics/InnerProductSpace/Gaussian.lean
@@ -47,6 +47,7 @@ For some relevant Gaussian integrals see
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/KroneckerDelta/Basic.lean b/Physlib/Mathematics/KroneckerDelta/Basic.lean
index 846e490428..c4ef1e23a1 100644
--- a/Physlib/Mathematics/KroneckerDelta/Basic.lean
+++ b/Physlib/Mathematics/KroneckerDelta/Basic.lean
@@ -36,6 +36,7 @@ determinant of a matrix of Kronecker deltas.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/KroneckerDelta/Contraction.lean b/Physlib/Mathematics/KroneckerDelta/Contraction.lean
index 9a9383da5e..fed4e3ddda 100644
--- a/Physlib/Mathematics/KroneckerDelta/Contraction.lean
+++ b/Physlib/Mathematics/KroneckerDelta/Contraction.lean
@@ -46,6 +46,7 @@ matrix determinant lemma when `det A` is a unit and Kronecker-delta matrices are
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/LeviCivita/Basic.lean b/Physlib/Mathematics/LeviCivita/Basic.lean
index b20ada7844..d92afc37cc 100644
--- a/Physlib/Mathematics/LeviCivita/Basic.lean
+++ b/Physlib/Mathematics/LeviCivita/Basic.lean
@@ -42,8 +42,7 @@ permutation via `Matrix.det_permutation`.
 
 ## iv. References
 
-- https://en.wikipedia.org/wiki/Levi-Civita_symbol
-
+* https://en.wikipedia.org/wiki/Levi-Civita_symbol. [ref: wiki_levi_civita_symbol]
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/LinearPMap.lean b/Physlib/Mathematics/LinearPMap.lean
index aebbe2a467..c28b8e2079 100644
--- a/Physlib/Mathematics/LinearPMap.lean
+++ b/Physlib/Mathematics/LinearPMap.lean
@@ -41,6 +41,7 @@ composition of partial linear maps while having the domain implicitly accounted
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/OneParameterSubgroups/Basic.lean b/Physlib/Mathematics/OneParameterSubgroups/Basic.lean
index f451c502b5..3b9ae59a6c 100644
--- a/Physlib/Mathematics/OneParameterSubgroups/Basic.lean
+++ b/Physlib/Mathematics/OneParameterSubgroups/Basic.lean
@@ -38,6 +38,7 @@ follows by differentiating two exponential representations at zero.
 
 ## iii. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean b/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean
index 2071429e51..110fc3e180 100644
--- a/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean
+++ b/Physlib/Mathematics/OneParameterSubgroups/Unitary.lean
@@ -31,9 +31,8 @@ Physlib.
 
 ## References
 
-* M. H. Stone, *Linear Transformations in Hilbert Space III. Operational Methods and Group Theory*,
-  Proc. Natl. Acad. Sci. 18 (1932), 172-175.
-
+* M. H. Stone, Linear Transformations in Hilbert Space III. Operational Methods and Group Theory,
+  Proc. Natl. Acad. Sci. 16 (1930), 172-175. [ref: stone_1930]
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/Resolvent.lean b/Physlib/Mathematics/Resolvent.lean
index 5556691d44..8141070f6b 100644
--- a/Physlib/Mathematics/Resolvent.lean
+++ b/Physlib/Mathematics/Resolvent.lean
@@ -43,6 +43,7 @@ affine reciprocal `t ↦ (z + a·t)⁻¹ = resolvent (-z) (a·t)` follow at call
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/SpecialFunctions/EllipticIntegral.lean b/Physlib/Mathematics/SpecialFunctions/EllipticIntegral.lean
index a27a171893..b94c73be3f 100644
--- a/Physlib/Mathematics/SpecialFunctions/EllipticIntegral.lean
+++ b/Physlib/Mathematics/SpecialFunctions/EllipticIntegral.lean
@@ -65,12 +65,11 @@ here. Every lemma of this file about a general parameter therefore carries its d
 
 ## iv. References
 
-- M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, §17.3 (the parameter
-  convention, 17.3.1).
-- NIST DLMF §19.7(ii) (the reciprocal-modulus transformation).
-- Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period as `K(k)`, modulus
-  convention).
-
+* M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, §17.3 (the parameter convention,
+  17.3.1). [ref: abramowitz_stegun_1964]
+* NIST DLMF §19.7(ii) (the reciprocal-modulus transformation). [ref: nist_dlmf]
+* Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period as `K(k)`, modulus
+  convention). [ref: landau_mechanics]
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/SpecialFunctions/PhysHermite.lean b/Physlib/Mathematics/SpecialFunctions/PhysHermite.lean
index 949ea91334..b2ffbe2f24 100644
--- a/Physlib/Mathematics/SpecialFunctions/PhysHermite.lean
+++ b/Physlib/Mathematics/SpecialFunctions/PhysHermite.lean
@@ -41,6 +41,7 @@ and, up to numerical factors, satisfy all of the same properties.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/Trigonometry/SinSq.lean b/Physlib/Mathematics/Trigonometry/SinSq.lean
index 99f54a1d03..98aee8286d 100644
--- a/Physlib/Mathematics/Trigonometry/SinSq.lean
+++ b/Physlib/Mathematics/Trigonometry/SinSq.lean
@@ -34,9 +34,8 @@ for every libration amplitude `|θ₀| < π`.
 
 ## iv. References
 
-- Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period, whose parameter is
-  `sin² (θ₀ / 2)`).
-
+* Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period, whose parameter is
+  `sin² (θ₀ / 2)`). [ref: landau_mechanics]
 -/
 
 @[expose] public section
diff --git a/Physlib/Mathematics/VariationalCalculus/Basic.lean b/Physlib/Mathematics/VariationalCalculus/Basic.lean
index bf4c898ccc..57c4c57704 100644
--- a/Physlib/Mathematics/VariationalCalculus/Basic.lean
+++ b/Physlib/Mathematics/VariationalCalculus/Basic.lean
@@ -71,8 +71,7 @@ configuration space, or a local chart thereof.
 
 ## References
 
-- https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Variational.20Calculus/with/529022834
-
+* https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Variational.20Calculus/with/529022834.
 -/
 
 @[expose] public section
diff --git a/Physlib/Meta/Sorry.lean b/Physlib/Meta/Sorry.lean
index e6d78dbd36..384ab32bc3 100644
--- a/Physlib/Meta/Sorry.lean
+++ b/Physlib/Meta/Sorry.lean
@@ -36,9 +36,8 @@ are correctly attributed `sorryful` and `pseudo` respectively.
 
 ## iv. References
 
-Some of the code here is adapted from from the file: `Lean.Util.CollectAxioms`
-copyright (c) 2020 Microsoft Corporation. Authored by Leonardo de Moura.
-
+* Adapted from `Lean.Util.CollectAxioms`, copyright (c) 2020 Microsoft
+  Corporation, authored by Leonardo de Moura.
 -/
 
 @[expose] public meta section
diff --git a/Physlib/Meta/TransverseTactics.lean b/Physlib/Meta/TransverseTactics.lean
index e857eeea46..735d292037 100644
--- a/Physlib/Meta/TransverseTactics.lean
+++ b/Physlib/Meta/TransverseTactics.lean
@@ -12,15 +12,15 @@ public import Physlib.Meta.TODO.Basic
 This file enables us to transverse tactics and test for conditions.
 
 ## References
-The content of this file is based on the following sources (released under the Apache 2.0 license).
 
-- https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
-- https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
+The content of this file is based on the following sources (released under the Apache 2.0
+license), with modifications made to the original content here.
 
-Modifications have been made to the original content of these files here.
-
-See also:
-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
+* https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean.
+  [ref: github_tryateachstep]
+* https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean.
+  [ref: github_leandojo_extractdata]
+* See also: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
index fabbdaba8a..3598b5a3f5 100644
--- a/Physlib/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
@@ -15,6 +15,10 @@ The Georgi-Glashow model is a grand unified theory that unifies the Standard Mod
 
 This file currently contains informal-results about the Georgi-Glashow group.
 
+## References
+
+* Baez's Grand Unified Theories notes, cited throughout below. [ref: baez_guts_notes]
+
 -/
 
 @[expose] public section
@@ -30,7 +34,7 @@ informal_definition GaugeGroupI where
 the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to
 `blockdiag (α ^ 3 g, α ^ (-2) h)`.
 
-See page 34 of https://math.ucr.edu/home/baez/guts.pdf
+See page 34 of https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition inclSM where
   deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI]
@@ -38,7 +42,7 @@ informal_definition inclSM where
 
 /-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`.
 
-See page 34 of https://math.ucr.edu/home/baez/guts.pdf
+See page 34 of https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_lemma inclSM_ker where
   deps := [``inclSM]
diff --git a/Physlib/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean
index 1ccc37b164..990392e4aa 100644
--- a/Physlib/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean
@@ -15,6 +15,11 @@ The Pati-Salam model is a petite unified theory that unifies the Standard Model
 
 This file currently contains informal-results about the Pati-Salam group.
 
+## References
+
+* Baez's Grand Unified Theories notes, cited throughout below. [ref: baez_guts_notes]
+* A reference for the kernel of `inclSM`, cited below. [ref: arxiv_2201_07245]
+
 -/
 
 @[expose] public section
@@ -35,7 +40,7 @@ informal_definition GaugeGroupI where
 group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to
 `(blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3))`.
 
-See page 54 of https://math.ucr.edu/home/baez/guts.pdf
+See page 54 of https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition inclSM where
   deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI]
@@ -43,7 +48,7 @@ informal_definition inclSM where
 
 /-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`.
 
-See footnote 10 of https://arxiv.org/pdf/2201.07245
+See footnote 10 of https://arxiv.org/pdf/2201.07245 [ref: arxiv_2201_07245]
 -/
 informal_lemma inclSM_ker where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₃SubGroup]
@@ -64,7 +69,7 @@ informal_definition gaugeGroupISpinEquiv where
 /-- The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the
 standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition gaugeGroupℤ₂SubGroup where
   deps := [``GaugeGroupI]
@@ -73,7 +78,7 @@ informal_definition gaugeGroupℤ₂SubGroup where
 /-- The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI`
 by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition GaugeGroupℤ₂ where
   deps := [``GaugeGroupI, ``gaugeGroupℤ₂SubGroup]
diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol.lean
index 386414afde..7aac19a8c4 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSol.lean
@@ -12,10 +12,11 @@ public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.P
 We give a series of properties held by solutions to the quadratic equation.
 
 In particular given a quad solution we define a map from linear solutions to quadratic solutions
-and show that it is a surjection. The main reference for this is:
+and show that it is a surjection.
 
-- https://arxiv.org/abs/2006.03588
+## References
 
+* The main reference for this is https://arxiv.org/abs/2006.03588. [ref: arxiv_2006_03588]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSolToSol.lean b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSolToSol.lean
index 326a04d160..bfe589ce2d 100644
--- a/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSolToSol.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/PlusU1/QuadSolToSol.lean
@@ -9,11 +9,11 @@ public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.P
 /-!
 # Solutions from quad solutions
 
-We use $B-L$ to form a surjective map from quad solutions to solutions. The main reference
-for this material is:
+We use $B-L$ to form a surjective map from quad solutions to solutions.
 
-- https://arxiv.org/abs/2006.03588
+## References
 
+* The main reference for this material is https://arxiv.org/abs/2006.03588. [ref: arxiv_2006_03588]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/BeyondTheStandardModel/Spin10/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/Spin10/Basic.lean
index 0e4f443287..fb344982b9 100644
--- a/Physlib/Particles/BeyondTheStandardModel/Spin10/Basic.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/Spin10/Basic.lean
@@ -14,6 +14,10 @@ public import Physlib.Particles.BeyondTheStandardModel.GeorgiGlashow.Basic
 Note: By physicists this is usually called SO(10). However, the true gauge group involved
 is Spin(10).
 
+## References
+
+* Baez's Grand Unified Theories notes, cited throughout below. [ref: baez_guts_notes]
+
 -/
 
 @[expose] public section
@@ -30,7 +34,7 @@ informal_definition GaugeGroupI where
 Precomposed with the isomorphism, `PatiSalam.gaugeGroupISpinEquiv`, between `SU(4) × SU(2) × SU(2)`
 and `Spin(6) × Spin(4)`.
 
-See page 56 of https://math.ucr.edu/home/baez/guts.pdf
+See page 56 of https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition inclPatiSalam where
   deps := [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv]
@@ -39,7 +43,7 @@ informal_definition inclPatiSalam where
 /-- The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of
 `embedPatiSalam` and `PatiSalam.inclSM`.
 
-See page 56 of https://math.ucr.edu/home/baez/guts.pdf
+See page 56 of https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 informal_definition inclSM where
   deps := [``inclPatiSalam, ``PatiSalam.inclSM]
@@ -47,6 +51,7 @@ informal_definition inclSM where
 
 /-- The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism
 from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`.
+[ref: baez_guts_notes]
 -/
 informal_definition inclGeorgiGlashow where
   deps := [``GaugeGroupI, ``GeorgiGlashow.GaugeGroupI]
diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
index 03983b715c..ef667f3922 100644
--- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -19,9 +19,8 @@ doublet.
 
 ## References
 
-- https://arxiv.org/abs/hep-ph/0605184
-- https://arxiv.org/abs/1605.03237
-
+* https://arxiv.org/abs/hep-ph/0605184. [ref: arxiv_hep_ph_0605184]
+* https://arxiv.org/abs/1605.03237. [ref: arxiv_1605_03237]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
index e065eb1f6a..5a78bcb4b3 100644
--- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean
@@ -10,11 +10,13 @@ public import Physlib.Particles.BeyondTheStandardModel.TwoHDM.Basic
 
 # The gram matrix for the two Higgs doublet model
 
-The main reference for material in this section is https://arxiv.org/pdf/hep-ph/0605184.
-
 We will show that the gram matrix of the two Higgs doublet model
 describes the gauge orbits of the configuration space.
 
+## References
+
+* The main reference for material in this section is https://arxiv.org/pdf/hep-ph/0605184. [ref: arxiv_hep_ph_0605184]
+
 -/
 
 @[expose] public section
@@ -30,7 +32,7 @@ open StandardModel
 -/
 
 /-- The Gram matrix of the two Higgs doublet.
-  This matrix is used in https://arxiv.org/abs/hep-ph/0605184. -/
+  This matrix is used in https://arxiv.org/abs/hep-ph/0605184. [ref: arxiv_hep_ph_0605184] -/
 noncomputable def gramMatrix (H : TwoHiggsDoublet) : Matrix (Fin 2) (Fin 2) ℂ :=
   !![⟪H.Φ1, H.Φ1⟫_ℂ, ⟪H.Φ2, H.Φ1⟫_ℂ; ⟪H.Φ1, H.Φ2⟫_ℂ, ⟪H.Φ2, H.Φ2⟫_ℂ]
 
diff --git a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
index 3583671c1a..7c57899f1d 100644
--- a/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
+++ b/Physlib/Particles/BeyondTheStandardModel/TwoHDM/Potential.lean
@@ -43,13 +43,11 @@ give stability properties of the potential.
 
 ## iv. References
 
-For the parameterization of the potential we follow the convention of
-- https://arxiv.org/pdf/1605.03237
-
-Stability arguments of the potential follow, in part, those from
-- https://arxiv.org/abs/hep-ph/0605184
-Although we note that we explicitly prove that one of the steps in this paper is not valid.
-
+* For the parameterization of the potential we follow the convention of
+  https://arxiv.org/pdf/1605.03237. [ref: arxiv_1605_03237]
+* Stability arguments of the potential follow, in part, those from
+  https://arxiv.org/abs/hep-ph/0605184, although we note that we explicitly prove that one of
+  the steps in this paper is not valid. [ref: arxiv_hep_ph_0605184]
 -/
 
 @[expose] public section
@@ -63,16 +61,16 @@ open StandardModel
 
 We define a type for the parameters of the Higgs potential in the 2HDM.
 
-We follow the convention of `1605.03237`, which is highlighted in the explicit construction
-of the potential itself.
+We follow the convention of `1605.03237` [ref: arxiv_1605_03237], which is highlighted in the
+explicit construction of the potential itself.
 
 We relate these parameters to the `ξ` and `η` parameters used in the gram vector formalism
-given in arXiv:hep-ph/0605184.
+given in arXiv:hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
 
 -/
 
 /-- The parameters of the Two Higgs doublet model potential.
-  Following the convention of https://arxiv.org/pdf/1605.03237. -/
+  Following the convention of https://arxiv.org/pdf/1605.03237 [ref: arxiv_1605_03237]. -/
 structure PotentialParameters where
   /-- The parameter corresponding to `m₁₁²` in the 2HDM potential. -/
   m₁₁2 : ℝ
@@ -144,7 +142,7 @@ instance : Zero PotentialParameters where
 ### A.2. Gram parameters
 
 A reparameterization of the potential parameters corresponding to `ξ` and `η` in
-arXiv:hep-ph/0605184.
+arXiv:hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
 
 -/
 
@@ -198,7 +196,7 @@ lemma η_zero : (0 : PotentialParameters).η = 0 := by
 -/
 
 /-- An example of potential parameters that serve as a counterexample to the stability
-  condition given in arXiv:hep-ph/0605184.
+  condition given in arXiv:hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
   This corresponds to the potential:
   `2 * (⟪H.Φ1, H.Φ2⟫_ℂ).im + ‖H.Φ1 - H.Φ2‖ ^ 4`
   which has the property that the quartic term is non-negative and only zero if
@@ -531,13 +529,13 @@ lemma stabilityCounterExample_not_potentialIsStable :
 ### E.3. The reduced mass term
 
 The reduced mass term is a function that helps express the stability condition.
-It is the function `J2` in https://arxiv.org/abs/hep-ph/0605184.
+It is the function `J2` in https://arxiv.org/abs/hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
 
 -/
 
 /-- A function related to the mass term of the potential, used in the stableness
   condition and equivalent to the term `J2` in
-  https://arxiv.org/abs/hep-ph/0605184. -/
+  https://arxiv.org/abs/hep-ph/0605184 [ref: arxiv_hep_ph_0605184]. -/
 noncomputable def massTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
   P.ξ (Sum.inl 0) + ∑ μ, P.ξ (Sum.inr μ) * k μ
 
@@ -577,13 +575,13 @@ lemma massTermReduced_stabilityCounterExample (k : EuclideanSpace ℝ (Fin 3)) :
 ### E.4. The reduced quartic term
 
 The reduced quartic term is a function that helps express the stability condition.
-It is the function `J4` in https://arxiv.org/abs/hep-ph/0605184.
+It is the function `J4` in https://arxiv.org/abs/hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
 
 -/
 
 /-- A function related to the quartic term of the potential, used in the stableness
   condition and equivalent to the term `J4` in
-  https://arxiv.org/abs/hep-ph/0605184. -/
+  https://arxiv.org/abs/hep-ph/0605184 [ref: arxiv_hep_ph_0605184]. -/
 noncomputable def quarticTermReduced (P : PotentialParameters) (k : EuclideanSpace ℝ (Fin 3)) : ℝ :=
   P.η (Sum.inl 0) (Sum.inl 0) + 2 * ∑ b, k b * P.η (Sum.inl 0) (Sum.inr b) +
   ∑ a, ∑ b, k a * k b * P.η (Sum.inr a) (Sum.inr b)
@@ -611,7 +609,7 @@ lemma quarticTermReduced_stabilityCounterExample_nonneg (k : EuclideanSpace ℝ
 We give some necessary and sufficient conditions for the potential to be stable
 in terms of the gram vectors.
 
-This follows the analysis in https://arxiv.org/abs/hep-ph/0605184.
+This follows the analysis in https://arxiv.org/abs/hep-ph/0605184 [ref: arxiv_hep_ph_0605184].
 
 We also give some necessary conditions.
 
@@ -884,8 +882,8 @@ lemma potentialIsStable_of_strong (P : PotentialParameters)
 
 -/
 
-/-- A lemma invalidating the step in https://arxiv.org/pdf/hep-ph/0605184 leading to
-  equation (4.4). -/
+/-- A lemma invalidating the step in https://arxiv.org/pdf/hep-ph/0605184
+  [ref: arxiv_hep_ph_0605184] leading to equation (4.4). -/
 lemma forall_reduced_exists_not_potentialIsStable :
     ∃ P, ¬ PotentialIsStable P ∧ (∀ k : EuclideanSpace ℝ (Fin 3), ‖k‖ ^ 2 ≤ 1 →
     0 ≤ quarticTermReduced P k ∧ (quarticTermReduced P k = 0 → 0 ≤ massTermReduced P k)) := by
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
index 33572ee5fa..4f3e74ddcc 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/Lemmas.lean
@@ -10,9 +10,13 @@ public import Physlib.Particles.StandardModel.AnomalyCancellation.NoGrav.One.Lin
 # Lemmas for 1 family SM Accs
 
 The main result of this file is the conclusion of this paper:
-  [Lohitsiri and Tong][Lohitsiri:2019fuu]
+  [Lohitsiri and Tong][Lohitsiri:2019fuu] [ref: Lohitsiri:2019fuu]
 
 That every solution to the ACCs without gravity satisfies for free the gravitational anomaly.
+
+## References
+
+* The main result of this file is the conclusion of this paper. [ref: Lohitsiri:2019fuu]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
index 493da05152..24bf3cb20e 100644
--- a/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
+++ b/Physlib/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean
@@ -14,8 +14,10 @@ In this file we give two parameterizations
 - `linearParameters` of solutions to the linear ACCs for 1 family
 - `linearParametersQENeqZero` of solutions to the linear ACCs for 1 family with Q and E non-zero
 
-These parameterizations are based on:
-https://arxiv.org/abs/1907.00514
+## References
+
+* These parameterizations are based on https://arxiv.org/abs/1907.00514.
+  [ref: Lohitsiri:2019fuu]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/StandardModel/Basic.lean b/Physlib/Particles/StandardModel/Basic.lean
index 70fc5f0a21..246f77a1d5 100644
--- a/Physlib/Particles/StandardModel/Basic.lean
+++ b/Physlib/Particles/StandardModel/Basic.lean
@@ -13,6 +13,10 @@ public import Mathlib.RingTheory.RootsOfUnity.Complex
 
 This file defines the basic properties of the standard model in particle physics.
 
+## References
+
+* Baez's Grand Unified Theories notes, cited throughout below. [ref: baez_guts_notes]
+
 -/
 
 @[expose] public section
@@ -281,7 +285,7 @@ lemma gaugeGroupℤ₆Hom_toU1 (α : rootsOfUnity 6 ℂ) :
 standard model, i.e., the ℤ₆-subgroup of `GaugeGroupI` with elements `(α^2 * I₃, α^(-3) * I₂, α)`,
 where `α` is a sixth complex root of unity.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 noncomputable def gaugeGroupℤ₆SubGroup : Subgroup GaugeGroupI :=
   gaugeGroupℤ₆Hom.range
@@ -307,7 +311,7 @@ instance gaugeGroupℤ₆SubGroup_normal : gaugeGroupℤ₆SubGroup.Normal where
 /-- The smallest possible gauge group of the Standard Model, i.e., the quotient of `GaugeGroupI` by
 the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 def GaugeGroupℤ₆ : Type :=
   GaugeGroupI ⧸ gaugeGroupℤ₆SubGroup
@@ -388,7 +392,7 @@ lemma gaugeGroupℤ₂Hom_toU1 (α : rootsOfUnity 2 ℂ) :
 standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ₂ subgroup of
 `gaugeGroupℤ₆SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 noncomputable def gaugeGroupℤ₂SubGroup : Subgroup GaugeGroupI :=
   gaugeGroupℤ₂Hom.range
@@ -418,7 +422,7 @@ instance gaugeGroupℤ₂SubGroup_normal : gaugeGroupℤ₂SubGroup.Normal where
 /-- The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 def GaugeGroupℤ₂ : Type :=
   GaugeGroupI ⧸ gaugeGroupℤ₂SubGroup
@@ -499,7 +503,7 @@ lemma gaugeGroupℤ₃Hom_toU1 (α : rootsOfUnity 3 ℂ) :
 standard model, i.e., the ℤ₃-subgroup of `GaugeGroupI` derived from the ℤ₃ subgroup of
 `gaugeGroupℤ₆SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 noncomputable def gaugeGroupℤ₃SubGroup : Subgroup GaugeGroupI :=
   gaugeGroupℤ₃Hom.range
@@ -529,7 +533,7 @@ instance gaugeGroupℤ₃SubGroup_normal : gaugeGroupℤ₃SubGroup.Normal where
 /-- The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by
 the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 def GaugeGroupℤ₃ : Type :=
   GaugeGroupI ⧸ gaugeGroupℤ₃SubGroup
@@ -577,7 +581,7 @@ deriving Fintype, DecidableEq
 `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model for a given choice of
 quotient.
 
-See https://math.ucr.edu/home/baez/guts.pdf
+See https://math.ucr.edu/home/baez/guts.pdf [ref: baez_guts_notes]
 -/
 def GaugeGroup : GaugeGroupQuot → Type
   | .ℤ₆ => GaugeGroupℤ₆
diff --git a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
index 11791b1b20..af6111aac1 100644
--- a/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
+++ b/Physlib/Particles/StandardModel/HiggsBoson/Basic.lean
@@ -64,9 +64,8 @@ In this module we define the Higgs field and prove some basic properties.
 
 ## iv. References
 
-- The particle data group has properties of the Higgs boson
-  [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx]
-
+* The particle data group has properties of the Higgs boson Review of Particle Physics, PDG.
+  [ref: ParticleDataGroup:2018ovx]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean
index 2cba2d097a..4d42de88f2 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/B3.lean
@@ -14,10 +14,7 @@ We define `B₃` and show that it is a double point of the cubic.
 
 # References
 
-The main reference for the material in this file is:
-
-[Allanach, Madigan and Tooby-Smith][Allanach:2021yjy]
-
+* The main reference for the material in this file. [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
index 8bbce90b0c..7543f1cdfe 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/LineY3B3.lean
@@ -16,9 +16,7 @@ is a solution to the quadratic `lineY₃B₃Charges_quad` and a double point of
 
 # References
 
-The main reference for the material in this file is:
-[Allanach, Madigan and Tooby-Smith][Allanach:2021yjy]
-
+* The main reference for the material in this file. [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
index 2c038fff98..0074b53a78 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/Basic.lean
@@ -14,10 +14,8 @@ about them.
 
 # References
 
-The main reference for the material in this file is:
-
-- https://arxiv.org/pdf/2107.07926.pdf
-
+* The main reference for the material in this file is https://arxiv.org/pdf/2107.07926.pdf.
+  [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
index dae9178f85..82b18a4a65 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/PlaneWithY3B3.lean
@@ -13,8 +13,7 @@ The plane spanned by Y₃, B₃ and third orthogonal point.
 
 # References
 
-- https://arxiv.org/pdf/2107.07926.pdf
-
+* https://arxiv.org/pdf/2107.07926.pdf. [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
index 6811c623d4..94bd16b821 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/OrthogY3B3/ToSols.lean
@@ -19,10 +19,8 @@ surjection on certain subtypes of `MSSMACC.Sols`.
 
 # References
 
-The main reference for the material in this file is:
-
-- https://arxiv.org/pdf/2107.07926.pdf
-
+* The main reference for the material in this file is https://arxiv.org/pdf/2107.07926.pdf.
+  [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Y3.lean b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Y3.lean
index 87a0f57c44..b3740aada4 100644
--- a/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Y3.lean
+++ b/Physlib/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Y3.lean
@@ -14,10 +14,8 @@ We define $Y_3$ and show that it is a double point of the cubic.
 
 # References
 
-The main reference for the material in this file is:
-
-- https://arxiv.org/pdf/2107.07926.pdf
-
+* The main reference for the material in this file is https://arxiv.org/pdf/2107.07926.pdf.
+  [ref: Allanach:2021yjy]
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/N1/Basic.lean b/Physlib/Particles/SuperSymmetry/N1/Basic.lean
index d125fa514f..e36ed003ba 100644
--- a/Physlib/Particles/SuperSymmetry/N1/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/N1/Basic.lean
@@ -82,6 +82,7 @@ is real. The species can express none of these alone.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/AllowsTerm.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/AllowsTerm.lean
index 44d333bc4b..7088ade366 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/AllowsTerm.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/AllowsTerm.lean
@@ -70,8 +70,7 @@ charge spectrum `x`, leads to a zero charge in the charges of potential term `T`
 
 ## iv. References
 
-There are no known references for the results in this file.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean
index a5cb1404aa..8bb28c3509 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Basic.lean
@@ -52,9 +52,8 @@ of the charge spectrum, which can help in searching for viable theories.
 
 ## iv. References
 
-There are no known references for charge spectra in the literature.
-They were created specifically for the purpose of Physlib.
-
+* None — these charge spectra were created specifically for the purpose of
+  Physlib; there is no external reference.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Completions.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Completions.lean
index 29aadf48a7..3d489d14fe 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Completions.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Completions.lean
@@ -49,8 +49,7 @@ are complete, and have their charges in the given subsets.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean
index 78e62cd0bd..bf20366f4c 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean
@@ -65,8 +65,7 @@ a computationally efficient way.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimalSuperSet.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimalSuperSet.lean
index 15604132a0..ec8daccf59 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimalSuperSet.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimalSuperSet.lean
@@ -42,8 +42,7 @@ In this file we define the minimal super set and prove some basic properties of
 
 ## iv. References
 
-There are no known references for the material in this file.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/Basic.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/Basic.lean
index 18c82be285..eef368fc4a 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/Basic.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/Basic.lean
@@ -49,7 +49,7 @@ We show that every charge spectrum which minimally allows `T` is of the form
 
 ## iv. References
 
-There are no known references for this material.
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/FinsetTerms.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/FinsetTerms.lean
index ae698b6a93..2df57567be 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/FinsetTerms.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/FinsetTerms.lean
@@ -43,8 +43,7 @@ We have special focus on those charge spectra which minimally allow a top and bo
 
 ## iv. References
 
-There are no references for this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/OfFinset.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/OfFinset.lean
index ddb4dd7cda..37d8e5340f 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/OfFinset.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/MinimallyAllowsTerm/OfFinset.lean
@@ -51,8 +51,7 @@ from a finset.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfFieldLabel.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfFieldLabel.lean
index 5856b9a6c9..4d3471ff25 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfFieldLabel.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfFieldLabel.lean
@@ -38,8 +38,7 @@ terms in the potential.
 
 ## iv. References
 
-There are no known references for the results in this file.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfPotentialTerm.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfPotentialTerm.lean
index e8c9432aa7..2f9708b837 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfPotentialTerm.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/OfPotentialTerm.lean
@@ -47,8 +47,7 @@ We will show that these two multisets have the same elements.
 
 ## iv. References
 
-There are no known references for this material.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoClosed.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoClosed.lean
index 50135936be..8f47f20bae 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoClosed.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoClosed.lean
@@ -61,8 +61,7 @@ which include three which are defined in this file: `IsPhenoClosedQ5`, `IsPhenoC
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoConstrained.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoConstrained.lean
index bfd14fa6bd..c77006b80b 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoConstrained.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/PhenoConstrained.lean
@@ -51,8 +51,7 @@ We define some variations of this result.
 
 ## iv. References
 
-There are no known references for the material in this file.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Yukawa.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Yukawa.lean
index 18c56f7fc1..674a56cced 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Yukawa.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Yukawa.lean
@@ -44,8 +44,7 @@ this module.
 
 ## iv. References
 
-There are no known references for this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/ZMod.lean b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/ZMod.lean
index 4dd3ee52d0..86a3bf0424 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/ZMod.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/ZMod.lean
@@ -52,8 +52,7 @@ In other files we usually just consider one.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean b/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean
index 7ff2814223..95dc060524 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/FieldLabels.lean
@@ -32,6 +32,7 @@ The key results are
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Particles/SuperSymmetry/SU5/Potential.lean b/Physlib/Particles/SuperSymmetry/SU5/Potential.lean
index ac8b565126..eaedbe317c 100644
--- a/Physlib/Particles/SuperSymmetry/SU5/Potential.lean
+++ b/Physlib/Particles/SuperSymmetry/SU5/Potential.lean
@@ -45,9 +45,8 @@ The terms of the Kahler potential are:
 
 ## iv. References
 
-- The main reference for the terms, and notation used in this module is: arXiv:0912.0853
-A previous version of this code was replaced in PR#569.
-
+* The main reference for the terms, and notation used in this module is: arXiv:0912.0853 A previous
+  version of this code was replaced in PR#569. [ref: arxiv_0912_0853]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/AnomalyCancellation/Basic.lean b/Physlib/QFT/AnomalyCancellation/Basic.lean
index 195bcf00ba..4653d24369 100644
--- a/Physlib/QFT/AnomalyCancellation/Basic.lean
+++ b/Physlib/QFT/AnomalyCancellation/Basic.lean
@@ -70,12 +70,10 @@ Related to these are the different types of spaces of charges:
 
 ## iv. References
 
-Some references on anomaly cancellation conditions are:
-- Alvarez-Gaume, L. and Ginsparg, P. H. (1985). The Structure of Gauge and
-Gravitational Anomalies.
-- Bilal, A. (2008). Lectures on Anomalies. arXiv preprint.
-- Nash, C. (1991). Differential topology and quantum field theory. Elsevier.
-
+* Alvarez-Gaume, L. and Ginsparg, P. H. (1985). The Structure of Gauge and Gravitational Anomalies.
+  [ref: alvarez_gaume_ginsparg_1985]
+* Bilal, A. (2008). Lectures on Anomalies. arXiv preprint. [ref: bilal_2008_anomalies]
+* Nash, C. (1991). Differential topology and quantum field theory. Elsevier. [ref: nash_1991_dtqft]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/PerturbationTheory/FieldSpecification/Basic.lean b/Physlib/QFT/PerturbationTheory/FieldSpecification/Basic.lean
index fcac680a66..069fbae6c3 100644
--- a/Physlib/QFT/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/Physlib/QFT/PerturbationTheory/FieldSpecification/Basic.lean
@@ -23,9 +23,10 @@ From each field we can create three different types of `FieldOp`.
 
 These states carry the same field statistic as the field they are derived from.
 
-## Some references
+## References
 
-- https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf
+* https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf.
+  [ref: ucdavis_spinorfeynrules]
 
 -/
 
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean
index b4d1a8c857..6108ab09fe 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean
@@ -76,8 +76,7 @@ conditions.
 
 ## iv. References
 
-- https://arxiv.org/pdf/1912.04804.pdf
-
+* https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean
index 59e6809bad..29e3acdcf0 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean
@@ -18,9 +18,9 @@ if the line through that point and through the two different planes formed by th
 We show that for a solution all its permutations satisfy this property, then there exists
 a permutation for which it lies in the unshifted plane.
 
-The main reference for this file is:
+## References
 
-- https://arxiv.org/pdf/1912.04804.pdf
+* The main reference for this file is https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean
index 36f614031c..1269ddef61 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean
@@ -13,9 +13,9 @@ Given maps `g : Fin n.succ → ℚ`, `f : Fin n → ℚ` and `a : ℚ` we form a
 equations. We show that every solution can be got in this way, up to permutation, unless it, up to
 permutation, lives in the unshifted plane.
 
-The main reference is:
+## References
 
-- https://arxiv.org/pdf/1912.04804.pdf
+* The main reference is https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 
 -/
 
diff --git a/Physlib/QFT/QED/AnomalyCancellation/LineInPlaneCond.lean b/Physlib/QFT/QED/AnomalyCancellation/LineInPlaneCond.lean
index e0e0674e52..b7cccc51c8 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/LineInPlaneCond.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/LineInPlaneCond.lean
@@ -16,7 +16,7 @@ We say a `LinSol` satisfies the `line in plane` condition if for all distinct `i
 We look at various consequences of this.
 The main reference for this material is
 
-- https://arxiv.org/pdf/1912.04804.pdf
+- https://arxiv.org/pdf/1912.04804.pdf [ref: arxiv_1912_04804]
 
 We will show that `n ≥ 4` the `line in plane` condition on solutions implies the
 `constAbs` condition.
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean
index b2ef0fb85d..29120794ac 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean
@@ -71,8 +71,7 @@ conditions.
 
 ## iv. References
 
-- https://arxiv.org/pdf/1912.04804.pdf
-
+* https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean
index 696608d1b0..6ebd0b4ead 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean
@@ -18,9 +18,9 @@ if the line through that point and through the two different planes formed by th
 We show that for a solution all its permutations satisfy this property,
 then the charge must be zero.
 
-The main reference for this file is:
+## References
 
-- https://arxiv.org/pdf/1912.04804.pdf
+* The main reference for this file is https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 -/
 
 @[expose] public section
diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean
index 41085efba9..e24b6ec1fc 100644
--- a/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean
+++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean
@@ -12,9 +12,9 @@ public import Physlib.QFT.QED.AnomalyCancellation.Odd.LineInCubic
 Given maps `g : Fin n → ℚ`, `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
 equations. We show that every solution can be got in this way, up to permutation, unless it is zero.
 
-The main reference is:
+## References
 
-- https://arxiv.org/pdf/1912.04804.pdf
+* The main reference is https://arxiv.org/pdf/1912.04804.pdf. [ref: arxiv_1912_04804]
 
 -/
 
diff --git a/Physlib/QuantumMechanics/FreeParticle/Basic.lean b/Physlib/QuantumMechanics/FreeParticle/Basic.lean
index 657ba42b37..decd44ec99 100644
--- a/Physlib/QuantumMechanics/FreeParticle/Basic.lean
+++ b/Physlib/QuantumMechanics/FreeParticle/Basic.lean
@@ -29,6 +29,7 @@ to the Hamiltonian `p²/2m` with no potential.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 480c38dba5..6c60052d52 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -47,6 +47,7 @@ in `d` dimensions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean
index 1f1ba488bb..0361e81d44 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Eigenstates.lean
@@ -41,6 +41,7 @@ hyperspherical harmonics. In such cases the energies only depend on the radial q
 
 ## iv. References
 
+* None.
 -/
 @[expose] public section
 
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
index 8d027fe804..068d226e0d 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
@@ -62,6 +62,7 @@ equivalence classes, essentially dropping information about the functions on the
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean
index 01372710c8..8acd841e52 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/DirichletSubmodule.lean
@@ -32,6 +32,7 @@ homogeneous Dirichlet boundary conditions on `Ω`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean
index 3521ade516..f056d12432 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Fourier.lean
@@ -35,6 +35,7 @@ equivalence of `Lp ℂ 2 volume`, hence of `SpaceDHilbertSpace d`, onto itself;
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean
index 33ef234bb0..773d7e4d42 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/MomentumStates.lean
@@ -24,8 +24,7 @@ of the dual of `𝓢(Space d, ℂ)` defined by evaluation of the Fourier transfo
 
 ## iv. References
 
-- https://en.wikipedia.org/wiki/Rigged_Hilbert_space
-
+* https://en.wikipedia.org/wiki/Rigged_Hilbert_space. [ref: wiki_rigged_hilbert_space]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean
index 605e798235..d6c517cfca 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PolyBddSchwartzSubmodule.lean
@@ -49,6 +49,7 @@ their being dense in `SpaceDHilbertSpace 0 ≅ ℂ`).
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean
index 50ab69bf33..a2a61b2d42 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/PositionStates.lean
@@ -24,8 +24,7 @@ of the dual of `𝓢(Space d, ℂ)` defined by evaluation at `x`.
 
 ## iv. References
 
-- https://en.wikipedia.org/wiki/Rigged_Hilbert_space
-
+* https://en.wikipedia.org/wiki/Rigged_Hilbert_space. [ref: wiki_rigged_hilbert_space]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
index eb7de6142b..e6789f6b43 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SchwartzSubmodule.lean
@@ -36,6 +36,7 @@ submodule into itself. It also is a convenient dense domain on which to define d
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
index d1b8209cdc..baa79dc082 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/SobolevSubmodule.lean
@@ -28,6 +28,7 @@ In this module we define the Sobolev submodules of `SpaceDHilbertSpace`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/HilbertSpaces/TensorProducts/CompleteTensorProduct.lean b/Physlib/QuantumMechanics/HilbertSpaces/TensorProducts/CompleteTensorProduct.lean
index d4f7a72b38..aeb984803d 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/TensorProducts/CompleteTensorProduct.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/TensorProducts/CompleteTensorProduct.lean
@@ -50,6 +50,7 @@ and prove that `⊗ₕ` is commutative and associative (up to linear isometric e
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Hydrogen/Basic.lean b/Physlib/QuantumMechanics/Hydrogen/Basic.lean
index 1ed9dd6842..5c776ac6ab 100644
--- a/Physlib/QuantumMechanics/Hydrogen/Basic.lean
+++ b/Physlib/QuantumMechanics/Hydrogen/Basic.lean
@@ -20,7 +20,11 @@ The standard hydrogen atom has `d=3`, `m = mₑmₚ/(mₑ + mₚ) ≈ mₑ` and
 The potential `V = -k/r` is singular at the origin. To address this we define a regularized
 Hamiltonian in which the potential is replaced by `-k·r(ε)⁻¹`, where `r(ε)² = ‖x‖² + ε²`.
 This goes by several names including "soft-core" and "truncated" Coulomb potential.
-e.g. see https://doi.org/10.1103/PhysRevA.80.032507 and https://doi.org/10.1063/1.3290740.
+
+## References
+
+* https://doi.org/10.1103/PhysRevA.80.032507. [ref: doi_physreva_80_032507]
+* https://doi.org/10.1063/1.3290740. [ref: doi_1063_1_3290740]
 
 -/
 
diff --git a/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean b/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean
index 57ab7c6d1b..fe3ff960e4 100644
--- a/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean
+++ b/Physlib/QuantumMechanics/InfiniteSquareWell/Basic.lean
@@ -30,6 +30,7 @@ trigonometric functions satisfying appropriate boundary conditions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
index aac1ecea7b..12618b686b 100644
--- a/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
+++ b/Physlib/QuantumMechanics/Operators/AngularMomentum.lean
@@ -38,6 +38,7 @@ Notation:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/Commutation.lean b/Physlib/QuantumMechanics/Operators/Commutation.lean
index 4bdbda525d..e1c5520db0 100644
--- a/Physlib/QuantumMechanics/Operators/Commutation.lean
+++ b/Physlib/QuantumMechanics/Operators/Commutation.lean
@@ -45,6 +45,7 @@ Commutator lemmas come in three flavors:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/Covariance.lean b/Physlib/QuantumMechanics/Operators/Covariance.lean
index e6207e22b7..6294d719b5 100644
--- a/Physlib/QuantumMechanics/Operators/Covariance.lean
+++ b/Physlib/QuantumMechanics/Operators/Covariance.lean
@@ -29,8 +29,7 @@ In this module we define the covariance of two partial linear maps `A` and `B` i
 
 ## iv. References
 
-- [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].
-
+* B. C. Hall, Quantum Theory for Mathematicians, Chapter 12. [ref: hall2013quantum]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/Momentum.lean b/Physlib/QuantumMechanics/Operators/Momentum.lean
index 7e74518c56..9adece071d 100644
--- a/Physlib/QuantumMechanics/Operators/Momentum.lean
+++ b/Physlib/QuantumMechanics/Operators/Momentum.lean
@@ -36,6 +36,7 @@ Notation:
 
 ## iv. References
 
+* None.
 -/
 
 TODO "Extend the domain of the momentum operator to the Sobolev space `H¹`."
diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index 7dff04e130..5ed8a5bb4b 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -57,9 +57,8 @@ through multiplication in the Fourier domain: see `Operators/Derivative.lean`.
 
 ## iv. References
 
-See examples 1.3 and 3.8 in
-- [Konrad Schmüdgen, *Unbounded Self-Adjoint Operators on Hilbert Space*][Schmudgen2012]
-
+* Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space, examples 1.3 and 3.8.
+  [ref: Schmudgen2012]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/Position.lean b/Physlib/QuantumMechanics/Operators/Position.lean
index 97b461be4b..a2ecc83789 100644
--- a/Physlib/QuantumMechanics/Operators/Position.lean
+++ b/Physlib/QuantumMechanics/Operators/Position.lean
@@ -46,6 +46,7 @@ Notation:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean
index 36940b05c1..5e4cb80466 100644
--- a/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean
+++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/Basic.lean
@@ -18,8 +18,8 @@ which are of central importance in quantum mechanics.
 
 Definitions for subsets of ℂ associated to an operator `T : H →ₗ.[ℂ] H` vary by author.
 Here we adopt those used in
-[Konrad Schmüdgen, *Unbounded Self-Adjoint Operators on Hilbert Space*][Schmudgen2012],
-summarized in the following table:
+[Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space][Schmudgen2012]
+[ref: Schmudgen2012], summarized in the following table:
 
 | Subset of ℂ | abbrev. | `D(T - z)` | `R(T - z)` | `(T - z)⁻¹` |
 | :---------- | :-----: | :--------: | :--------: | :---------: |
@@ -81,8 +81,7 @@ Main results
 
 ## iv. References
 
-- [Konrad Schmüdgen, *Unbounded Self-Adjoint Operators on Hilbert Space*][Schmudgen2012]
-
+* Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space. [ref: Schmudgen2012]
 -/
 
 TODO "Move spectral theory definitions and lemmas over to Mathlib equivalents if/when available."
diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/SelfAdjoint.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/SelfAdjoint.lean
index 19b14ec2e4..f004b86de4 100644
--- a/Physlib/QuantumMechanics/Operators/SpectralTheory/SelfAdjoint.lean
+++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/SelfAdjoint.lean
@@ -33,6 +33,7 @@ In this module we develop the spectral theory for self-adjoint operators.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean
index ca653f883d..d65384f337 100644
--- a/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean
+++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean
@@ -34,6 +34,7 @@ For each `x : H` there is an associated measure `μₓ` given by `μₓ A = ‖
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/SpectralTheory/Symmetric.lean b/Physlib/QuantumMechanics/Operators/SpectralTheory/Symmetric.lean
index 8e03c66617..2da0e3bce2 100644
--- a/Physlib/QuantumMechanics/Operators/SpectralTheory/Symmetric.lean
+++ b/Physlib/QuantumMechanics/Operators/SpectralTheory/Symmetric.lean
@@ -39,6 +39,7 @@ simply reinterprets the numerical range as a subset of ℝ.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/StateObservables/ExpectedValue.lean b/Physlib/QuantumMechanics/Operators/StateObservables/ExpectedValue.lean
index d960f82c8a..c6c4656c4f 100644
--- a/Physlib/QuantumMechanics/Operators/StateObservables/ExpectedValue.lean
+++ b/Physlib/QuantumMechanics/Operators/StateObservables/ExpectedValue.lean
@@ -24,8 +24,7 @@ defines the expectation value and the centered vector `Tψ - ⟨T⟩_ψ ψ`.
 
 ## References
 
-- [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].
-
+* B. C. Hall, Quantum Theory for Mathematicians, Chapter 12. [ref: hall2013quantum]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean b/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean
index f593942184..de9faea890 100644
--- a/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean
+++ b/Physlib/QuantumMechanics/Operators/StateObservables/Variance.lean
@@ -32,8 +32,7 @@ When `T` is symmetric, `‖ψ‖ = 1`, and `Tψ ∈ T.domain`, it also equals `
 
 ## References
 
-- [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].
-
+* B. C. Hall, Quantum Theory for Mathematicians, Chapter 12. [ref: hall2013quantum]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/Operators/Unbounded.lean b/Physlib/QuantumMechanics/Operators/Unbounded.lean
index 4660002d3e..82cabec42b 100644
--- a/Physlib/QuantumMechanics/Operators/Unbounded.lean
+++ b/Physlib/QuantumMechanics/Operators/Unbounded.lean
@@ -82,9 +82,9 @@ Results
 
 ## iv. References
 
-- [Reed and Simon, *Methods of Modern Mathematical Physics, Vol. I: Functional Analysis*][Reed1972]
-- [Konrad Schmüdgen, *Unbounded Self-Adjoint Operators on Hilbert Space*][Schmudgen2012]
-
+* Reed and Simon, Methods of Modern Mathematical Physics, Vol. I: Functional Analysis.
+  [ref: Reed1972]
+* Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space. [ref: Schmudgen2012]
 -/
 
 TODO "Prove that `IsStarNormal (T : H →ₗ.[ℂ] H)` is equivalent
diff --git a/Physlib/QuantumMechanics/Operators/Uncertainty.lean b/Physlib/QuantumMechanics/Operators/Uncertainty.lean
index dc546a1c1c..051a45f26b 100644
--- a/Physlib/QuantumMechanics/Operators/Uncertainty.lean
+++ b/Physlib/QuantumMechanics/Operators/Uncertainty.lean
@@ -45,10 +45,9 @@ to `Bψ` and `B` to `Aψ`.
 
 ## iv. References
 
-- [H. P. Robertson, *The Uncertainty Principle* (1929)][robertson1929uncertainty].
-- [E. Schrodinger, *Zum Heisenbergschen Unscharfeprinzip* (1930)][schrodinger1930heisenberg].
-- [B. C. Hall, *Quantum Theory for Mathematicians*, Chapter 12][hall2013quantum].
-
+* H. P. Robertson, The Uncertainty Principle (1929). [ref: robertson1929uncertainty]
+* E. Schrodinger, Zum Heisenbergschen Unscharfeprinzip (1930). [ref: schrodinger1930heisenberg]
+* B. C. Hall, Quantum Theory for Mathematicians, Chapter 12. [ref: hall2013quantum]
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean
index 204a9586af..e5606e43ba 100644
--- a/Physlib/QuantumMechanics/PoschlTeller/Basic.lean
+++ b/Physlib/QuantumMechanics/PoschlTeller/Basic.lean
@@ -37,8 +37,7 @@ the parameter controlling its depth is a positive integer.
 
 ## iv. References
 
-- https://arxiv.org/pdf/2411.14941
-
+* https://arxiv.org/pdf/2411.14941. [ref: arxiv_2411_14941]
 -/
 @[expose] public section
 
@@ -46,7 +45,7 @@ TODO "Define the Hamiltonian and related operators for the Pöschl-Teller quantu
 
 TODO "Develop the eigensystem of the Hamiltonian for the Pöschl-Teller quantum system
   using properties of the creation/annihilation operators
-  (e.g. following https://arxiv.org/pdf/2411.14941)."
+  (e.g. following https://arxiv.org/pdf/2411.14941 [ref: arxiv_2411_14941])."
 
 TODO "Prove that the Pöschl-Teller potential is reflectionless."
 
diff --git a/Physlib/QuantumMechanics/QuantumSystem/Basic.lean b/Physlib/QuantumMechanics/QuantumSystem/Basic.lean
index d917f828ee..85c8a601b7 100644
--- a/Physlib/QuantumMechanics/QuantumSystem/Basic.lean
+++ b/Physlib/QuantumMechanics/QuantumSystem/Basic.lean
@@ -37,6 +37,7 @@ Definitions
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean
index f4a0c75f04..50f9b85838 100644
--- a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean
+++ b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean
@@ -34,6 +34,7 @@ on a closed interval and zero elsewhere.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/QuantumMechanics/SpaceDQuantumSystem.lean b/Physlib/QuantumMechanics/SpaceDQuantumSystem.lean
index 551efb4263..2bbbd0062a 100644
--- a/Physlib/QuantumMechanics/SpaceDQuantumSystem.lean
+++ b/Physlib/QuantumMechanics/SpaceDQuantumSystem.lean
@@ -30,6 +30,7 @@ namely the number of spatial dimensions, the particle's mass and the potential f
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Fermions/Dirac/Basic.lean b/Physlib/Relativity/Fermions/Dirac/Basic.lean
index ee38828fa1..65dfb7c819 100644
--- a/Physlib/Relativity/Fermions/Dirac/Basic.lean
+++ b/Physlib/Relativity/Fermions/Dirac/Basic.lean
@@ -19,8 +19,7 @@ That is a LeftHandedWeyl and a DualRightHandedWeyl.
 
 ## References
 
-- arXiv:0812.1594 page 197.
-
+* arXiv:0812.1594 page 197. [ref: Dreiner:2008tw]
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean
index 6884f71db6..0e7c57656a 100644
--- a/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean
+++ b/Physlib/Relativity/Fermions/Weyl/DualLeftHanded.lean
@@ -21,10 +21,8 @@ and we consider them to have down indices `ψ_α` with `α = 1,2`.
 
 ### References
 
-A good reference for the material in this file is:
-https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf
-Although a different index convention is used there.
-
+* A good reference for the material in this file, although it uses a different
+  index convention: https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf. [ref: ucdavis_spinorfeynrules]
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/LorentzAlgebra/Basis.lean b/Physlib/Relativity/LorentzAlgebra/Basis.lean
index d40c2a6674..9f8322e8a5 100644
--- a/Physlib/Relativity/LorentzAlgebra/Basis.lean
+++ b/Physlib/Relativity/LorentzAlgebra/Basis.lean
@@ -33,9 +33,8 @@ block, while rotation generators are antisymmetric matrices acting only on spati
 
 ## References
 
-- Weinberg, *The Quantum Theory of Fields*, Vol 1, Section 2.7
-- Peskin & Schroeder, *An Introduction to QFT*, Appendix A
-
+* Weinberg, The Quantum Theory of Fields, Vol 1, Section 2.7. [ref: weinberg_qft1]
+* Peskin & Schroeder, An Introduction to QFT, Appendix A. [ref: peskin_schroeder_qft]
 ## Future Work
 
 TODO can be completed by proving linear independence and spanning of these
diff --git a/Physlib/Relativity/LorentzGroup/Basic.lean b/Physlib/Relativity/LorentzGroup/Basic.lean
index 7ae8ca1059..7c11825e13 100644
--- a/Physlib/Relativity/LorentzGroup/Basic.lean
+++ b/Physlib/Relativity/LorentzGroup/Basic.lean
@@ -18,9 +18,9 @@ We define the Lorentz group.
 
 ## References
 
-- *Lorentz Transformations, Rotations, and Boosts*, Jaffe.
-<https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf>
-
+* Lorentz Transformations, Rotations, and Boosts, Jaffe.
+  <https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf>.
+  [ref: jaffe_lorentz_notes]
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean b/Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean
index cccd072891..fe129e9860 100644
--- a/Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean
+++ b/Physlib/Relativity/LorentzGroup/Boosts/Generalized.lean
@@ -21,9 +21,8 @@ A boost is the special case of a generalised boost when `u = basis 0`.
 
 ## References
 
-- The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
-  https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
-
+* The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
+  https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf. [ref: cobos_2015_lorentz_group]
 -/
 
 @[expose] public section
@@ -384,11 +383,7 @@ lemma generalizedBoost_inv (u v : Velocity d) :
     minkowskiProduct_symm v.1 u.1]
   match_scalars <;> field_simp <;> ring
 
-/-- The time component of a generalised boost.
-
-A proof of this result can be found at the below link:
-https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Lorentz.20group/near/523249684
--/
+/-- The time component of a generalised boost. -/
 lemma generalizedBoost_timeComponent_eq (u v : Velocity d) :
     (generalizedBoost u v).1 (Sum.inl 0) (Sum.inl 0) = 1 +
     ‖u.1.timeComponent • v.1.spatialPart -
diff --git a/Physlib/Relativity/MinkowskiMatrix.lean b/Physlib/Relativity/MinkowskiMatrix.lean
index ff851798fd..001a13b274 100644
--- a/Physlib/Relativity/MinkowskiMatrix.lean
+++ b/Physlib/Relativity/MinkowskiMatrix.lean
@@ -51,8 +51,7 @@ This will be used to help define the Lorentz group in later files.
 
 ## iv. References
 
-No references are given here.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/SpeedOfLight.lean b/Physlib/Relativity/SpeedOfLight.lean
index 5dbb140e3e..1c58820b75 100644
--- a/Physlib/Relativity/SpeedOfLight.lean
+++ b/Physlib/Relativity/SpeedOfLight.lean
@@ -29,6 +29,7 @@ and should be thought of as the speed of light in some chosen but arbitrary syst
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/ComponentIdx/Basic.lean b/Physlib/Relativity/Tensors/ComponentIdx/Basic.lean
index 0dc461f994..a238cb8269 100644
--- a/Physlib/Relativity/Tensors/ComponentIdx/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComponentIdx/Basic.lean
@@ -33,8 +33,7 @@ component indices induced by tensor products and contractions live in sibling fi
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean b/Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean
index 61e22f9155..2b3ab25495 100644
--- a/Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean
+++ b/Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean
@@ -36,8 +36,7 @@ component choices at the contracted positions.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/ComponentIdx/Product.lean b/Physlib/Relativity/Tensors/ComponentIdx/Product.lean
index 60f2d2dde4..e91dca52ec 100644
--- a/Physlib/Relativity/Tensors/ComponentIdx/Product.lean
+++ b/Physlib/Relativity/Tensors/ComponentIdx/Product.lean
@@ -28,8 +28,7 @@ of component indices for each side of the append.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/ComponentIdx/Single.lean b/Physlib/Relativity/Tensors/ComponentIdx/Single.lean
index cb521a7ada..344b0eed84 100644
--- a/Physlib/Relativity/Tensors/ComponentIdx/Single.lean
+++ b/Physlib/Relativity/Tensors/ComponentIdx/Single.lean
@@ -29,8 +29,7 @@ color and the basis indices of that color.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean
index 6864bec217..a0ca001a61 100644
--- a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean
+++ b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean
@@ -49,6 +49,7 @@ The complementary convention keeps the replacement index in place. Contracting s
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean
index 2031873ff5..0a5bc790fa 100644
--- a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean
+++ b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean
@@ -41,6 +41,7 @@ operation live with the unit-tensor collapse theory in
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean
index 1f9deb11e5..d633d121b0 100644
--- a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean
+++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean
@@ -47,6 +47,7 @@ from the `CommRing` `crossToEnd`/`crossToSlot` algebra.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Dual.lean b/Physlib/Relativity/Tensors/Dual.lean
index ff486db50d..5a2c96f542 100644
--- a/Physlib/Relativity/Tensors/Dual.lean
+++ b/Physlib/Relativity/Tensors/Dual.lean
@@ -49,6 +49,7 @@ reindexing of the colors.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/LeviCivita/Basic.lean b/Physlib/Relativity/Tensors/LeviCivita/Basic.lean
index cb2e89fad8..0266f51685 100644
--- a/Physlib/Relativity/Tensors/LeviCivita/Basic.lean
+++ b/Physlib/Relativity/Tensors/LeviCivita/Basic.lean
@@ -39,6 +39,7 @@ components are carried by `TensorSpecies.Tensor.TensorInt.toTensor`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean b/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean
index 771c2c24b1..bbf53fb6b6 100644
--- a/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean
+++ b/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean
@@ -55,6 +55,7 @@ and the Euclidean contraction theorems evaluate those sums.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Product.lean b/Physlib/Relativity/Tensors/Product.lean
index 6128625fd4..908205f575 100644
--- a/Physlib/Relativity/Tensors/Product.lean
+++ b/Physlib/Relativity/Tensors/Product.lean
@@ -67,8 +67,8 @@ The following results exist for both `prodP` and `prodT` :
 
 ## iv. References
 
-- arXiv:2411.07667
-
+* Tooby-Smith, Formalization of physics index notation in Lean 4, arXiv:2411.07667.
+  [ref: tooby_smith_2024_index_notation]
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/RealTensor/Contraction/CrossToEnd.lean b/Physlib/Relativity/Tensors/RealTensor/Contraction/CrossToEnd.lean
index c66371f1fa..857fc88913 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Contraction/CrossToEnd.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Contraction/CrossToEnd.lean
@@ -27,6 +27,7 @@ component expansion to one finite sum.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
index 6caab05fe4..c9d2e04be3 100644
--- a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -53,10 +53,9 @@ The main definitions and statements are:
 
 ## iv. References
 
-The general formalism of Lorentz tensors and their operations is developed in
-other parts of the library; here we only specialise to the passage from real to
-complex Lorentz tensors.
-
+* None — the general formalism of Lorentz tensors and their operations is
+  developed in other parts of the library; here we only specialise to the
+  passage from real to complex Lorentz tensors.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean
index da42139ec6..6c567308a3 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean
@@ -26,6 +26,7 @@ contravariant bases.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/Relativity/Tensors/Tensorial.lean b/Physlib/Relativity/Tensors/Tensorial.lean
index 33857e0923..e5afc34091 100644
--- a/Physlib/Relativity/Tensors/Tensorial.lean
+++ b/Physlib/Relativity/Tensors/Tensorial.lean
@@ -51,8 +51,7 @@ We define the class `Tensorial` here, and provide an API around its use.
 
 ## iv. References
 
-There are no known references for this material.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
index 3bccaca7a6..48b9999f0e 100644
--- a/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
+++ b/Physlib/SpaceAndTime/Space/ConstantSliceDist.lean
@@ -47,6 +47,7 @@ lines and planes, rather then points.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/CrossProduct.lean b/Physlib/SpaceAndTime/Space/CrossProduct.lean
index b904c9367f..ac020af8d9 100644
--- a/Physlib/SpaceAndTime/Space/CrossProduct.lean
+++ b/Physlib/SpaceAndTime/Space/CrossProduct.lean
@@ -33,6 +33,7 @@ and prove various properties about it related to time derivatives and inner prod
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean b/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean
index dc8161afd8..9766708b3d 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -50,6 +50,7 @@ in the standard directions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean
index 8b890096bf..8afeb162ba 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Curl.lean
@@ -52,6 +52,7 @@ We also prove some basic vector-identities involving of the curl operator.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/DerivativeIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/DerivativeIndex.lean
index e7a5cca1f9..9e6583a3ce 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/DerivativeIndex.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/DerivativeIndex.lean
@@ -28,6 +28,7 @@ remaining independent of any specific jet or field-theory construction.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Div.lean b/Physlib/SpaceAndTime/Space/Derivatives/Div.lean
index 92f8daac28..2fb714afac 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Div.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Div.lean
@@ -37,6 +37,7 @@ properties about it.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Grad.lean b/Physlib/SpaceAndTime/Space/Derivatives/Grad.lean
index 0343ab3480..10039c7148 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Grad.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Grad.lean
@@ -53,6 +53,7 @@ of the input function with respect to each spatial coordinate.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
index af9506c204..11a43c9e4a 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Iterated.lean
@@ -37,6 +37,7 @@ of coordinate directions, and the iterated derivative is then defined by repeate
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/Laplacian.lean b/Physlib/SpaceAndTime/Space/Derivatives/Laplacian.lean
index dcdb7a4b64..590b4e0d0d 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/Laplacian.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/Laplacian.lean
@@ -31,6 +31,7 @@ functions defined on `Space d`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean b/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
index c7a61b8155..eddc791cb0 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MatrixDiv.lean
@@ -35,6 +35,7 @@ the vector field whose `i`th component is
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
index 999ac26136..2303efe8de 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
@@ -35,6 +35,7 @@ Theory development.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/DistConst.lean b/Physlib/SpaceAndTime/Space/DistConst.lean
index e169eda71c..5fb2a3672a 100644
--- a/Physlib/SpaceAndTime/Space/DistConst.lean
+++ b/Physlib/SpaceAndTime/Space/DistConst.lean
@@ -28,6 +28,7 @@ We show that the derivatives of this constant distribution are zero.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/DistOfFunction.lean b/Physlib/SpaceAndTime/Space/DistOfFunction.lean
index 8fbc194ba9..0fd7769286 100644
--- a/Physlib/SpaceAndTime/Space/DistOfFunction.lean
+++ b/Physlib/SpaceAndTime/Space/DistOfFunction.lean
@@ -36,6 +36,7 @@ to reference the underlying Schwartz maps.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean
index 20c0fb61e7..a9086fbbed 100644
--- a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean
+++ b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean
@@ -36,6 +36,7 @@ The integrability of `x ↦ ‖x‖ᵖ` on `ball 0 b` and `(ball 0 b)ᶜ` follow
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
index 9f1b1549d4..c9c6e2d1cb 100644
--- a/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
+++ b/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean
@@ -36,6 +36,7 @@ This file is equivalent to `invPowMeasure`, which will slowly be deprecated.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/IsDistBounded.lean b/Physlib/SpaceAndTime/Space/IsDistBounded.lean
index e977aef5c8..1f0c680cde 100644
--- a/Physlib/SpaceAndTime/Space/IsDistBounded.lean
+++ b/Physlib/SpaceAndTime/Space/IsDistBounded.lean
@@ -61,6 +61,7 @@ of the space.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/LengthUnit.lean b/Physlib/SpaceAndTime/Space/LengthUnit.lean
index 05dba0162a..a5c6b86ccc 100644
--- a/Physlib/SpaceAndTime/Space/LengthUnit.lean
+++ b/Physlib/SpaceAndTime/Space/LengthUnit.lean
@@ -22,6 +22,17 @@ To define specific length units, we first state the existence of a
 a given length unit, and then construct all other length units from it. We choose to state the
 existence of the length unit of meters, and construct all other length units from that.
 
+## References
+
+* The BIPM SI Brochure, for the meter, the speed of light, and SI prefixes.
+  [ref: bipm_si_brochure_2019]
+* NIST Handbook 44, Appendix C, for the international foot-based units and the international
+  nautical mile. [ref: nist_hb44_2023]
+* IAU 2012 Resolution B2, for the astronomical unit. [ref: iau_2012_resolution_b2]
+* The IAU Style Manual recommendations, for the Julian year convention used in the light-year.
+  [ref: iau_style_manual_units]
+* IAU 2015 Resolution B2, for the exact parsec convention. [ref: iau_2015_resolution_b2]
+
 -/
 
 @[expose] public section
@@ -143,17 +154,17 @@ From this choice of meters, we can define other length units by scaling meters.
 
 The references for the numerical definitions used below are:
 * the BIPM SI Brochure for the meter, the speed of light, and SI prefixes:
-  https://www.bipm.org/documents/d/guest/si-brochure-9-en-pdf
+  https://www.bipm.org/documents/d/guest/si-brochure-9-en-pdf [ref: bipm_si_brochure_2019]
 * NIST Handbook 44, Appendix C, for the international foot-based units and
   the international nautical mile:
-  https://doi.org/10.6028/NIST.HB.44-2023
+  https://doi.org/10.6028/NIST.HB.44-2023 [ref: nist_hb44_2023]
 * IAU 2012 Resolution B2 for the astronomical unit:
-  https://iauarchive.eso.org/static/resolutions/IAU2012_English.pdf
+  https://iauarchive.eso.org/static/resolutions/IAU2012_English.pdf [ref: iau_2012_resolution_b2]
 * the IAU Style Manual recommendations for the Julian year convention used in
   the light-year:
-  https://iauarchive.eso.org/publications/proceedings_rules/units/
+  https://iauarchive.eso.org/publications/proceedings_rules/units/ [ref: iau_style_manual_units]
 * IAU 2015 Resolution B2 for the exact parsec convention:
-  https://iauarchive.eso.org/static/resolutions/IAU2015_English.pdf
+  https://iauarchive.eso.org/static/resolutions/IAU2015_English.pdf [ref: iau_2015_resolution_b2]
 
 -/
 
diff --git a/Physlib/SpaceAndTime/Space/Norm/Basic.lean b/Physlib/SpaceAndTime/Space/Norm/Basic.lean
index 7d6774cdbb..6561843a87 100644
--- a/Physlib/SpaceAndTime/Space/Norm/Basic.lean
+++ b/Physlib/SpaceAndTime/Space/Norm/Basic.lean
@@ -66,6 +66,7 @@ We use properties of this power series to prove various results about distributi
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Norm/IteratedLaplacian.lean b/Physlib/SpaceAndTime/Space/Norm/IteratedLaplacian.lean
index 555e2f2061..c19bf600bb 100644
--- a/Physlib/SpaceAndTime/Space/Norm/IteratedLaplacian.lean
+++ b/Physlib/SpaceAndTime/Space/Norm/IteratedLaplacian.lean
@@ -27,6 +27,7 @@ gives a nonzero constant multiple of the Dirac delta at the origin.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Norm/Regularized.lean b/Physlib/SpaceAndTime/Space/Norm/Regularized.lean
index 41bd66c986..e943ae7738 100644
--- a/Physlib/SpaceAndTime/Space/Norm/Regularized.lean
+++ b/Physlib/SpaceAndTime/Space/Norm/Regularized.lean
@@ -29,6 +29,7 @@ This file contains basic API for regularized powers of the norm on `Space d`, na
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Space/Slice.lean b/Physlib/SpaceAndTime/Space/Slice.lean
index 4487e19d38..34600ef0de 100644
--- a/Physlib/SpaceAndTime/Space/Slice.lean
+++ b/Physlib/SpaceAndTime/Space/Slice.lean
@@ -31,8 +31,7 @@ extracts the `i`th coordinate on `Space d.succ`.
 
 ## iv. References
 
-- https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/API.20around.20.60Space.20.28d1.20.2B.20d2.29.60.20to.20.60Space.20d1.20x.20Space.20d2.60/with/556754634
-
+* https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/API.20around.20.60Space.20.28d1.20.2B.20d2.29.60.20to.20.60Space.20d1.20x.20Space.20d2.60/with/556754634.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/SpaceTime/Basic.lean b/Physlib/SpaceAndTime/SpaceTime/Basic.lean
index 745cbd140e..57a44cc3b7 100644
--- a/Physlib/SpaceAndTime/SpaceTime/Basic.lean
+++ b/Physlib/SpaceAndTime/SpaceTime/Basic.lean
@@ -62,6 +62,7 @@ allowing it to be used in tensorial expressions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/SpaceTime/Boosts.lean b/Physlib/SpaceAndTime/SpaceTime/Boosts.lean
index 0e3769ba18..24bdefb97e 100644
--- a/Physlib/SpaceAndTime/SpaceTime/Boosts.lean
+++ b/Physlib/SpaceAndTime/SpaceTime/Boosts.lean
@@ -28,9 +28,7 @@ Note that the material here currently assumes that the speed of light `c = 1`.
 
 ## iv. References
 
-See e.g.
-- https://en.wikipedia.org/wiki/Lorentz_transformation
-
+* https://en.wikipedia.org/wiki/Lorentz_transformation. [ref: wiki_lorentz_transformation]
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean b/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean
index 3dceaf282c..eddc56d7cc 100644
--- a/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean
+++ b/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean
@@ -52,6 +52,7 @@ distributions on `SpaceTime d`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/SpaceTime/LorentzAction.lean b/Physlib/SpaceAndTime/SpaceTime/LorentzAction.lean
index a84380c9a1..049731c58c 100644
--- a/Physlib/SpaceAndTime/SpaceTime/LorentzAction.lean
+++ b/Physlib/SpaceAndTime/SpaceTime/LorentzAction.lean
@@ -36,6 +36,7 @@ we define the induced action on Schwartz functions and distributions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Time/Basic.lean b/Physlib/SpaceAndTime/Time/Basic.lean
index 1bec924fd8..d12bd19cbb 100644
--- a/Physlib/SpaceAndTime/Time/Basic.lean
+++ b/Physlib/SpaceAndTime/Time/Basic.lean
@@ -61,6 +61,7 @@ or origin.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean
index ef8abfe26f..282f118e04 100644
--- a/Physlib/SpaceAndTime/Time/Derivatives.lean
+++ b/Physlib/SpaceAndTime/Time/Derivatives.lean
@@ -46,6 +46,7 @@ In this module we define and prove basic lemmas about derivatives of functions o
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/TimeAndSpace/Basic.lean b/Physlib/SpaceAndTime/TimeAndSpace/Basic.lean
index 75fb653f11..6f855507f5 100644
--- a/Physlib/SpaceAndTime/TimeAndSpace/Basic.lean
+++ b/Physlib/SpaceAndTime/TimeAndSpace/Basic.lean
@@ -53,6 +53,7 @@ The derivative and distribution results are in the namespace `Space` by conventi
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
index 1a519568e9..a0e8f12602 100644
--- a/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
+++ b/Physlib/SpaceAndTime/TimeAndSpace/ConstantTimeDist.lean
@@ -54,6 +54,7 @@ to get a Schwartz Map on `Space d`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/Action.lean b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/Action.lean
index a7e4575c9b..256a6c8044 100644
--- a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/Action.lean
+++ b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/Action.lean
@@ -32,6 +32,7 @@ the time coordinate and acts on the space coordinate by the usual Euclidean-grou
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean
index b289e50582..b51a383e0e 100644
--- a/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean
+++ b/Physlib/SpaceAndTime/TimeAndSpace/EuclideanGroup/SchwartzAction.lean
@@ -30,6 +30,7 @@ In this file we define the pullback action of the Euclidean group on Schwartz ma
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean b/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean
index a2df56b9d1..61ccd42cd0 100644
--- a/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean
+++ b/Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean
@@ -87,10 +87,10 @@ mean energies and integrability.
 
 ## 8. References
 
-* L. D. Landau & E. M. Lifshitz, *Statistical Physics, Part 1*.
+* L. D. Landau & E. M. Lifshitz, Statistical Physics, Part 1. [ref: landau_statphys1]
 * D. Tong, Cambridge Lecture Notes (sections on canonical ensemble).
-  - https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf
-  - https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf
+  - https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf [ref: tong_statphys_notes_one]
+  - https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf [ref: tong_statphys_notes_two]
 
 ## 9. Roadmap
 
diff --git a/Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean b/Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean
index e644cb8c9d..0b1900a00d 100644
--- a/Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean
+++ b/Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean
@@ -41,9 +41,8 @@ systems (addition, `nsmul`, and `congr`).
 
 ## References
 
-- L. D. Landau & E. M. Lifshitz, *Statistical Physics, Part 1*, §31.
-- D. Tong, *Lectures on Statistical Physics*, §1.3.
-
+* L. D. Landau & E. M. Lifshitz, Statistical Physics, Part 1, §31. [ref: landau_statphys1]
+* D. Tong, Lectures on Statistical Physics, §1.3. [ref: tong_statistical_physics]
 -/
 
 @[expose] public section
diff --git a/Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean b/Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean
index 59e14cf0e3..4a6eb680af 100644
--- a/Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean
+++ b/Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean
@@ -48,9 +48,9 @@ calculus identities for the canonical ensemble.
 
 ## References
 
-Same references as `Basic.lean` (Landau–Lifshitz; Tong), especially the identities
-`F = U - T S` and `U = -∂_β log Z`.
-
+* Same references as `Basic.lean`. [ref: landau_statphys1]
+* Same references as `Basic.lean`, especially the identities `F = U - T S` and
+  `U = -∂_β log Z`. [ref: tong_statistical_physics]
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Basic.lean b/Physlib/StringTheory/FTheory/SU5/Basic.lean
index e255252144..505277ca6e 100644
--- a/Physlib/StringTheory/FTheory/SU5/Basic.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Basic.lean
@@ -43,7 +43,8 @@ There are a number of important propositions in the theory.
 
 The charges are additionally constrained by the configuration `CodimensionOneConfig`,
 of the zero-section (`σ₀`) and the additional rational section (`σ₁`).
-This is detailed in the paper `arxiv:1504.05593`. In implemented here using
+This is detailed in the paper `arxiv:1504.05593` [ref: lawrie_schafer_nameki_wong_2015]. In
+implemented here using
 - `Charges.ofFinset S5 S10`: which gives the finite set of charges where the 5-bar charges
   must live in the set `S5` and the 10-bar charges must live in the set `S10`.
 
@@ -54,7 +55,6 @@ This is detailed in the paper `arxiv:1504.05593`. In implemented here using
 
 ## References
 
-This theory is looked at in the following paper:
-- arXiv:1507.05961.
-
+* Froggatt-Nielsen meets Mordell-Weil: A Phenomenological Survey of Global F-theory GUTs
+  with U(1)s (arxiv:1507.05961). [ref: arxiv_1507_05961]
 -/@[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Charges/AnomalyFree.lean b/Physlib/StringTheory/FTheory/SU5/Charges/AnomalyFree.lean
index 3dab14bab6..ace86fdbf1 100644
--- a/Physlib/StringTheory/FTheory/SU5/Charges/AnomalyFree.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Charges/AnomalyFree.lean
@@ -39,8 +39,7 @@ which do not have exotics.
 
 ## iv. References
 
-There are no known references for the material in this section.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Charges/OfRationalSection.lean b/Physlib/StringTheory/FTheory/SU5/Charges/OfRationalSection.lean
index 4b8e0e436c..96c507937d 100644
--- a/Physlib/StringTheory/FTheory/SU5/Charges/OfRationalSection.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Charges/OfRationalSection.lean
@@ -15,12 +15,13 @@ public import Mathlib.Data.Fintype.Sets
 
 Within SU(5) F-theory with 10d and 5-bar matter fields there are constraints on the
 allowed U(1) charges the fields can have.
-These constraints are determined in arXiv:1504.05593. They are related to the
+These constraints are determined in arXiv:1504.05593 [ref: lawrie_schafer_nameki_wong_2015].
+They are related to the
 distinct configurations of the zero-section (`σ₀`) relativity to the
 additional rational section (`σ₁`s) in codimension one fiber.
 For our purposes here, we currently just state the constraints found
-in arXiv:1504.05593, and leave the proof and derivation of these constraints to future
-work.
+in arXiv:1504.05593 [ref: lawrie_schafer_nameki_wong_2015], and leave the proof and derivation
+of these constraints to future work.
 
 ## ii. Key results
 
@@ -45,20 +46,17 @@ work.
 
 ## iv. References
 
-The main reference for the material in this section is the paper:
-
-Lawrie, Schafer-Nameki and Wong.
-F-theory and All Things Rational: Surveying U(1) Symmetries with Rational Sections
-<https://arxiv.org/pdf/1504.05593>. Page 6.
-
-- See also footnote 4 of 1507.05961
-
+* The main reference for the material in this section: Lawrie, Schafer-Nameki and Wong, F-theory
+  and All Things Rational: Surveying U(1) Symmetries with Rational Sections, page 6.
+  [ref: lawrie_schafer_nameki_wong_2015]
+* See also footnote 4 of 1507.05961. [ref: arxiv_1507_05961]
 -/
 
 @[expose] public section
 
 TODO "The results in this file are currently stated, but not proved.
-  They should should be proved following e.g. https://arxiv.org/pdf/1504.05593.
+  They should should be proved following e.g. https://arxiv.org/pdf/1504.05593
+  [ref: lawrie_schafer_nameki_wong_2015].
   This is a large project."
 
 namespace FTheory
diff --git a/Physlib/StringTheory/FTheory/SU5/Charges/Viable.lean b/Physlib/StringTheory/FTheory/SU5/Charges/Viable.lean
index 0b48100415..2121b5f89a 100644
--- a/Physlib/StringTheory/FTheory/SU5/Charges/Viable.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Charges/Viable.lean
@@ -90,8 +90,7 @@ will be very welcome. In particular working out a way to restrict by anomaly can
 
 ## iv. References
 
-There are no known references for the material in this section.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean
index 89c157a522..ad432dcd58 100644
--- a/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/Basic.lean
@@ -118,9 +118,8 @@ they can be derived from other data structures.
 
 ## iv. References
 
-- [1] arXiv:1401.5084
-- For an old version of the material in this module see PR #569.
-
+* Rational F-Theory GUTs without exotics (arXiv:1401.5084). [ref: arxiv_1401_5084]
+* For an old version of the material in this module see PR #569.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean
index 1af23d3566..eed9fe57d9 100644
--- a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/ChiralIndices.lean
@@ -40,8 +40,7 @@ we state them for the representation `D = (bar 3,1)_{1/3}` only:
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Completeness.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Completeness.lean
index 986e2a3b25..a39cb77d36 100644
--- a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Completeness.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Completeness.lean
@@ -59,8 +59,7 @@ are only constrained by `2` SM representations `D` and `L`.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean
index 1f6da927a7..4ddfb0738d 100644
--- a/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Fluxes/NoExotics/Elems.lean
@@ -52,8 +52,7 @@ elements of those elements.
 
 ## iv. References
 
-There are no known references for the material in this module.
-
+* None.
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/Basic.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/Basic.lean
index a521686ce8..0eb6a9def3 100644
--- a/Physlib/StringTheory/FTheory/SU5/Quanta/Basic.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Quanta/Basic.lean
@@ -46,8 +46,8 @@ properties thereof.
 
 ## iv. References
 
-A reference for the anomaly cancellation conditions is arXiv:1401.5084 equation 22.
-
+* Rational F-Theory GUTs without exotics (arXiv:1401.5084), Anomaly cancellation conditions,
+  equation 22. [ref: arxiv_1401_5084]
 -/
 
 @[expose] public section
@@ -208,8 +208,8 @@ There are two anomaly cancellation conditions in the SU(5)×U(1) model which inv
 - `∑ᵢ qᵢ² Nᵢ + 3 * ∑ₐ qₐ² Nₐ = 0` where the first sum is over all 5-bar representations and the
   second is over all 10d representations.
 
-According to arXiv:1401.5084 it is unclear whether this second condition should necessarily be
-imposed.
+According to arXiv:1401.5084 [ref: arxiv_1401_5084] it is unclear whether this second condition
+should necessarily be imposed.
 
 -/
 
diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean
index f8b8d6c726..17619bdc3e 100644
--- a/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Quanta/FiveQuanta.lean
@@ -78,8 +78,8 @@ properties thereof.
 
 ## iv. References
 
-A reference for the anomaly cancellation conditions is arXiv:1401.5084.
-
+* Rational F-Theory GUTs without exotics (arXiv:1401.5084), Anomaly cancellation
+  conditions. [ref: arxiv_1401_5084]
 -/
 
 @[expose] public section
@@ -910,9 +910,9 @@ variable [CommRing 𝓩]
   The anomaly coefficient of a `FiveQuanta` is given by the pair of integers:
   `(∑ᵢ qᵢ Nᵢ, ∑ᵢ qᵢ² Nᵢ)`.
 
-  The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084.
-  The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly,
-  see equation (23) of arXiv:1401.5084.
+  The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084
+  [ref: arxiv_1401_5084]. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly,
+  see equation (23) of arXiv:1401.5084 [ref: arxiv_1401_5084].
 -/
 def anomalyCoefficient (F : FiveQuanta 𝓩) : 𝓩 × 𝓩 :=
   ((F.map fun x => x.2.2 • x.1).sum, (F.map fun x => x.2.2 • (x.1 * x.1)).sum)
diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean
index 4c36e95b8e..af86831902 100644
--- a/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Quanta/IsViable.lean
@@ -54,8 +54,8 @@ lake exe graph --from
 
 ## iv. References
 
-The key reference for the material in this module is: arXiv:1507.05961.
-
+* Froggatt-Nielsen meets Mordell-Weil: A Phenomenological Survey of Global F-theory GUTs
+  with U(1)s (arxiv:1507.05961). [ref: arxiv_1507_05961]
 -/
 
 @[expose] public section
diff --git a/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean b/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean
index f2adeb9c84..c25506f91f 100644
--- a/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean
+++ b/Physlib/StringTheory/FTheory/SU5/Quanta/TenQuanta.lean
@@ -80,8 +80,8 @@ properties thereof.
 
 ## iv. References
 
-A reference for the anomaly cancellation conditions is arXiv:1401.5084.
-
+* Rational F-Theory GUTs without exotics (arXiv:1401.5084), Anomaly cancellation
+  conditions. [ref: arxiv_1401_5084]
 -/
 
 @[expose] public section
@@ -1053,9 +1053,9 @@ variable [CommRing 𝓩]
   The anomaly coefficient of a `TenQuanta` is given by the pair of integers:
   `(∑ᵢ qᵢ Nᵢ, 3 * ∑ᵢ qᵢ² Nᵢ)`.
 
-  The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084.
-  The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly,
-    see equation (23) of arXiv:1401.5084.
+  The first components is for the mixed U(1)-MSSM, see equation (22) of arXiv:1401.5084
+  [ref: arxiv_1401_5084]. The second component is for the mixed U(1)Y-U(1)-U(1) gauge anomaly,
+  see equation (23) of arXiv:1401.5084 [ref: arxiv_1401_5084].
 -/
 def anomalyCoefficient (F : TenQuanta 𝓩) : 𝓩 × 𝓩 :=
   ((F.map fun x => x.2.2 • x.1).sum, 3 * (F.map fun x => x.2.2 • (x.1 * x.1)).sum)
diff --git a/Physlib/Units/Basic.lean b/Physlib/Units/Basic.lean
index b618aba6da..bf7f4b72e4 100644
--- a/Physlib/Units/Basic.lean
+++ b/Physlib/Units/Basic.lean
@@ -50,8 +50,9 @@ Units within Physlib are implemented with the following convention:
 ## References
 
 Zulip chats discussing units:
-- https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units
-- https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Dimensional.20Analysis.20Revisited/with/530238303
+
+* https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/physical.20units.
+* https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Dimensional.20Analysis.20Revisited/with/530238303.
 
 ## Note
 
diff --git a/Physlib/Units/ISQDimensionBase.lean b/Physlib/Units/ISQDimensionBase.lean
index dd955080ca..bc717ac951 100644
--- a/Physlib/Units/ISQDimensionBase.lean
+++ b/Physlib/Units/ISQDimensionBase.lean
@@ -27,10 +27,9 @@ PhysLib's default `LTMCTDimensionBase` in two ways:
 
 ## References
 
-* ISO/IEC 80000-1:2009, *Quantities and units — Part 1: General*.
-* JCGM 200:2012, *International vocabulary of metrology — Basic and general concepts
-  and associated terms (VIM, 3rd edition)*.
-
+* ISO/IEC 80000-1:2009, Quantities and units — Part 1: General. [ref: iso_80000_1_2009]
+* JCGM 200:2012, International vocabulary of metrology — Basic and general concepts and associated
+  terms (VIM, 3rd edition). [ref: jcgm_200_2012]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/Action.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/Action.lean
index bcfc089076..e54fb3cd09 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/Action.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/Action.lean
@@ -37,9 +37,8 @@ for its variations are kept explicit in the API.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5.
+  [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrange.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrange.lean
index a7c3d8a68f..cd204a7b22 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrange.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrange.lean
@@ -32,9 +32,8 @@ close to the one in the book while avoiding a premature smooth structure on `Jet
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5.
+  [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrangeEquation.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrangeEquation.lean
index 1347f4488e..36ee5712ee 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrangeEquation.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/EulerLagrangeEquation.lean
@@ -36,9 +36,8 @@ Euler-Lagrange operator or any new analytic hypotheses.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  arXiv:1612.03100v2, Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics,
+  arXiv:1612.03100v2, Chapter 5, Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstOrder.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstOrder.lean
index 627f449569..468513212f 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstOrder.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstOrder.lean
@@ -42,9 +42,8 @@ case easier to state in examples and later mechanics bridges.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  arXiv:1612.03100v2, Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics,
+  arXiv:1612.03100v2, Chapter 5. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation.lean
index 693fd3956e..04922bbeb0 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation.lean
@@ -31,9 +31,8 @@ surface-level statements of the local Euler-Lagrange criterion.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Basic.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Basic.lean
index efce90c42b..e189575da3 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Basic.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Basic.lean
@@ -27,9 +27,8 @@ the linearized density before integration by parts and its Euler-Lagrange pairin
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Criterion.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Criterion.lean
index 2e760f1f85..e43531825a 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Criterion.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Criterion.lean
@@ -29,9 +29,8 @@ facade.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Density.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Density.lean
index 6bb11bb125..a489f55176 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Density.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Density.lean
@@ -28,9 +28,8 @@ and the corresponding packaged hypotheses.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/IntegrationByParts.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/IntegrationByParts.lean
index 6624273501..8114b194a2 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/IntegrationByParts.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/IntegrationByParts.lean
@@ -28,9 +28,8 @@ Euler-Lagrange criterion.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Regularity.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Regularity.lean
index 690a720033..719dca2783 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Regularity.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Regularity.lean
@@ -27,9 +27,8 @@ regularity of the local Lagrangian to the packaged smooth-regularity statement.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Support.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Support.lean
index 875632bece..c46431aa76 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Support.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/FirstVariation/Support.lean
@@ -28,9 +28,8 @@ test functions, and continuity of the varied local-jet coordinate map.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5, Theorem 5.2.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5,
+  Theorem 5.2. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPoint.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPoint.lean
index f83a59a518..0b90b81188 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPoint.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPoint.lean
@@ -41,9 +41,8 @@ coordinate.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  arXiv:1612.03100v2, Chapter 5, Section 5.1.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics,
+  arXiv:1612.03100v2, Chapter 5, Section 5.1. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointFiber.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointFiber.lean
index b914d32b56..1fe5e3360f 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointFiber.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointFiber.lean
@@ -34,6 +34,7 @@ At this stage, it introduces:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointRegularity.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointRegularity.lean
index 2b90a4a507..d924d7e105 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointRegularity.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/JetPointRegularity.lean
@@ -34,6 +34,7 @@ At this stage, it provides:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/Lagrangian.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/Lagrangian.lean
index a46335f1e5..6770ace9e2 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/Lagrangian.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/Lagrangian.lean
@@ -38,9 +38,8 @@ structure on local jet-point data has been made explicit enough to support it na
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5.
+  [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDerivative.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDerivative.lean
index 44b8b171e2..2dcdaf3fbf 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDerivative.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDerivative.lean
@@ -31,6 +31,7 @@ formula, without yet introducing a separate coordinate-level derivative calculus
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergence.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergence.lean
index 1931e871b0..063cef37e6 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergence.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergence.lean
@@ -42,9 +42,8 @@ symbolic calculus for coordinate derivatives of total derivatives.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  arXiv:1612.03100v2, Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics,
+  arXiv:1612.03100v2, Chapter 5. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergenceEquivalence.lean b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergenceEquivalence.lean
index 771dbe7298..802bc55205 100644
--- a/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergenceEquivalence.lean
+++ b/PhyslibAlpha/ClassicalFieldTheory/Local/TotalDivergenceEquivalence.lean
@@ -42,9 +42,8 @@ which facts are data and which facts are proved.
 
 ## iv. References
 
-- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*,
-  arXiv:1612.03100v2, Chapter 5.
-
+* J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics,
+  arXiv:1612.03100v2, Chapter 5. [ref: cortes_haupt_2016]
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean b/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean
index 7cfd2cf75e..41c74dd770 100644
--- a/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean
+++ b/PhyslibAlpha/Mathematics/LadderSystem/Basic.lean
@@ -60,6 +60,7 @@ Theorems:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean b/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean
index c863442692..9908d89c90 100644
--- a/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean
+++ b/PhyslibAlpha/Mathematics/LadderSystem/Irreducibility.lean
@@ -31,6 +31,7 @@ characteristic zero.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean b/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean
index ce92e90271..e7eb9d36b3 100644
--- a/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean
+++ b/PhyslibAlpha/Mathematics/LadderSystem/OccupationBasis.lean
@@ -49,6 +49,7 @@ Theorems:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean b/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean
index 752f7e57d6..0407e4b4b1 100644
--- a/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean
+++ b/PhyslibAlpha/Mathematics/LadderSystem/SymmetricPower.lean
@@ -26,6 +26,7 @@ isomorphism sends this basis to the occupation-number states, i.e. it is exactly
 
 ## iii. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean b/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean
index 469c2c4302..73321c6fc7 100644
--- a/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean
+++ b/PhyslibAlpha/Mathematics/LadderSystem/Vacuum.lean
@@ -45,6 +45,7 @@ Theorems:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean
index cd736e10d3..4ff8121f03 100644
--- a/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean
+++ b/PhyslibAlpha/Particles/BeyondTheStandardModel/TwoHDM/Invariants.lean
@@ -20,9 +20,10 @@ public import Mathlib.Analysis.Real.Pi.Irrational
 
 ## i. Overview
 
-In the *bilinear formalism* of the two Higgs doublet model (hep-ph/0605184) the four
-gauge-invariant bilinears — the Gram vector `gramVector` — describe the gauge orbits of the
-configuration space. This file proves the corresponding statement for the potential: every
+In the *bilinear formalism* of the two Higgs doublet model (hep-ph/0605184
+[ref: arxiv_hep_ph_0605184]) the four gauge-invariant bilinears — the Gram vector `gramVector`
+— describe the gauge orbits of the configuration space. This file proves the corresponding
+statement for the potential: every
 gauge-invariant polynomial effective potential is a polynomial in these four gauge-invariant
 bilinears.
 
@@ -61,11 +62,10 @@ and runs the following physical pipeline:
 
 ## iv. References
 
-* The bilinear formalism: https://arxiv.org/abs/hep-ph/0605184.
-
-Mathematically the result is the first fundamental theorem of invariant theory for `SU(2)` acting on
-two doublets in `ℂ²`.
+* The bilinear formalism: https://arxiv.org/abs/hep-ph/0605184. [ref: arxiv_hep_ph_0605184]
 
+Mathematically the result is the first fundamental theorem of invariant theory for `SU(2)`
+acting on two doublets in `ℂ²`.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean
index 769e1b5165..d081d6f546 100644
--- a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -49,6 +49,7 @@ in `d` dimensions.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean
index 4e6c97aa4c..1c0a69a040 100644
--- a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean
+++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderOperators.lean
@@ -54,6 +54,7 @@ Theorems:
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean
index 27dea1c4c5..b3094a4185 100644
--- a/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean
+++ b/PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean
@@ -37,6 +37,7 @@ mode, so it is proved separately.
 
 ## iii. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/QuantumInfo/Capacity/Capacity.lean b/QuantumInfo/Capacity/Capacity.lean
index d35e563d87..1a3298941d 100644
--- a/QuantumInfo/Capacity/Capacity.lean
+++ b/QuantumInfo/Capacity/Capacity.lean
@@ -95,8 +95,7 @@ And other important theorems like superdense coding, nonadditivity, superactivat
 
 ## iv. References
 
- * [Watrous's notes](https://cs.uwaterloo.ca/~watrous/TQI/TQI.8.pdf), Chapter 8 of
-   *The Theory of Quantum Information*.
+* Watrous's notes, Chapter 8 of The Theory of Quantum Information. [ref: watrous_tqi_ch8]
 -/
 
 @[expose] public section
diff --git a/QuantumInfo/Entropy/Axiomatized/Defs.lean b/QuantumInfo/Entropy/Axiomatized/Defs.lean
index 6677c9ef54..d312f8afe9 100644
--- a/QuantumInfo/Entropy/Axiomatized/Defs.lean
+++ b/QuantumInfo/Entropy/Axiomatized/Defs.lean
@@ -35,13 +35,12 @@ function, and then derive much of `Entropy` from it.
 
 ## References:
 
- - [Khinchin’s Fourth Axiom of Entropy Revisited](https://www.mdpi.com/2571-905X/6/3/49)
- - [α-z Relative Entropies](https://warwick.ac.uk/fac/sci/maths/research/events/2013-2014/statmech/su/Nilanjana-slides.pdf)
- - Watrous's notes, [Max-relative entropy and conditional min-entropy](https://cs.uwaterloo.ca/~watrous/QIT-notes/QIT-notes.02.pdf)
- - [Quantum Relative Entropy - An Axiomatic Approach](https://www.marcotom.info/files/entropy-masterclass2022.pdf)
-by Marco Tomamichel
- - [StackExchange](https://quantumcomputing.stackexchange.com/a/12953/10115)
-
+* Khinchin’s Fourth Axiom of Entropy Revisited. [ref: mdpi_khinchin_fourth_axiom]
+* α-z Relative Entropies. [ref: warwick_alpha_z_relative_entropies]
+* Watrous's notes, Max-relative entropy and conditional min-entropy. [ref: watrous_qit_notes_02]
+* Quantum Relative Entropy - An Axiomatic Approach by Marco Tomamichel.
+  [ref: tomamichel_relative_entropy_masterclass]
+* StackExchange. [ref: stackexchange_qc_12953]
 -/
 
 @[expose] public section
diff --git a/QuantumInfo/ForMathlib/LinearEquiv.lean b/QuantumInfo/ForMathlib/LinearEquiv.lean
index 2626a07acf..af8a976c29 100644
--- a/QuantumInfo/ForMathlib/LinearEquiv.lean
+++ b/QuantumInfo/ForMathlib/LinearEquiv.lean
@@ -31,6 +31,7 @@ together with lemmas relating them to `Matrix.reindex`.
 
 ## iv. References
 
+* None.
 -/
 
 @[expose] public section
diff --git a/QuantumInfo/States/Pure/BargmannInvariant.lean b/QuantumInfo/States/Pure/BargmannInvariant.lean
index ed04a8852a..3e8d73375e 100644
--- a/QuantumInfo/States/Pure/BargmannInvariant.lean
+++ b/QuantumInfo/States/Pure/BargmannInvariant.lean
@@ -29,10 +29,11 @@ geodesic triangle in projective Hilbert space.
  * `norm_bargmannInvariantThree_le_one`: `‖Δ₃‖ ≤ 1` (via `Braket.norm_dot_le_one`)
 
 ## References
- * [V. Bargmann, *Note on Wigner's theorem on symmetry operations*,
-   J. Math. Phys. 5, 862–868 (1964)][bargmann1964]
- * [S. Pancharatnam, *Generalized theory of interference, and its
-   applications*, Proc. Indian Acad. Sci. A 44, 247–262 (1956)][pancharatnam1956]
+
+* V. Bargmann, Note on Wigner's theorem on symmetry operations, J. Math. Phys. 5, 862–868 (1964).
+  [ref: bargmann1964]
+* S. Pancharatnam, Generalized theory of interference, and its applications, Proc. Indian Acad.
+  Sci. A 44, 247–262 (1956). [ref: pancharatnam1956]
 -/
 
 open Braket Complex
diff --git a/QuantumInfo/States/Pure/BlochSphere.lean b/QuantumInfo/States/Pure/BlochSphere.lean
index f07ef13312..c4ca228ea2 100644
--- a/QuantumInfo/States/Pure/BlochSphere.lean
+++ b/QuantumInfo/States/Pure/BlochSphere.lean
@@ -28,10 +28,11 @@ then builds the solid angle and dot product API on sphere points.
  * `dot_blochPoint`: dot product of Bloch vectors in terms of angle differences
 
 ## References
- * [S. Pancharatnam, *Generalized theory of interference, and its
-   applications*, Proc. Indian Acad. Sci. A 44, 247–262 (1956)][pancharatnam1956]
- * [M. V. Berry, *Quantal phase factors accompanying adiabatic changes*,
-   Proc. R. Soc. London A 392, 45–57 (1984)][berry1984]
+
+* S. Pancharatnam, Generalized theory of interference, and its applications, Proc. Indian Acad.
+  Sci. A 44, 247–262 (1956). [ref: pancharatnam1956]
+* M. V. Berry, Quantal phase factors accompanying adiabatic changes, Proc. R. Soc. London A 392,
+  45–57 (1984). [ref: berry1984]
 -/
 
 open Complex Matrix
diff --git a/README.md b/README.md
index 6be2849e25..b096cfcfbc 100644
--- a/README.md
+++ b/README.md
@@ -51,6 +51,7 @@ The core library — physics digitalizations reviewed and curated to a high stan
 <td width="33%" valign="top">
 
 ###  [**PhyslibAlpha**](./PhyslibAlpha)
+### [**PhyslibAlpha**](./PhyslibAlpha)
 
 PhyslibAlpha exists for the rapid development of physics digitalizations, enabled by a lighter review process built to handle large-scale, human- or AI-generated contributions.
 
@@ -77,6 +78,7 @@ Quantum information theory. Currently a distinct codebase with its own conventio
 
 🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from **physics**,
   including quantum information, formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
+including quantum information, formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
 
 🎯 The project shall be **organized** by **physics**.
 
@@ -87,6 +89,7 @@ Quantum information theory. Currently a distinct codebase with its own conventio
 🎯 The project shall contain Physics Lean **tactics**, **notation** and **syntax** for physicists.
 
 🎯 The project shall *not* be tied to physics axiomizations (e.g. axiomatic QFT), but rather flexiable enough to accommodate different approaches and starting points.
+🎯 The project shall _not_ be tied to physics axiomizations (e.g. axiomatic QFT), but rather flexiable enough to accommodate different approaches and starting points.
 
 🎯 The content of the project shall be carefully **reviewed** and curated, to ensure reusability, readability and fit.
 
@@ -108,7 +111,8 @@ Because of the lower-review bar for PhyslibAlpha we cannot promise to maintain c
 Physlib is open-source and community run, and we welcome contributions from anyone.
 All you need to do is open a pull-request with your changes
 and our team of maintainers will review it and iterate with you on feedback until it
-can be merged.
+can be merged. Please add references to the `## References` section at the top of the file
+and add them to the .bib file.
 
 If you unsure where you would like to contribute, you may find ideas on:
 - our [open issues](https://github.com/leanprover-community/physlib/issues).
diff --git a/docs/references.bib b/docs/references.bib
index f5063b818a..dee4808c24 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1,124 +1,803 @@
-
 # To normalize:
 # bibtool --preserve.key.case=on --preserve.keys=on --pass.comments=on --print.use.tab=off -s -i docs/references.bib -o docs/references.bib
 
 # When possible, please use the reference obtained from InspireHep.
 
-# To link to an entry in `references.bib`, use the following formats:
-#   [Author, *Title* (optional location)][bibkey]
-@Article{         Allanach:2021yjy,
-  author        = "Allanach, B. C. and Madigan, Maeve and Tooby-Smith,
-                  Joseph",
-  title         = "{A nu supersymmetric anomaly-free atlas}",
-  eprint        = "2107.07926",
-  archiveprefix = "arXiv",
-  primaryclass  = "hep-ph",
-  doi           = "10.1007/JHEP02(2022)144",
-  journal       = "JHEP",
-  volume        = "02",
-  pages         = "144",
-  year          = "2022"
-}
-
-@Article{         Dreiner:2008tw,
-  author        = "Dreiner, Herbi K. and Haber, Howard E. and Martin, Stephen
-                  P.",
-  title         = "{Two-component spinor techniques and Feynman rules for
-                  quantum field theory and supersymmetry}",
-  eprint        = "0812.1594",
-  archiveprefix = "arXiv",
-  primaryclass  = "hep-ph",
-  reportnumber  = "BN-TH-2008-12, SCIPP-08-08, FERMILAB-PUB-09-855-T,
-                  BN-TH-2008-12 and SCIPP-08/08",
-  doi           = "10.1016/j.physrep.2010.05.002",
-  journal       = "Phys. Rept.",
-  volume        = "494",
-  pages         = "1--196",
-  year          = "2010"
-}
-
-@Book{            hall2013quantum,
-  author        = "Hall, Brian C.",
-  title         = "{Quantum Theory for Mathematicians}",
-  publisher     = "Springer",
-  year          = "2013"
-}
-
-@Article{         robertson1929uncertainty,
-  author        = "Robertson, H. P.",
-  title         = "{The Uncertainty Principle}",
-  doi           = "10.1103/PhysRev.34.163",
-  journal       = "Phys. Rev.",
-  volume        = "34",
-  pages         = "163--164",
-  year          = "1929"
-}
-
-@Article{         schrodinger1930heisenberg,
-  author        = "Schr{\"o}dinger, Erwin",
-  title         = "{Zum Heisenbergschen Unscharfeprinzip}",
-  journal       = "Sitzungsberichte der Preussischen Akademie der Wissenschaften,
-                  Physikalisch-mathematische Klasse",
-  pages         = "296--303",
-  year          = "1930"
-}
-
-@Article{         Lohitsiri:2019fuu,
-  author        = "Lohitsiri, Nakarin and Tong, David",
-  title         = "{Hypercharge Quantisation and Fermat's Last Theorem}",
-  eprint        = "1907.00514",
-  archiveprefix = "arXiv",
-  primaryclass  = "hep-th",
-  doi           = "10.21468/SciPostPhys.8.1.009",
-  journal       = "SciPost Phys.",
-  volume        = "8",
-  number        = "1",
-  pages         = "009",
-  year          = "2020"
-}
-
-@Article{         ParticleDataGroup:2018ovx,
-  author        = "Tanabashi, M. and others",
-  collaboration = "Particle Data Group",
-  title         = "{Review of Particle Physics}",
-  doi           = "10.1103/PhysRevD.98.030001",
-  journal       = "Phys. Rev. D",
-  volume        = "98",
-  number        = "3",
-  pages         = "030001",
-  year          = "2018"
-}
-
-@Article{         raynor2021graphical,
-  title         = {Graphical combinatorics and a distributive law for modular
-                  operads},
-  author        = {Raynor, Sophie},
-  journal       = {Advances in Mathematics},
-  volume        = {392},
-  pages         = {108011},
-  year          = {2021},
-  publisher     = {Elsevier}
-}
-
-@Book{        Reed1972,
+# To cite an entry in `references.bib` from a module's docstring, append
+# "[ref: <bibkey>]" to the end of the bullet describing it, e.g.:
+#   * Landau & Lifshitz, Mechanics, 3rd ed., section 25. [ref: landau_mechanics]
+
+# Do not add Zulip links to the .bib file, keep them as plain URLs within the Lean files
+
+
+@article{Allanach:2021yjy,
+  author        = {Allanach, B. C. and Madigan, Maeve and Tooby-Smith, Joseph},
+  title         = {A nu supersymmetric anomaly-free atlas},
+  volume        = {02},
+  eprint        = {2107.07926},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-ph},
+  doi           = {10.1007/JHEP02(2022)144},
+  journal       = {JHEP},
+  pages         = {144},
+  year          = {2022}
+}
+
+@article{Dreiner:2008tw,
+  author        = {Dreiner, Herbi K. and Haber, Howard E. and Martin, Stephen P.},
+  title         = {Two-component spinor techniques and Feynman rules for quantum field theory and supersymmetry},
+  volume        = {494},
+  eprint        = {0812.1594},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-ph},
+  doi           = {10.1016/j.physrep.2010.05.002},
+  journal       = {Phys. Rept.},
+  pages         = {1-196},
+  year          = {2010},
+  note          = {not currently cited by any module; kept for future use}
+}
+
+@article{Lohitsiri:2019fuu,
+  author        = {Lohitsiri, Nakarin and Tong, David},
+  title         = {Hypercharge Quantisation and Fermat's Last Theorem},
+  volume        = {8},
+  number        = {1},
+  eprint        = {1907.00514},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.21468/SciPostPhys.8.1.009},
+  journal       = {SciPost Phys.},
+  pages         = {009},
+  year          = {2020}
+}
+
+@article{ParticleDataGroup:2018ovx,
+  author        = {Tanabashi, M. and others},
+  collaboration = {Particle Data Group},
+  title         = {Review of Particle Physics},
+  volume        = {98},
+  number        = {3},
+  doi           = {10.1103/PhysRevD.98.030001},
+  journal       = {Phys. Rev. D},
+  pages         = {030001},
+  year          = {2018}
+}
+
+@book{Reed1972,
   author    = {Reed, Michael and Simon, Barry},
   title     = {Functional Analysis},
   series    = {Methods of Modern Mathematical Physics},
   volume    = {1},
-  year      = {1972},
+  doi       = {10.1016/B978-0-12-585001-8.X5001-6},
   publisher = {Academic Press},
-  isbn      = {978-0-12-585001-8},
-  doi       = {10.1016/B978-0-12-585001-8.X5001-6}
+  year      = {1972},
+  isbn      = {978-0-12-585001-8}
 }
 
-@Book{        Schmudgen2012,
-  author    = {Konrad Schm{\"u}dgen},
+@book{Schmudgen2012,
+  author    = {Schmudgen, Konrad},
   title     = {Unbounded Self-Adjoint Operators on Hilbert Space},
   series    = {Graduate Texts in Mathematics},
   volume    = {265},
-  year      = {2012},
+  doi       = {10.1007/978-94-007-4753-1},
   publisher = {Springer},
   address   = {Dordrecht},
-  isbn      = {978-94-007-4753-1},
-  doi       = {10.1007/978-94-007-4753-1}
+  year      = {2012},
+  isbn      = {978-94-007-4753-1}
+}
+
+@book{abramowitz_stegun_1964,
+  author    = {Abramowitz, Milton and Stegun, Irene A.},
+  title     = {Handbook of Mathematical Functions},
+  publisher = {National Bureau of Standards},
+  year      = {1964}
+}
+
+@article{alvarez_gaume_ginsparg_1985,
+  author  = {Alvarez-Gaume, L. and Ginsparg, P. H.},
+  title   = {The structure of gauge and gravitational anomalies},
+  doi     = {10.1016/0003-4916(85)90087-9},
+  journal = {Annals of Physics},
+  volume  = {161},
+  number  = {2},
+  pages   = {423-490},
+  year    = {1985}
+}
+
+@book{arnold_mechanics,
+  author    = {Arnold, V. I.},
+  title     = {Mathematical Methods of Classical Mechanics},
+  series    = {Graduate Texts in Mathematics},
+  volume    = {60},
+  edition   = {2nd},
+  publisher = {Springer},
+  year      = {1989}
+}
+
+@book{arnold_ode,
+  author    = {Arnold, V. I.},
+  title     = {Ordinary Differential Equations},
+  publisher = {MIT Press},
+  year      = {1973},
+  note      = {translated from the Russian by Richard A. Silverman; this
+               translation's Chapter 4, "Proofs of the Main Theorems," matches
+               the citing module's chapter title and content (Picard iteration)
+               -- confirmed against the table of contents, which distinguishes
+               it from the differently-organized Springer 1992 translation}
+}
+
+@article{arxiv_0912_0853,
+  author        = {Dudas, Emilian and Palti, Eran},
+  title         = {Froggatt-Nielsen models from E8 in F-theory GUTs},
+  eprint        = {0912.0853},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.1007/JHEP01(2010)127},
+  journal       = {JHEP},
+  volume        = {01},
+  pages         = {127},
+  year          = {2010}
+}
+
+@article{arxiv_1401_5084,
+  author        = {Krippendorf, Sven and Mayorga Pena, Damian Kaloni and Oehlmann,
+                   Paul-Konstantin and Ruehle, Fabian},
+  title         = {Rational F-Theory GUTs without exotics},
+  eprint        = {1401.5084},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.1007/JHEP07(2014)013},
+  journal       = {JHEP},
+  volume        = {07},
+  pages         = {013},
+  year          = {2014}
+}
+
+@article{arxiv_1507_05961,
+  author        = {Krippendorf, Sven and Schafer-Nameki, Sakura and Wong, Jin-Mann},
+  title         = {Froggatt-Nielsen meets Mordell-Weil: A Phenomenological Survey of Global
+                   F-theory GUTs with U(1)s},
+  eprint        = {1507.05961},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  year          = {2015}
+}
+
+@article{arxiv_1605_03237,
+  author        = {Draper, Patrick and Haber, Howard E. and Ruderman, Joshua T.},
+  title         = {Partially Natural Two Higgs Doublet Models},
+  eprint        = {1605.03237},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-ph},
+  doi           = {10.1007/JHEP06(2016)124},
+  journal       = {JHEP},
+  volume        = {06},
+  pages         = {124},
+  year          = {2016}
+}
+
+@article{arxiv_1912_04804,
+  author        = {Allanach, B. C. and Gripaios, Ben and Tooby-Smith, Joseph},
+  title         = {Geometric General Solution to the U(1) Anomaly Equations},
+  eprint        = {1912.04804},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.1007/JHEP05(2020)065},
+  journal       = {JHEP},
+  volume        = {05},
+  pages         = {065},
+  year          = {2020}
+}
+
+@article{arxiv_2006_03588,
+  author        = {Allanach, B. C. and Gripaios, Ben and Tooby-Smith, Joseph},
+  title         = {Anomaly cancellation with an extra gauge boson},
+  eprint        = {2006.03588},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.1103/PhysRevLett.125.161601},
+  journal       = {Phys. Rev. Lett.},
+  volume        = {125},
+  pages         = {161601},
+  year          = {2020}
+}
+
+@article{arxiv_2201_07245,
+  author        = {Davighi, Joe and Tooby-Smith, Joseph},
+  title         = {Electroweak flavour unification},
+  eprint        = {2201.07245},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-ph},
+  doi           = {10.1007/JHEP09(2022)193},
+  journal       = {JHEP},
+  volume        = {09},
+  pages         = {193},
+  year          = {2022}
+}
+
+@article{arxiv_2411_14941,
+  author        = {Erman, F. and Turgut, O. T.},
+  title         = {Completeness of Energy Eigenfunctions for the Reflectionless Potential in
+                   Quantum Mechanics},
+  eprint        = {2411.14941},
+  archiveprefix = {arXiv},
+  primaryclass  = {quant-ph},
+  doi           = {10.1119/5.0228452},
+  journal       = {American Journal of Physics},
+  volume        = {92},
+  pages         = {950-956},
+  year          = {2024}
+}
+
+@article{arxiv_hep_ph_0605184,
+  author        = {Maniatis, M. and von Manteuffel, A. and Nachtmann, O. and Nagel, F.},
+  title         = {Stability and Symmetry Breaking in the General Two-Higgs-Doublet Model},
+  eprint        = {hep-ph/0605184},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-ph},
+  doi           = {10.1140/epjc/s10052-006-0016-6},
+  journal       = {Eur. Phys. J. C},
+  volume        = {48},
+  pages         = {805-823},
+  year          = {2006},
+  note          = {one citing module notes that a step of this paper's argument is not valid}
+}
+
+@article{baez_guts_notes,
+  author        = {Baez, John C. and Huerta, John},
+  title         = {The Algebra of Grand Unified Theories},
+  eprint        = {0904.1556},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  journal       = {Bull. Amer. Math. Soc.},
+  volume        = {47},
+  pages         = {483-552},
+  year          = {2010},
+  url           = {https://math.ucr.edu/home/baez/guts.pdf}
+}
+
+@book{barenblatt_1996_scaling,
+  author    = {Barenblatt, G. I.},
+  title     = {Scaling, Self-similarity, and Intermediate Asymptotics},
+  publisher = {Cambridge University Press},
+  year      = {1996}
+}
+
+@article{bargmann1964,
+  author  = {Bargmann, V.},
+  title   = {Note on Wigner's theorem on symmetry operations},
+  doi     = {10.1063/1.1704188},
+  volume  = {5},
+  journal = {J. Math. Phys.},
+  pages   = {862-868},
+  year    = {1964}
+}
+
+@article{berry1984,
+  author  = {Berry, M. V.},
+  title   = {Quantal phase factors accompanying adiabatic changes},
+  doi     = {10.1098/rspa.1984.0023},
+  volume  = {392},
+  number  = {1802},
+  journal = {Proc. R. Soc. London A},
+  pages   = {45-57},
+  year    = {1984}
+}
+
+@article{bilal_2008_anomalies,
+  author        = {Bilal, A.},
+  title         = {Lectures on Anomalies},
+  eprint        = {0802.0634},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  year          = {2008}
+}
+
+@misc{bipm_si_brochure_2019,
+  title        = {International Bureau of Weights and Measures (BIPM), The International System of Units (SI Brochure)},
+  edition      = {9th},
+  year         = {2019},
+  howpublished = {},
+  url          = {https://www.bipm.org/documents/d/guest/si-brochure-9-en-pdf}
+}
+
+@article{caldirola_1941,
+  author  = {Caldirola, P.},
+  title   = {Forze non conservative nella meccanica quantistica},
+  volume  = {18},
+  journal = {Nuovo Cimento},
+  pages   = {393-400},
+  year    = {1941},
+  note    = {title translates to "Non-conservative forces in quantum mechanics"}
+}
+
+@misc{cobos_2015_lorentz_group,
+  author       = {Cobos, Guillem},
+  title        = {The Lorentz Group},
+  year         = {2015},
+  howpublished = {},
+  url          = {https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf}
+}
+
+@article{cortes_haupt_2016,
+  author        = {Cortes, Vicente and Haupt, Alexander S.},
+  title         = {Lecture Notes on Mathematical Methods of Classical Physics},
+  eprint        = {1612.03100},
+  archiveprefix = {arXiv},
+  year          = {2016}
+}
+
+@article{doi_1063_1_3290740,
+  author  = {Hall, Richard L. and Saad, Nasser and Sen, K. D.},
+  title   = {Soft-core Coulomb potentials and Heun's differential equation},
+  doi     = {10.1063/1.3290740},
+  journal = {J. Math. Phys.},
+  volume  = {51},
+  pages   = {022107},
+  year    = {2010}
+}
+
+@article{doi_physreva_80_032507,
+  author  = {Hall, Richard L. and Saad, Nasser and Sen, K. D. and Ciftci, Hakan},
+  title   = {Energies and wave functions for a soft-core Coulomb potential},
+  doi     = {10.1103/PhysRevA.80.032507},
+  journal = {Phys. Rev. A},
+  volume  = {80},
+  pages   = {032507},
+  year    = {2009}
+}
+
+@misc{github_leandojo_extractdata,
+  howpublished = {},
+  url          = {https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean}
+}
+
+@misc{github_tryateachstep,
+  howpublished = {},
+  url          = {https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean}
+}
+
+@book{goldstein_classicalmechanics,
+  author    = {Goldstein, Herbert and Poole, Charles P. and Safko, John L.},
+  title     = {Classical Mechanics},
+  edition   = {3rd},
+  publisher = {Addison-Wesley},
+  year      = {2002}
+}
+
+@book{hall2013quantum,
+  author    = {Hall, Brian C.},
+  title     = {Quantum Theory for Mathematicians},
+  publisher = {Springer},
+  year      = {2013}
+}
+
+@book{huygens_1673,
+  author = {Huygens, Christiaan},
+  title  = {Horologium Oscillatorium},
+  year   = {1673}
+}
+
+@misc{iau_2012_resolution_b2,
+  title        = {IAU 2012 Resolution B2 (the astronomical unit)},
+  howpublished = {},
+  url          = {https://iauarchive.eso.org/static/resolutions/IAU2012_English.pdf}
+}
+
+@misc{iau_2015_resolution_b2,
+  title        = {IAU 2015 Resolution B2 (the exact parsec convention)},
+  howpublished = {},
+  url          = {https://iauarchive.eso.org/static/resolutions/IAU2015_English.pdf}
+}
+
+@misc{iau_style_manual_units,
+  author       = {Wilkins, G. A.},
+  title        = {Recommendations concerning Units (SI Units)},
+  howpublished = {},
+  url          = {https://iauarchive.eso.org/publications/proceedings_rules/units/},
+  note         = {reprinted from the IAU Style Manual (1989); the Julian year
+                  convention used in the light-year is cited in the citing module}
+}
+
+@book{ioffe_1957,
+  author    = {Ioffe, A. F.},
+  title     = {Semiconductor Thermoelements and Thermoelectric Cooling},
+  publisher = {Infosearch},
+  year      = {1957}
+}
+
+@misc{iso_80000_1_2009,
+  title = {ISO/IEC 80000-1:2009, Quantities and units - Part 1: General}
+}
+
+@misc{jaffe_lorentz_notes,
+  author       = {Jaffe, Arthur},
+  title        = {Lorentz Transformations, Rotations, and Boosts},
+  howpublished = {},
+  url          = {https://cdn.ku.edu.tr/cdn/files/amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf},
+  note         = {course handout by Arthur Jaffe (Harvard); mirrored as course
+                  material at Koc University, which is the copy cited}
+}
+
+@misc{jcgm_200_2012,
+  title = {JCGM 200:2012, International vocabulary of metrology - Basic and general concepts and associated terms (VIM, 3rd edition)}
+}
+
+@article{kanai_1948,
+  author  = {Kanai, E.},
+  title   = {On the Quantization of the Dissipative Systems},
+  doi     = {10.1143/ptp/3.4.440},
+  volume  = {3},
+  number  = {4},
+  journal = {Progress of Theoretical Physics},
+  pages   = {440-442},
+  year    = {1948}
+}
+
+@article{koor_et_al_2023_wirtinger,
+  author        = {Koor, B. and Qiu, Y. and Kwek, L. and Rebentrost, P.},
+  title         = {A short tutorial on Wirtinger Calculus with applications in quantum information},
+  eprint        = {2312.04858},
+  archiveprefix = {arXiv}
+}
+
+@article{kreutz_delgado_cr_calculus,
+  author        = {Kreutz-Delgado, K.},
+  title         = {The Complex Gradient Operator and the CR-Calculus},
+  eprint        = {0906.4835},
+  archiveprefix = {arXiv}
+}
+
+@book{landau_fluidmechanics,
+  author    = {Landau, L. D. and Lifshitz, E. M.},
+  title     = {Fluid Mechanics},
+  series    = {Course of Theoretical Physics},
+  volume    = {6},
+  edition   = {2nd},
+  publisher = {Pergamon Press},
+  year      = {1987}
+}
+
+@book{landau_mechanics,
+  author    = {Landau, L. D. and Lifshitz, E. M.},
+  title     = {Mechanics},
+  series    = {Course of Theoretical Physics},
+  volume    = {1},
+  edition   = {3rd},
+  publisher = {Butterworth-Heinemann},
+  year      = {1976}
+}
+
+@book{landau_statphys1,
+  author    = {Landau, L. D. and Lifshitz, E. M.},
+  title     = {Statistical Physics, Part 1},
+  series    = {Course of Theoretical Physics},
+  volume    = {5},
+  edition   = {3rd},
+  publisher = {Butterworth-Heinemann},
+  year      = {1980}
+}
+
+@article{lawrie_schafer_nameki_wong_2015,
+  author        = {Lawrie, Craig and Schafer-Nameki, Sakura and Wong, Jin-Mann},
+  title         = {F-theory and All Things Rational: Surveying U(1) Symmetries with Rational Sections},
+  eprint        = {1504.05593},
+  archiveprefix = {arXiv},
+  primaryclass  = {hep-th},
+  doi           = {10.1007/JHEP09(2015)144},
+  journal       = {JHEP},
+  volume        = {09},
+  pages         = {144},
+  year          = {2015},
+  note          = {page 6 is cited in the citing module}
+}
+
+@article{mdpi_khinchin_fourth_axiom,
+  author  = {Zhang, Zhiyi and Huang, Hongwei and Xu, Hao},
+  title   = {Khinchin's Fourth Axiom of Entropy Revisited},
+  doi     = {10.3390/stats6030049},
+  journal = {Stats},
+  volume  = {6},
+  number  = {3},
+  pages   = {763-772},
+  year    = {2023}
+}
+
+@article{mortini_rupp_2022,
+  author  = {Mortini, R. and Rupp, R.},
+  title   = {The Clairaut-Schwarz Theorem for Mixed Wirtinger Derivatives},
+  doi     = {10.1007/s41980-021-00660-1},
+  volume  = {48},
+  number  = {5},
+  journal = {Bull. Iranian Math. Soc.},
+  pages   = {2643-2647},
+  year    = {2022}
+}
+
+@techreport{nasa_ntrs_20140002333,
+  author       = {Simpson, James C. and Lane, John E. and Immer, Christopher D. and
+                  Youngquist, Robert C.},
+  title        = {Simple Analytic Expressions for the Magnetic Field of a Circular
+                  Current Loop},
+  institution  = {NASA Kennedy Space Center},
+  number       = {NASA/TM-2013-217919},
+  year         = {2001},
+  howpublished = {},
+  url          = {https://ntrs.nasa.gov/api/citations/20140002333/downloads/20140002333.pdf}
+}
+
+@book{nash_1991_dtqft,
+  author    = {Nash, C.},
+  title     = {Differential topology and quantum field theory},
+  publisher = {Elsevier},
+  year      = {1991}
+}
+
+@book{nielsen_chuang_qci,
+  author    = {Nielsen, M. A. and Chuang, I. L.},
+  title     = {Quantum Computation and Quantum Information},
+  edition   = {10th Anniversary},
+  publisher = {Cambridge University Press},
+  year      = {2010}
+}
+
+@misc{nist_dlmf,
+  title        = {NIST Digital Library of Mathematical Functions},
+  howpublished = {},
+  url          = {https://dlmf.nist.gov/},
+  note         = {section 19.7(ii) is cited in the citing module}
+}
+
+@misc{nist_hb44_2023,
+  title = {NIST Handbook 44, Appendix C (international foot-based units and the international nautical mile)},
+  doi   = {10.6028/NIST.HB.44-2023}
+}
+
+@article{nominal_solar_mass_article,
+  author  = {Prsa, Andrej and others},
+  title   = {Nominal values for selected solar and planetary quantities: IAU 2015
+             Resolution B3},
+  doi     = {10.3847/0004-6256/152/2/41},
+  journal = {Astron. J.},
+  volume  = {152},
+  number  = {2},
+  pages   = {41},
+  year    = {2016}
+}
+
+@book{oneill_1983_semi_riemannian,
+  author    = {O'Neill, Barrett},
+  title     = {Semi-Riemannian Geometry With Applications to Relativity},
+  publisher = {Academic Press},
+  year      = {1983}
+}
+
+@article{pancharatnam1956,
+  author  = {Pancharatnam, S.},
+  title   = {Generalized theory of interference, and its applications},
+  doi     = {10.1007/bf03046050},
+  volume  = {44},
+  number  = {5},
+  journal = {Proc. Indian Acad. Sci. A},
+  pages   = {247-262},
+  year    = {1956}
+}
+
+@book{peskin_schroeder_qft,
+  author    = {Peskin, Michael E. and Schroeder, Daniel V.},
+  title     = {An Introduction to Quantum Field Theory},
+  publisher = {Westview Press},
+  year      = {1995}
+}
+
+@misc{qmul_emt10_notes,
+  title        = {MSci 4261 Electromagnetism: Lecture Notes X.10.1, The Energy-Momentum Tensor},
+  howpublished = {},
+  url          = {https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf},
+  note         = {Queen Mary University of London course notes}
+}
+
+@article{raynor2021graphical,
+  author    = {Raynor, Sophie},
+  title     = {Graphical combinatorics and a distributive law for modular operads},
+  volume    = {392},
+  journal   = {Advances in Mathematics},
+  pages     = {108011},
+  publisher = {Elsevier},
+  year      = {2021},
+  note      = {not currently cited by any module; kept for future use}
+}
+
+@article{robertson1929uncertainty,
+  author  = {Robertson, H. P.},
+  title   = {The Uncertainty Principle},
+  volume  = {34},
+  doi     = {10.1103/PhysRev.34.163},
+  journal = {Phys. Rev.},
+  pages   = {163-164},
+  year    = {1929}
+}
+
+@article{schrodinger1930heisenberg,
+  author  = {Schrodinger, Erwin},
+  title   = {Zum Heisenbergschen Unscharfeprinzip},
+  journal = {Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse},
+  pages   = {296-303},
+  year    = {1930}
+}
+
+@article{snyder_toberer_2008,
+  author  = {Snyder, G. J. and Toberer, E. S.},
+  title   = {Complex thermoelectric materials},
+  volume  = {7},
+  journal = {Nature Materials},
+  pages   = {105-114},
+  year    = {2008}
+}
+
+@misc{stackexchange_qc_12953,
+  title        = {Quantum Computing Stack Exchange answer 12953},
+  howpublished = {},
+  url          = {https://quantumcomputing.stackexchange.com/a/12953/10115}
+}
+
+@article{stone_1930,
+  author  = {Stone, M. H.},
+  title   = {Linear Transformations in Hilbert Space III. Operational Methods and Group Theory},
+  doi     = {10.1073/pnas.16.2.172},
+  volume  = {16},
+  journal = {Proc. Natl. Acad. Sci.},
+  pages   = {172-175},
+  year    = {1930},
+  note    = {the citing module originally gave "18 (1932)"; corrected against
+             the DOI record to volume 16, 1930}
+}
+
+@book{sussman_wisdom_sicm,
+  author    = {Sussman, Gerald Jay and Wisdom, Jack},
+  title     = {Structure and Interpretation of Classical Mechanics},
+  edition   = {1st},
+  publisher = {MIT Press},
+  year      = {2001},
+  url       = {https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/book-Z-H-36.html#%_sec_3.1.2},
+  note      = {edition inferred from the free online HTML edition cited (matches the 1st ed.)}
+}
+
+@misc{terek_variational_manifolds,
+  author       = {Terek, Ivo},
+  title        = {Introductory Variational Calculus on Manifolds},
+  howpublished = {},
+  url          = {https://web.williams.edu/Mathematics/it3/texts/var_noether.pdf},
+  note         = {lecture notes; no publication year given in the document}
+}
+
+@misc{tomamichel_relative_entropy_masterclass,
+  title        = {Tomamichel, Quantum Relative Entropy - An Axiomatic Approach},
+  howpublished = {},
+  url          = {https://www.marcotom.info/files/entropy-masterclass2022.pdf}
+}
+
+@article{tong_line_operators_sm,
+  author        = {Tong, D.},
+  title         = {Line Operators in the Standard Model},
+  volume        = {07},
+  eprint        = {1705.01853},
+  archiveprefix = {arXiv},
+  journal       = {JHEP},
+  pages         = {104},
+  year          = {2017}
+}
+
+@misc{tong_statistical_physics,
+  author       = {Tong, David},
+  title        = {Lectures on Statistical Physics},
+  howpublished = {},
+  url          = {https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf}
+}
+
+@misc{tong_statphys_notes_one,
+  author       = {Tong, David},
+  title        = {Cambridge Lecture Notes on Statistical Physics, part one},
+  howpublished = {},
+  url          = {https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf}
+}
+
+@misc{tong_statphys_notes_two,
+  author       = {Tong, David},
+  title        = {Cambridge Lecture Notes on Statistical Physics, part two},
+  howpublished = {},
+  url          = {https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf}
+}
+
+@article{tooby_smith_2024_index_notation,
+  author        = {Tooby-Smith, Joseph},
+  title         = {Formalization of physics index notation in Lean 4},
+  eprint        = {2411.07667},
+  archiveprefix = {arXiv},
+  primaryclass  = {cs.LO},
+  year          = {2024}
+}
+
+@misc{ucdavis_spinorfeynrules,
+  author       = {Terning, John},
+  title        = {Modern Supersymmetry: Slides -- Spinor Feynman Rules},
+  howpublished = {},
+  url          = {https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf},
+  note         = {companion teaching material to Terning, Modern Supersymmetry:
+                  Dynamics and Duality, Oxford University Press (2006); a
+                  different spinor index convention is used there than in Physlib}
+}
+
+@misc{ucsd_ph130a_node452,
+  author       = {Branson, James},
+  title        = {Quantum Physics (UCSD Physics 130) -- Course Notes},
+  howpublished = {},
+  url          = {https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html}
+}
+
+@misc{warwick_alpha_z_relative_entropies,
+  title        = {alpha-z Relative Entropies},
+  howpublished = {},
+  url          = {https://warwick.ac.uk/fac/sci/maths/research/events/2013-2014/statmech/su/Nilanjana-slides.pdf}
+}
+
+@misc{watrous_qit_notes_02,
+  title        = {Watrous, Max-relative entropy and conditional min-entropy},
+  howpublished = {},
+  url          = {https://cs.uwaterloo.ca/~watrous/QIT-notes/QIT-notes.02.pdf},
+  note         = {lecture notes}
+}
+
+@book{watrous_tqi_ch8,
+  author    = {Watrous, John},
+  title     = {The Theory of Quantum Information},
+  publisher = {Cambridge University Press},
+  year      = {2018},
+  isbn      = {978-1-107-18056-7},
+  url       = {https://cs.uwaterloo.ca/~watrous/TQI/TQI.8.pdf},
+  note      = {Chapter 8 is cited in the citing module; url is the author's own
+               freely available copy of that chapter}
+}
+
+@book{weinberg_qft1,
+  author    = {Weinberg, Steven},
+  title     = {The Quantum Theory of Fields, Volume 1: Foundations},
+  publisher = {Cambridge University Press},
+  year      = {1995}
+}
+
+@misc{wiki_classical_em_and_sr,
+  title        = {Classical electromagnetism and special relativity},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Classical_electromagnetism_and_special_relativity}
+}
+
+@misc{wiki_complex_differential_form,
+  title        = {Complex differential form (Dolbeault operators)},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Complex_differential_form}
+}
+
+@misc{wiki_em_field_gauge_freedom,
+  title        = {Mathematical descriptions of the electromagnetic field (gauge freedom)},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Mathematical_descriptions_of_the_electromagnetic_field#Gauge_freedom}
+}
+
+@misc{wiki_levi_civita_symbol,
+  title        = {Levi-Civita symbol},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Levi-Civita_symbol}
+}
+
+@misc{wiki_lorentz_transformation,
+  title        = {Lorentz transformation},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Lorentz_transformation}
+}
+
+@misc{wiki_rigged_hilbert_space,
+  title        = {Rigged Hilbert space},
+  howpublished = {},
+  url          = {https://en.wikipedia.org/wiki/Rigged_Hilbert_space}
 }
diff --git a/scripts/MetaPrograms/check_rfl.lean b/scripts/MetaPrograms/check_rfl.lean
index 1a51f18aa6..ab7f0285bd 100644
--- a/scripts/MetaPrograms/check_rfl.lean
+++ b/scripts/MetaPrograms/check_rfl.lean
@@ -13,15 +13,15 @@ import Physlib.Meta.TransverseTactics
 This file produces a list of places where `rfl` will complete the goal.
 
 ## References
-The content of this file is based on the following sources (released under the Apache 2.0 license).
 
-- https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
-- https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
+The content of this file is based on the following sources (released under the Apache 2.0
+license), with modifications made to the original content here.
 
-Modifications have been made to the original content of these files here.
-
-See also:
-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
+* https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean.
+  [ref: github_tryateachstep]
+* https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean.
+  [ref: github_leandojo_extractdata]
+* See also: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E.
 -/
 open Lean Elab System
 
diff --git a/scripts/MetaPrograms/free_simps.lean b/scripts/MetaPrograms/free_simps.lean
index 7f61d54669..8edbe1623f 100644
--- a/scripts/MetaPrograms/free_simps.lean
+++ b/scripts/MetaPrograms/free_simps.lean
@@ -12,16 +12,15 @@ import Physlib.Meta.TransverseTactics
 
 This file checks for non-terminating `simp` tactics which do not appear as `simp only`.
 ## References
-The content of this file is based on the following sources (released under the Apache 2.0 license).
 
-- https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
-- https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
-
-Modifications have been made to the original content of these files here.
-
-See also:
-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E
+The content of this file is based on the following sources (released under the Apache 2.0
+license), with modifications made to the original content here.
 
+* https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean.
+  [ref: github_tryateachstep]
+* https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean.
+  [ref: github_leandojo_extractdata]
+* See also: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Memory.20increase.20in.20loops.2E.
 -/
 open Lean Elab System
 
diff --git a/scripts/check_references.py b/scripts/check_references.py
new file mode 100755
index 0000000000..4547e7e6b8
--- /dev/null
+++ b/scripts/check_references.py
@@ -0,0 +1,90 @@
+#!/usr/bin/env python3
+"""Validates the '## References' sections of Physlib/QuantumInfo/PhyslibAlpha modules.
+
+Checks, for every module docstring References section:
+  * the body is not empty
+  * every "[ref: <key>]" tag resolves to an entry in docs/references.bib
+  * docs/references.bib contains no Zulip entries (Zulip links clutter the
+    bibliography and aren't useful indexed as formal references -- they should
+    be left as plain, untagged URLs in the docstring instead)
+
+Usage: ./scripts/check_references.py
+Exits non-zero (and prints one message per problem) if any check fails.
+"""
+import pathlib
+import re
+import sys
+
+ROOT = pathlib.Path(__file__).resolve().parent.parent
+HEAD_RE = re.compile(r'^#{1,4}\s*(?:(?:i{1,3}v?|\d+)\.\s*)?References?:?\s*$')
+REF_TAG_RE = re.compile(r'\[ref:\s*([^\]]+?)\]')
+BIB_ENTRY_RE = re.compile(r'^@(\w+)\{\s*([^,\s]+)\s*,(.*?)^\}', re.MULTILINE | re.DOTALL)
+
+
+def load_registry():
+    text = (ROOT / 'docs' / 'references.bib').read_text(encoding='utf-8')
+    entries = {}
+    for m in BIB_ENTRY_RE.finditer(text):
+        entries[m.group(2)] = m.group(3)
+    return entries
+
+
+def find_blocks(lines):
+    blocks = []
+    i = 0
+    while i < len(lines):
+        if HEAD_RE.match(lines[i].strip()):
+            j = i + 1
+            while j < len(lines):
+                s = lines[j].strip()
+                if s.startswith('#') and 'References' not in s:
+                    break
+                if s == '-/' or s.startswith('-/'):
+                    break
+                j += 1
+            blocks.append((i, j))
+            i = j
+        else:
+            i += 1
+    return blocks
+
+
+def main():
+    registry = load_registry()
+    keys = set(registry)
+    problems = []
+
+    for key, fields in registry.items():
+        if 'zulip' in key.lower() or 'zulipchat.com' in fields:
+            problems.append(f"docs/references.bib: entry '{key}' is a Zulip link "
+                             f"-- Zulip links should not be added to the bibliography")
+
+    for path in sorted(ROOT.rglob('*.lean')):
+        if '.lake' in path.parts:
+            continue
+        lines = path.read_text(encoding='utf-8', errors='replace').split('\n')
+        for head_idx, end_idx in find_blocks(lines):
+            body_lines = lines[head_idx + 1:end_idx]
+            body = '\n'.join(body_lines).strip()
+            rel = path.relative_to(ROOT)
+            if not body:
+                problems.append(f"{rel}:{head_idx + 1}: empty References section "
+                                 f"(use '* None.' if there is genuinely no reference)")
+                continue
+            for line_no, line in enumerate(body_lines, start=head_idx + 2):
+                for m in REF_TAG_RE.finditer(line):
+                    key = m.group(1).strip()
+                    if key not in keys:
+                        problems.append(f"{rel}:{line_no}: unknown reference key "
+                                         f"'{key}' (not in docs/references.bib)")
+
+    if problems:
+        for p in problems:
+            print(p)
+        print(f"\n{len(problems)} problem(s) found")
+        sys.exit(1)
+    print("References sections OK")
+
+
+if __name__ == '__main__':
+    main()