docs: Add TODO items

Physlib.lean

@@ -94,6 +94,7 @@ public import Physlib.Meta.Remark.Basic
 public import Physlib.Meta.Remark.Properties
 public import Physlib.Meta.Sorry
 public import Physlib.Meta.TODO.Basic
+public import Physlib.Meta.TODO.Global
 public import Physlib.Meta.TransverseTactics
 public import Physlib.Optics.Basic
 public import Physlib.Optics.Polarization.Basic

Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean

@@ -23,8 +23,9 @@ namespace HarmonicOscillator
 TODO "Configuration Space should be refactored to take `EuclideanSpace ℝ (Fin 1)`
     as its value."
 
-TODO "The API around this should be improved to allow further development of a proper
-    geometric model of the Harmonic Oscillator (see TODO item 4DK2M)."
+TODO "The API around the configuration space
+    should be improved to allow further development of a proper
+    geometric model of the Harmonic Oscillator."
 
 /-- The configuration space of the harmonic oscillator. -/
 structure ConfigurationSpace where

Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -209,7 +209,7 @@ The correctness proofs showing that the conversion produces the expected traject
 are given later in section D.1, after the trajectory machinery has been defined.
 -/
 
-TODO "Implement other initial conditions (deferred to future PRs). For example:
+TODO "Implement other initial conditions for the classical harmonic oscillator. For example:
 - Two positions at different times.
 - Two velocities at different times.
 And convert them into the type `InitialConditions` above."

Physlib/Electromagnetism/Current/CircularCoil.lean

@@ -29,8 +29,8 @@ electromagnetic potentials and fields around a circular coil.
 
 @[expose] public section
 
-TODO "Copying the structure of the electrostatics of an infinite wire,
-  complete the definitions and proofs for a circular coil carrying a steady current."
+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."
 
 namespace Electromagnetism
 namespace DistElectromagneticPotential

Physlib/Mathematics/LinearMaps.lean

@@ -18,7 +18,8 @@ quadratic and cubic equations.
 -/
 
 @[expose] public section
-TODO "Replace the definitions in this file with Mathlib definitions."
+TODO "Replace the definitions of bi-linear maps in `./Mathematics/LinaerMaps`
+ with definitions from Mathlib."
 
 /-- The structure defining a homogeneous quadratic equation. -/
 @[simp]

Physlib/Meta/TODO/Global.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+module
+
+public import Physlib.Meta.TODO.Basic
+/-!
+
+# Global TODO items
+
+This module contains global TODO items, which are not specific to any particular module,
+but are still important for the development of Physlib.
+
+-/
+
+@[expose] public section
+
+
+/-!
+
+## Style
+
+-/
+
+TODO "Ensure that all the lines in QuantumInfo are below 100 characters long."
+
+TODO "Remove all instances of `erw` within Physlib. This usually
+  indicates the need for better API."

Physlib/Relativity/Tensors/Basic.lean

@@ -15,6 +15,13 @@ public import Physlib.Meta.TODO.Basic
 
 -/
 
+TODO "In this file (Physlib/Relativity/Tensors/Basic.lean), write an overview of the
+  implementation of tensors in Physlib. It should cover the main points:
+- the definition of a tensor species,
+- the meaning of color,
+- the tensorial instances,
+- other key definitions."
+
 @[expose] public section
 
 open Module IndexNotation CategoryTheory MonoidalCategory

Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean

@@ -19,6 +19,13 @@ We create an API around Lorentz vectors to make working with them as easy as pos
 
 @[expose] public section
 
+TODO "Split this module on Lorentz co-vectors into two: `Basic.lean` and `Tensorial.lean`.
+  The former should contain the basic definitions and vector space structure of
+  Lorentz co-vectors (e.g. the basis etc.). This should only depend on imports from Mathlib.
+  The latter should contain the tensorial instance and everything which should
+  depend on the `Tensorial` imports. A similar TODO item exists
+  for Lorentz vectors."
+
 open Module IndexNotation
 open CategoryTheory
 open MonoidalCategory

Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean

@@ -19,6 +19,13 @@ We create an API around Lorentz vectors to make working with them as easy as pos
 
 @[expose] public section
 
+TODO "Refactor: Split this module on Lorentz vectors into two: `Basic.lean` and `Tensorial.lean`.
+  The former should contain the basic definitions and vector space structure of
+  Lorentz vectors (e.g. the basis etc.). This should only depend on imports from Mathlib.
+  The latter should contain the tensorial instance and everything which should
+  depend on the `Tensorial` imports. A similar TODO item exists
+  for Lorentz co-vectors."
+
 open Module IndexNotation
 open CategoryTheory
 open MonoidalCategory

Physlib/SpaceAndTime/Space/Basic.lean

@@ -76,11 +76,6 @@ the `VAdd (EuclideanSpace ℝ (Fin d)) (Space d)` instance instead.
 
 -/
 
-TODO "In the above documentation describe the notion of a type, and
-  introduce the type `Space d`."
-
-TODO "Convert `Space` from an `abbrev` to a `def`."
-
 /-- The type `Space d` is the world-volume which corresponds to
 `d` dimensional (flat) Euclidean space with a given (but arbitrary)
 choice of length unit, and a given (but arbitrary) choice of zero.
@@ -258,6 +253,10 @@ instance {d : ℕ} : Nontrivial (Space d.succ) where
 
 -/
 
+TODO "Fix the manifold structure on `Space d`. In particular, we should not need to
+  define `manifoldStructure`. Instead, we should be able to give `Space d` an instance
+  of `IsManifold` directly."
+
 /-- The manifold structure on `Space d`. -/
 noncomputable def manifoldStructure (d : ℕ) :
     ModelWithCorners ℝ (EuclideanSpace ℝ (Fin d)) (Space d) where

Physlib/SpaceAndTime/Space/Module.lean

@@ -293,8 +293,6 @@ instance {d : ℕ} : BorelSpace (Space d) where
 TODO "In the above documentation describe what an instance is, and why
   it is useful to have instances for `Space d`."
 
-TODO "After TODO 'HB6VC', give `Space d` the necessary instances
-  using `inferInstanceAs`."
 /-!
 
 ## The norm on `Space`