From 34df54b967c32f59c90ff472044659aa6787f9b6 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 24 Feb 2026 10:54:39 +0000 Subject: [PATCH 1/9] feat: Improve docs on space --- PhysLean/SpaceAndTime/Space/Basic.lean | 39 ++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index 097d66181..48e70f45d 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -20,8 +20,40 @@ to a `d`-dimensional Euclidean space and prove some properties about it. PhysLean sits downstream of Mathlib, and above we import the necessary Mathlib modules which contain (perhaps transitively through imports) the definitions and theorems we need. +## Implementation details + +The exact implementation of `Space d` into PhysLean is discussed in numerous places +on the Lean Zulip, including: + +- https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575332888 + +There is a choice between defining `Space d` as an `abbrev` of `EuclideanSpace ℝ (Fin d)`, +as a `def` of a type with value `EuclideanSpace ℝ (Fin d)` or as a structure +with a field `val : Fin d → ℝ`. + ++---------------------------------------------------+---------+-------+-----------+ +| | abbrev | def | structure | ++---------------------------------------------------+---------+-------+-----------+ +| allows casting from `EuclideanSpace` | yes | yes | no | +| carries instances from `EuclideanSpace` | yes | no | no | +| requires reproving of lemmas from `EuclideanSpace`| no | no | yes | ++---------------------------------------------------+---------+-------+-----------+ + +The `structure` is the most conservative choice, as everything needs redefining, however, +there is are two benefits of this: + +1. It allows us to be precise about the instances we define on `Space d`, and makes + future refactoring of those instances easier. +2. It allows us to give the necessary physics context to results about `Space d`, which + would not otherwise be possible if we reuse results from Mathlib. + +Currently `Space d` has the structure of a `Module` (which requires the choice +of a zero), a future refactor should give `Space d` the structure of an `AddTorsor` +(an affine space) which does not require the choice of a zero. + -/ + /-! ## The `Space` type @@ -33,8 +65,11 @@ TODO "HB6RR" "In the above documentation describe the notion of a type, and TODO "HB6VC" "Convert `Space` from an `abbrev` to a `def`." -/-- The type `Space d` represents `d` dimensional Euclidean space. - The default value of `d` is `3`. Thus `Space = Space 3`. -/ +/-- The type `Space d` is the world-volume which corresponds to + `d` dimensional Euclidean space with a given (but arbitrary) +choice of length unit, and a given (but arbitrary) choice of zero. + +The default value of `d` is `3`. Thus `Space = Space 3`-/ structure Space (d : ℕ := 3) where /-- The underlying map `Fin d → ℝ` associated with a point in `Space`. -/ val : Fin d → ℝ From 36615ff6a4b2701d767c70aa549e6a4e2266c357 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 24 Feb 2026 10:57:28 +0000 Subject: [PATCH 2/9] feat: Add add and zero paragraph --- PhysLean/SpaceAndTime/Space/Basic.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index 48e70f45d..ce70d61cf 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -47,9 +47,14 @@ there is are two benefits of this: 2. It allows us to give the necessary physics context to results about `Space d`, which would not otherwise be possible if we reuse results from Mathlib. -Currently `Space d` has the structure of a `Module` (which requires the choice -of a zero), a future refactor should give `Space d` the structure of an `AddTorsor` -(an affine space) which does not require the choice of a zero. +Currently `Space d` has the instance of a `Module` (which requires the choice +of a zero), a future refactor should give `Space d` the instance of an `AddTorsor` +(an affine space) which does not require the choice of a zero. This has not been done +yet since `fderiv` requires a `Module` instance. + +Because of this, one should be careful to avoid using the explicit zero in `Space d`, +or adding two `Space d` values together. Where possible one should use +the `VAdd (EuclideanSpace ℝ (Fin d)) (Space d)` instance instead. -/ From 354bbe5aee7f1c08fae18fb54a137eb07ede8aa4 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 24 Feb 2026 16:33:56 +0000 Subject: [PATCH 3/9] Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Eric Wieser --- PhysLean/SpaceAndTime/Space/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index ce70d61cf..91cd8c5dc 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -48,7 +48,7 @@ there is are two benefits of this: would not otherwise be possible if we reuse results from Mathlib. Currently `Space d` has the instance of a `Module` (which requires the choice -of a zero), a future refactor should give `Space d` the instance of an `AddTorsor` +of a zero), a future refactor should give `Space d` only the instance of an `AddTorsor` (an affine space) which does not require the choice of a zero. This has not been done yet since `fderiv` requires a `Module` instance. From c524cece2bd5b76281ae8f013475405cdb40a2b9 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 25 Feb 2026 13:05:05 +0000 Subject: [PATCH 4/9] Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> --- PhysLean/SpaceAndTime/Space/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index 91cd8c5dc..6d5fd670b 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -71,7 +71,7 @@ TODO "HB6RR" "In the above documentation describe the notion of a type, and TODO "HB6VC" "Convert `Space` from an `abbrev` to a `def`." /-- The type `Space d` is the world-volume which corresponds to - `d` dimensional Euclidean space with a given (but arbitrary) + `d` dimensional (flat) Euclidean space with a given (but arbitrary) choice of length unit, and a given (but arbitrary) choice of zero. The default value of `d` is `3`. Thus `Space = Space 3`-/ From 4a657e68f0f6a0d87ecbd26a9c9a18112860c3e6 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 25 Feb 2026 13:05:53 +0000 Subject: [PATCH 5/9] Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> --- PhysLean/SpaceAndTime/Space/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index 6d5fd670b..ef06ad534 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -49,7 +49,7 @@ there is are two benefits of this: Currently `Space d` has the instance of a `Module` (which requires the choice of a zero), a future refactor should give `Space d` only the instance of an `AddTorsor` -(an affine space) which does not require the choice of a zero. This has not been done +(an affine space) which does not require the choice of a zero, in such a way that `Space d` should be a special case of Riemannian manifolds. This has not been done yet since `fderiv` requires a `Module` instance. Because of this, one should be careful to avoid using the explicit zero in `Space d`, From e103a396116d82bc5f9d107f389266792a4178d3 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 25 Feb 2026 13:06:04 +0000 Subject: [PATCH 6/9] Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com> --- PhysLean/SpaceAndTime/Space/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index ef06ad534..e686c2022 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -51,7 +51,7 @@ Currently `Space d` has the instance of a `Module` (which requires the choice of a zero), a future refactor should give `Space d` only the instance of an `AddTorsor` (an affine space) which does not require the choice of a zero, in such a way that `Space d` should be a special case of Riemannian manifolds. This has not been done yet since `fderiv` requires a `Module` instance. - +Similarly, `Norm` `InnerProductSpace` instances should be replaced by the `MetricSpace` instance giving directly the Euclidean distance. Because of this, one should be careful to avoid using the explicit zero in `Space d`, or adding two `Space d` values together. Where possible one should use the `VAdd (EuclideanSpace ℝ (Fin d)) (Space d)` instance instead. From 1a8ea0a291476b77b41b29a02821b6ce66c63cf4 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 25 Feb 2026 13:12:15 +0000 Subject: [PATCH 7/9] refactor: Update docs --- PhysLean/SpaceAndTime/Space/Basic.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index e686c2022..c84ece403 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -15,7 +15,7 @@ import Mathlib.Analysis.InnerProductSpace.Calculus # Space In this module, we define the the type `Space d` which corresponds -to a `d`-dimensional Euclidean space and prove some properties about it. +to `d`-dimensional flat Euclidean space and prove some properties about it. PhysLean sits downstream of Mathlib, and above we import the necessary Mathlib modules which contain (perhaps transitively through imports) the definitions and theorems we need. @@ -47,18 +47,19 @@ there is are two benefits of this: 2. It allows us to give the necessary physics context to results about `Space d`, which would not otherwise be possible if we reuse results from Mathlib. -Currently `Space d` has the instance of a `Module` (which requires the choice -of a zero), a future refactor should give `Space d` only the instance of an `AddTorsor` -(an affine space) which does not require the choice of a zero, in such a way that `Space d` should be a special case of Riemannian manifolds. This has not been done -yet since `fderiv` requires a `Module` instance. -Similarly, `Norm` `InnerProductSpace` instances should be replaced by the `MetricSpace` instance giving directly the Euclidean distance. +Currently `Space d` has the instances of `Module` (which requires the choice +of a zero), `Norm` and `InnerProductSpace`. +A future refactor should instead give `Space d` the instance of a `NormedAddTorsor` and a +`MetricSpace` giving it directly the Euclidean distance. + +This has not been done yet since `fderiv` requires a `Module` instance. + Because of this, one should be careful to avoid using the explicit zero in `Space d`, or adding two `Space d` values together. Where possible one should use the `VAdd (EuclideanSpace ℝ (Fin d)) (Space d)` instance instead. -/ - /-! ## The `Space` type From 6cc540b2ff09617392f5b1603484e65a8ae78c95 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 26 Feb 2026 05:12:49 +0000 Subject: [PATCH 8/9] Update PhysLean/SpaceAndTime/Space/Basic.lean Co-authored-by: Eric Wieser --- PhysLean/SpaceAndTime/Space/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index c84ece403..facb45a33 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -36,7 +36,7 @@ with a field `val : Fin d → ℝ`. +---------------------------------------------------+---------+-------+-----------+ | allows casting from `EuclideanSpace` | yes | yes | no | | carries instances from `EuclideanSpace` | yes | no | no | -| requires reproving of lemmas from `EuclideanSpace`| no | no | yes | +| requires reproving of lemmas from `EuclideanSpace`| no | yes | yes | +---------------------------------------------------+---------+-------+-----------+ The `structure` is the most conservative choice, as everything needs redefining, however, From 6aef2cc58d0ab2bd72d788e002c0c8de0649b2e2 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 2 Mar 2026 09:28:10 +0000 Subject: [PATCH 9/9] refactor: Review comments --- PhysLean/SpaceAndTime/Space/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean index facb45a33..7c6a732be 100644 --- a/PhysLean/SpaceAndTime/Space/Basic.lean +++ b/PhysLean/SpaceAndTime/Space/Basic.lean @@ -29,7 +29,7 @@ on the Lean Zulip, including: There is a choice between defining `Space d` as an `abbrev` of `EuclideanSpace ℝ (Fin d)`, as a `def` of a type with value `EuclideanSpace ℝ (Fin d)` or as a structure -with a field `val : Fin d → ℝ`. +with a field `val : Fin d → ℝ` : +---------------------------------------------------+---------+-------+-----------+ | | abbrev | def | structure | @@ -39,8 +39,8 @@ with a field `val : Fin d → ℝ`. | requires reproving of lemmas from `EuclideanSpace`| no | yes | yes | +---------------------------------------------------+---------+-------+-----------+ -The `structure` is the most conservative choice, as everything needs redefining, however, -there is are two benefits of this: +The `structure` is the most conservative choice, as everything needs redefining. However, +there is are two benefits of using it: 1. It allows us to be precise about the instances we define on `Space d`, and makes future refactoring of those instances easier. @@ -49,7 +49,7 @@ there is are two benefits of this: Currently `Space d` has the instances of `Module` (which requires the choice of a zero), `Norm` and `InnerProductSpace`. -A future refactor should instead give `Space d` the instance of a `NormedAddTorsor` and a +A future refactor should instead give `Space d` the instance of `NormedAddTorsor` and `MetricSpace` giving it directly the Euclidean distance. This has not been done yet since `fderiv` requires a `Module` instance.