From b7dcd50785e921c385bffffdd3d2f6645566e78b Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Thu, 30 Apr 2026 20:07:29 +0100 Subject: [PATCH] docs: Add TODO items --- Physlib.lean | 1 + .../ConfigurationSpace.lean | 5 ++-- .../HarmonicOscillator/Solution.lean | 2 +- .../Current/CircularCoil.lean | 4 +-- Physlib/Mathematics/LinearMaps.lean | 3 +- Physlib/Meta/TODO/Global.lean | 30 +++++++++++++++++++ Physlib/Relativity/Tensors/Basic.lean | 7 +++++ .../Tensors/RealTensor/CoVector/Basic.lean | 7 +++++ .../Tensors/RealTensor/Vector/Basic.lean | 7 +++++ Physlib/SpaceAndTime/Space/Basic.lean | 9 +++--- Physlib/SpaceAndTime/Space/Module.lean | 2 -- 11 files changed, 64 insertions(+), 13 deletions(-) create mode 100644 Physlib/Meta/TODO/Global.lean diff --git a/Physlib.lean b/Physlib.lean index bcb7d0759..19fd8fe2b 100644 --- a/Physlib.lean +++ b/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 diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean index 8f5625215..fcd64f8f2 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean +++ b/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 diff --git a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean b/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean index 6cd744552..a8b9b9a9f 100644 --- a/Physlib/ClassicalMechanics/HarmonicOscillator/Solution.lean +++ b/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." diff --git a/Physlib/Electromagnetism/Current/CircularCoil.lean b/Physlib/Electromagnetism/Current/CircularCoil.lean index 4cb5eb890..a1095e8ee 100644 --- a/Physlib/Electromagnetism/Current/CircularCoil.lean +++ b/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 diff --git a/Physlib/Mathematics/LinearMaps.lean b/Physlib/Mathematics/LinearMaps.lean index 9d728b846..c42349996 100644 --- a/Physlib/Mathematics/LinearMaps.lean +++ b/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] diff --git a/Physlib/Meta/TODO/Global.lean b/Physlib/Meta/TODO/Global.lean new file mode 100644 index 000000000..357fcb740 --- /dev/null +++ b/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." diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean index 19b26c738..921b1d119 100644 --- a/Physlib/Relativity/Tensors/Basic.lean +++ b/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 diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean index fcd147acb..6949eabd4 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean +++ b/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 diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean index e4da1a348..ca4d05f30 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean +++ b/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 diff --git a/Physlib/SpaceAndTime/Space/Basic.lean b/Physlib/SpaceAndTime/Space/Basic.lean index 16d9d7715..fd156e472 100644 --- a/Physlib/SpaceAndTime/Space/Basic.lean +++ b/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 diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 4507ed74b..20380ef4c 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/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`