From 03cbedbe164bf3a30ba3b58f2c8392ab11f81583 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 5 Mar 2026 06:55:39 +0000
Subject: [PATCH 1/6] feat: AddTorsor instance on space

---
 PhysLean/SpaceAndTime/Space/Basic.lean | 54 +++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 1 deletion(-)

diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index 85903fa66..c91006b13 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -216,13 +216,39 @@ instance {d} : Module ℝ (Space d) where
 
 /-!
 
-## B.3. Addition of Euclidean spaces
+## B.3. Relation to `EuclideanSpace`
+
+-/
+
+/-- The map from `Space d` to `EuclideanSpace ℝ (Fin d)`. -/
+def toEuclid {d} (s : Space d) : EuclideanSpace ℝ (Fin d) where
+  ofLp := s.val
+
+@[simp]
+lemma toEuclid_apply {d} (s : Space d) (i : Fin d) : toEuclid s i = s i := rfl
+
+lemma toEuclid_injective {d} : Function.Injective (@toEuclid d) := fun s1 s2 h => by
+  ext i
+  rw [← toEuclid_apply s1 i, ← toEuclid_apply s2 i, h]
+
+lemma toEuclid_surjective {d} : Function.Surjective (@toEuclid d) := fun v => by
+  use ⟨v.ofLp⟩
+  ext i
+  simp [toEuclid_apply]
+
+/-!
+
+## B.3.1. The additive action
 
 -/
 
 noncomputable instance : VAdd (EuclideanSpace ℝ (Fin d)) (Space d) where
   vadd v s := ⟨fun i => v i + s.val i⟩
 
+@[simp]
+lemma vadd_toEuclid {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
+    toEuclid (v +ᵥ s) = v + toEuclid s := rfl
+
 @[simp]
 lemma vadd_val {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
     (v +ᵥ s).val = fun i => v i + s.val i := rfl
@@ -267,6 +293,32 @@ lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
 
 /-!
 
+## B.3.2. Subtraction
+
+-/
+
+noncomputable instance {d} : VSub (EuclideanSpace ℝ (Fin d)) (Space d) where
+  vsub s1 s2 := toEuclid s1 - toEuclid s2
+
+lemma vsub_eq_toEuclid_sub {d} (s1 s2 : Space d) :
+    s1 -ᵥ s2 = toEuclid s1 - toEuclid s2 := rfl
+
+@[simp]
+lemma vsub_apply {d} (s1 s2 : Space d) (i : Fin d) :
+    (s1 -ᵥ s2) i = s1 i - s2 i := rfl
+
+/-!
+
+## B.3.3. AddTorsor instance
+
+-/
+
+noncomputable instance {d} : AddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
+  vsub_vadd' s1 s2 := toEuclid_injective <| by simp [vsub_eq_toEuclid_sub]
+  vadd_vsub' s1 s2 := by simp [vsub_eq_toEuclid_sub, vadd_toEuclid]
+
+/-!
+
 ## B.3. Instance of an inner product space
 
 -/

From 761c6526c750ad0e904b2b32b0cb5a712299a4d5 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 5 Mar 2026 08:10:06 +0000
Subject: [PATCH 2/6] refactor: Redefine VSub

---
 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 c91006b13..f927f46da 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -298,7 +298,7 @@ lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
 -/
 
 noncomputable instance {d} : VSub (EuclideanSpace ℝ (Fin d)) (Space d) where
-  vsub s1 s2 := toEuclid s1 - toEuclid s2
+  vsub s1 s2 := WithLp.toLp 2 <| fun i => s1 i - s2 i
 
 lemma vsub_eq_toEuclid_sub {d} (s1 s2 : Space d) :
     s1 -ᵥ s2 = toEuclid s1 - toEuclid s2 := rfl

From ebccb6d9f4a80722c16c0497fcbb0ababf3d2757 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 5 Mar 2026 10:05:43 +0000
Subject: [PATCH 3/6] refactor: Split basic and module

---
 PhysLean.lean                                 |   1 +
 .../DDimensions/SpaceDHilbertSpace/Basic.lean |   2 +-
 PhysLean/SpaceAndTime/Space/Basic.lean        | 667 ++----------------
 .../SpaceAndTime/Space/Integrals/Basic.lean   |   2 +-
 PhysLean/SpaceAndTime/Space/Module.lean       | 603 ++++++++++++++++
 5 files changed, 654 insertions(+), 621 deletions(-)
 create mode 100644 PhysLean/SpaceAndTime/Space/Module.lean

diff --git a/PhysLean.lean b/PhysLean.lean
index a60765a40..2d8e75697 100644
--- a/PhysLean.lean
+++ b/PhysLean.lean
@@ -352,6 +352,7 @@ import PhysLean.SpaceAndTime.Space.Integrals.Basic
 import PhysLean.SpaceAndTime.Space.Integrals.RadialAngularMeasure
 import PhysLean.SpaceAndTime.Space.IsDistBounded
 import PhysLean.SpaceAndTime.Space.LengthUnit
+import PhysLean.SpaceAndTime.Space.Module
 import PhysLean.SpaceAndTime.Space.Norm
 import PhysLean.SpaceAndTime.Space.Slice
 import PhysLean.SpaceAndTime.Space.Translations
diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
index 5aeb42810..4f2f874e3 100644
--- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
+++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean
@@ -5,7 +5,7 @@ Authors: Gregory J. Loges
 -/
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.MeasureTheory.Function.L2Space
-import PhysLean.SpaceAndTime.Space.Basic
+import PhysLean.SpaceAndTime.Space.Module
 /-!
 
 # Hilbert space for quantum mechanics on Space d
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index f927f46da..ee3c70231 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -17,6 +17,10 @@ import Mathlib.Analysis.InnerProductSpace.Calculus
 In this module, we define the the type `Space d` which corresponds
 to `d`-dimensional flat Euclidean space and prove some properties about it.
 
+The scope of this module is to define on `Space d` basic instances related translations and
+the metric. We do not here define the structure of a `Module` on `Space d`, as this is done in
+`PhysLean.SpaceAndTime.Space.Module`.
+
 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,12 +51,18 @@ there is are two benefits of using it:
 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 instances of `Module` (which requires the choice
-of a zero), `Norm` and `InnerProductSpace`.
-A future refactor should instead give `Space d` the instance of `NormedAddTorsor` and
-`MetricSpace` giving it directly the Euclidean distance.
+In this module we give `Space d` the instances of a `NormedAddTorsor`
+and a `MetricSpace`. These physically correspond to the statement that
+you can add a vector to a point in space, and that there is a notion of distance between
+points in space. This notion of distance corresponds to a choice of length unit.
+
+In `PhysLean.SpaceAndTime.Space.Module` we give `Space d` the structure of a `Module`
+(aka vector space), a `Norm` and an `InnerProductSpace`. These require certain choices, for example
+the choice of a zero in `Space d`.
 
-This has not been done yet since `fderiv` requires a `Module` instance.
+This module structure is necessary in numerous places. For example,
+the normal derivatives used by physicists `∂_x, ∂_y, ∂_z` require a
+module structure.
 
 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
@@ -62,7 +72,7 @@ the `VAdd (EuclideanSpace ℝ (Fin d)) (Space d)` instance instead.
 
 /-!
 
-## The `Space` type
+## A. The `Space` type
 
 -/
 
@@ -120,121 +130,22 @@ lemma eq_of_apply {d} {p q : Space d}
 
 /-!
 
-## B.1. Instance of an additive commutative monoid
+## B.2. The Non-emptiness
 
 -/
 
-instance {d} : Add (Space d) where
-  add p q := ⟨fun i => p.val i + q.val i⟩
-
-@[simp]
-lemma add_val {d: ℕ} (x y : Space d) :
-    (x + y).val = x.val + y.val := rfl
-
-@[simp]
-lemma add_apply {d : ℕ} (x y : Space d) (i : Fin d) :
-    (x + y) i = x i + y i := by
-  simp [add_val]
+instance {d} : Nonempty (Space d) := Nonempty.intro ⟨fun _ => 0⟩
 
-instance {d} : Zero (Space d) where
-  zero := ⟨fun _ => 0⟩
-
-@[simp]
-lemma zero_val {d : ℕ} : (0 : Space d).val = fun _ => 0 := rfl
-
-@[simp]
-lemma zero_apply {d : ℕ} (i : Fin d) :
-    (0 : Space d) i = 0 := by
-  simp [zero_val]
-
-instance {d} : AddCommMonoid (Space d) where
-  add_assoc a b c:= by
-    apply eq_of_val
-    simp only [add_val]
-    ring
-  zero_add a := by
-    apply eq_of_val
-    simp only [zero_val, add_val, add_eq_right]
-    rfl
-  add_zero a := by
-    apply eq_of_val
-    simp only [zero_val, add_val, add_eq_left]
-    rfl
-  add_comm a b := by
-    apply eq_of_val
-    simp only [add_val]
-    ring
-  nsmul n a := ⟨fun i => n • a.val i⟩
-
-@[simp]
-lemma nsmul_val {d : ℕ} (n : ℕ) (a : Space d) :
-    (n • a).val = fun i => n • a.val i := rfl
-
-@[simp]
-lemma nsmul_apply {d : ℕ} (n : ℕ) (a : Space d) (i : Fin d) :
-    (n • a) i = n • (a i) := by rfl
-
-/-!
-
-## B.2. Instance of a module over `ℝ`
-
--/
-
-instance {d} : SMul ℝ (Space d) where
-  smul c p := ⟨fun i => c * p.val i⟩
-
-@[simp]
-lemma smul_val {d : ℕ} (c : ℝ) (p : Space d) :
-    (c • p).val = fun i => c * p.val i := rfl
-
-@[simp]
-lemma smul_apply {d : ℕ} (c : ℝ) (p : Space d) (i : Fin d) :
-    (c • p) i = c * (p i) := by rfl
-
-instance {d} : Module ℝ (Space d) where
-  one_smul x := by
-    ext i
-    simp
-  mul_smul a b x := by
-    ext i
-    simp only [smul_apply]
-    ring
-  smul_add a x y := by
-    ext i
-    simp only [smul_apply, add_apply]
-    ring
-  smul_zero a := by
-    ext i
-    simp
-  add_smul a b x := by
-    ext i
-    simp only [smul_apply, add_apply]
-    ring
-  zero_smul x := by
-    ext i
-    simp
-
-/-!
-
-## B.3. Relation to `EuclideanSpace`
-
--/
-
-/-- The map from `Space d` to `EuclideanSpace ℝ (Fin d)`. -/
-def toEuclid {d} (s : Space d) : EuclideanSpace ℝ (Fin d) where
-  ofLp := s.val
-
-@[simp]
-lemma toEuclid_apply {d} (s : Space d) (i : Fin d) : toEuclid s i = s i := rfl
-
-lemma toEuclid_injective {d} : Function.Injective (@toEuclid d) := fun s1 s2 h => by
-  ext i
-  rw [← toEuclid_apply s1 i, ← toEuclid_apply s2 i, h]
+instance {d : ℕ} : Nontrivial (Space d.succ) := by
+  refine { exists_pair_ne := ?_ }
+  use ⟨fun _ => 0⟩, ⟨fun _ => 1⟩
+  simp only [Nat.succ_eq_add_one, ne_eq, mk.injEq]
+  refine Function.ne_iff.mpr ⟨0, ?_⟩
+  simp
 
-lemma toEuclid_surjective {d} : Function.Surjective (@toEuclid d) := fun v => by
-  use ⟨v.ofLp⟩
+instance : Subsingleton (Space 0) := Subsingleton.intro <| fun x y => by
   ext i
-  simp [toEuclid_apply]
+  fin_cases i
 
 /-!
 
@@ -245,10 +156,6 @@ lemma toEuclid_surjective {d} : Function.Surjective (@toEuclid d) := fun v => by
 noncomputable instance : VAdd (EuclideanSpace ℝ (Fin d)) (Space d) where
   vadd v s := ⟨fun i => v i + s.val i⟩
 
-@[simp]
-lemma vadd_toEuclid {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
-    toEuclid (v +ᵥ s) = v + toEuclid s := rfl
-
 @[simp]
 lemma vadd_val {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
     (v +ᵥ s).val = fun i => v i + s.val i := rfl
@@ -264,17 +171,6 @@ lemma vadd_transitive {d} (s1 s2 : Space d) :
   ext i
   simp
 
-lemma eq_vadd_zero {d} (s : Space d) :
-    ∃ v : EuclideanSpace ℝ (Fin d), s = v +ᵥ (0 : Space d) := by
-  obtain ⟨v, h⟩ := vadd_transitive 0 s
-  use v
-  rw [h]
-
-@[simp]
-lemma smul_vadd_zero {d} (k : ℝ) (v : EuclideanSpace ℝ (Fin d)) :
-    k • (v +ᵥ (0 : Space d)) = (k • v) +ᵥ (0 : Space d) := by
-  ext i
-  simp
 
 noncomputable instance : AddAction (EuclideanSpace ℝ (Fin d)) (Space d) where
   zero_vadd s := by
@@ -285,12 +181,6 @@ noncomputable instance : AddAction (EuclideanSpace ℝ (Fin d)) (Space d) where
     simp only [vadd_apply, PiLp.add_apply]
     ring
 
-@[simp]
-lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
-    (v1 +ᵥ (0 : Space d)) + (v2 +ᵥ (0 : Space d)) = (v1 + v2) +ᵥ (0 : Space d) := by
-  ext i
-  simp
-
 /-!
 
 ## B.3.2. Subtraction
@@ -300,9 +190,6 @@ lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
 noncomputable instance {d} : VSub (EuclideanSpace ℝ (Fin d)) (Space d) where
   vsub s1 s2 := WithLp.toLp 2 <| fun i => s1 i - s2 i
 
-lemma vsub_eq_toEuclid_sub {d} (s1 s2 : Space d) :
-    s1 -ᵥ s2 = toEuclid s1 - toEuclid s2 := rfl
-
 @[simp]
 lemma vsub_apply {d} (s1 s2 : Space d) (i : Fin d) :
     (s1 -ᵥ s2) i = s1 i - s2 i := rfl
@@ -314,509 +201,51 @@ lemma vsub_apply {d} (s1 s2 : Space d) (i : Fin d) :
 -/
 
 noncomputable instance {d} : AddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
-  vsub_vadd' s1 s2 := toEuclid_injective <| by simp [vsub_eq_toEuclid_sub]
-  vadd_vsub' s1 s2 := by simp [vsub_eq_toEuclid_sub, vadd_toEuclid]
-
-/-!
-
-## B.3. Instance of an inner product space
-
--/
-
-noncomputable instance {d} : Norm (Space d) where
-  norm p := √ (∑ i, (p i)^2)
-
-lemma norm_eq {d} (p : Space d) : ‖p‖ = √ (∑ i, (p i) ^ 2) := by
-  rfl
-
-@[simp]
-lemma abs_eval_le_norm {d} (p : Space d) (i : Fin d) :
-    |p i| ≤ ‖p‖ := by
-  simp [norm_eq]
-  refine Real.abs_le_sqrt ?_
-  trans ∑ j ∈ {i}, (p j) ^ 2
-  · simp
-  refine Finset.sum_le_univ_sum_of_nonneg (fun i => by positivity)
-
-lemma norm_sq_eq {d} (p : Space d) :
-    ‖p‖ ^ 2 = ∑ i, (p i) ^ 2 := by
-  rw [norm_eq]
-  refine Real.sq_sqrt ?_
-  positivity
-
-lemma point_dim_zero_eq (p : Space 0) : p = 0 := by
-  ext i
-  fin_cases i
-
-@[simp]
-lemma norm_vadd_zero {d} (v : EuclideanSpace ℝ (Fin d)) :
-    ‖v +ᵥ (0 : Space d)‖ = ‖v‖ := by
-  simp [norm_eq, PiLp.norm_eq_of_L2]
-
-instance : Neg (Space d) where
-  neg p := ⟨fun i => - (p.val i)⟩
-
-@[simp]
-lemma neg_val {d : ℕ} (p : Space d) :
-    (-p).val = fun i => - (p.val i) := rfl
-
-@[simp]
-lemma neg_apply {d : ℕ} (p : Space d) (i : Fin d) :
-    (-p) i = - (p i) := by rfl
-
-noncomputable instance {d} : AddCommGroup (Space d) where
-  zsmul z p := ⟨fun i => z * p.val i⟩
-  neg_add_cancel p := by
+  vsub_vadd' s1 s2 := by
     ext i
     simp
-  zsmul_zero' p := by
-    ext i
-    simp
-  zsmul_succ' n p := by
-    ext i
-    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, Int.cast_add, Int.cast_natCast,
-      Int.cast_one, add_apply]
-    ring
-  zsmul_neg' n p := by
+  vadd_vsub' s1 s2 := by
     ext i
-    simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, Nat.succ_eq_add_one,
-      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_apply]
-    ring
-
-@[simp]
-lemma sub_apply {d} (p q : Space d) (i : Fin d) :
-    (p - q) i = p i - q i := by
-  simp [sub_eq_add_neg, neg_apply, add_apply]
-
-@[simp]
-lemma sub_val {d} (p q : Space d) :
-    (p - q).val = fun i => p.val i - q.val i := by rfl
-
-@[simp]
-lemma vadd_zero_sub_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
-    (v1 +ᵥ (0 : Space d)) - (v2 +ᵥ (0 : Space d)) = (v1 - v2) +ᵥ (0 : Space d) := by
-  ext i
-  simp [sub_apply, vadd_apply]
-
-noncomputable instance {d} : SeminormedAddCommGroup (Space d) where
-  dist_self x := by
-    simp [norm_eq]
-  dist_comm x y := by
-    simp [norm_eq]
-    congr
-    funext i
-    ring
-  dist_triangle := by
-    intros x y z
-    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
-    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
-    obtain ⟨v3, rfl⟩ := eq_vadd_zero z
-    simp [vadd_zero_sub_vadd_zero, norm_vadd_zero]
-    exact norm_sub_le_norm_sub_add_norm_sub v1 v2 v3
-
-@[simp]
-lemma dist_eq {d} (p q : Space d) :
-    dist p q = ‖p - q‖ := by
-  rfl
-
-noncomputable instance : NormedAddCommGroup (Space d) where
-  eq_of_dist_eq_zero := by
-    intro x y h
-    simp at h
-    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
-    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
-    simp only [vadd_zero_sub_vadd_zero, norm_vadd_zero] at h
-    congr
-    exact eq_of_dist_eq_zero h
-
-instance {d} : Inner ℝ (Space d) where
-  inner p q := ∑ i, p i * q i
-
-@[simp]
-lemma inner_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
-    inner ℝ (v1 +ᵥ (0 : Space d)) (v2 +ᵥ (0 : Space d)) = Inner.inner ℝ v1 v2 := by
-  simp [inner, vadd_apply]
-  apply Finset.sum_congr rfl
-  intro i hi
-  ring
-
-lemma inner_apply {d} (p q : Space d) :
-    inner ℝ p q = ∑ i, p i * q i := by rfl
-
-instance {d} : InnerProductSpace ℝ (Space d) where
-  norm_smul_le a x := by
-    obtain ⟨v, rfl⟩ := eq_vadd_zero x
-    simp only [smul_vadd_zero, norm_vadd_zero, Real.norm_eq_abs]
-    exact norm_smul_le a v
-  norm_sq_eq_re_inner x := by
-    obtain ⟨v, rfl⟩ := eq_vadd_zero x
     simp
-  conj_inner_symm x y := by
-    simp [inner_apply]
-    congr
-    funext i
-    ring
-  add_left x y z := by
-    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
-    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
-    obtain ⟨v3, rfl⟩ := eq_vadd_zero z
-    simp only [add_vadd_zero, inner_vadd_zero]
-    exact InnerProductSpace.add_left v1 v2 v3
-  smul_left x y a := by
-    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
-    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
-    simp only [smul_vadd_zero, inner_vadd_zero, conj_trivial]
-    exact InnerProductSpace.smul_left v1 v2 a
-
-/-!
-
-## B.4. Instance of a measurable space
-
--/
-
-instance {d : ℕ} : MeasurableSpace (Space d) := borel (Space d)
-
-instance {d : ℕ} : BorelSpace (Space d) where
-  measurable_eq := by rfl
-
-TODO "HB6YZ" "In the above documentation describe what an instance is, and why
-  it is useful to have instances for `Space d`."
-
-TODO "HB6WN" "After TODO 'HB6VC', give `Space d` the necessary instances
-  using `inferInstanceAs`."
-/-!
-
-## The norm on `Space`
-
--/
-
-/-!
-
-## Inner product
-
--/
-
-lemma inner_eq_sum {d} (p q : Space d) :
-    inner ℝ p q = ∑ i, p i * q i := by
-  simp [inner]
-
-@[simp]
-lemma sum_apply {ι : Type} [Fintype ι] (f : ι → Space d) (i : Fin d) :
-    (∑ x, f x) i = ∑ x, f x i := by
-  let P (ι : Type) [Fintype ι] : Prop := ∀ (f : ι → Space d) (i : Fin d), (∑ x, f x) i = ∑ x, f x i
-  have h1 : P ι := by
-    apply Fintype.induction_empty_option
-    · intro α β h e h f i
-      rw [← @e.sum_comp _, h, ← @e.sum_comp _]
-    · simp [P]
-    · intro α _ h f i
-      simp only [Fintype.sum_option, add_apply, add_right_inj]
-      rw [h]
-  exact h1 f i
-
-/-!
-
-## Basis
-
--/
-
-TODO "HB6Z4" "In the above documentation describe the notion of a basis
-  in Lean."
-
-/-- The standard basis of Space based on `Fin d`. -/
-noncomputable def basis {d} : OrthonormalBasis (Fin d) ℝ (Space d) where
-  repr := {
-    toFun p := WithLp.toLp 2 fun i => p i
-    invFun := fun v => ⟨v⟩
-    left_inv := by
-      intro p
-      rfl
-    right_inv := by
-      intro v
-      rfl
-    map_add' := by
-      intro v1 v2
-      rfl
-    map_smul' := by
-      intro c v
-      rfl
-    norm_map' := by
-      intro x
-      simp [norm_eq, PiLp.norm_eq_of_L2]}
-
-lemma apply_eq_basis_repr_apply {d} (p : Space d) (i : Fin d) :
-    p i = basis.repr p i := by
-  simp [basis]
-
-@[simp]
-lemma basis_repr_apply {d} (p : Space d) (i : Fin d) :
-    basis.repr p i = p i := by
-  simp [apply_eq_basis_repr_apply]
-
-@[simp]
-lemma basis_repr_symm_apply {d} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) :
-    basis.repr.symm v i = v i := by rfl
-
-lemma basis_apply {d} (i j : Fin d) :
-    basis i j = if i = j then 1 else 0 := by
-  simp [apply_eq_basis_repr_apply]
-  congr 1
-  exact Lean.Grind.eq_congr' rfl rfl
-
-@[simp]
-lemma basis_self {d} (i : Fin d) : basis i i = 1 := by
-  simp [basis_apply]
-
-@[simp high]
-lemma inner_basis {d} (p : Space d) (i : Fin d) :
-    inner ℝ p (basis i) = p i := by
-  simp [inner_eq_sum, basis_apply]
-
-@[simp high]
-lemma basis_inner {d} (i : Fin d) (p : Space d) :
-    inner ℝ (basis i) p = p i := by
-  simp [inner_eq_sum, basis_apply]
-
-open InnerProductSpace
-
-lemma basis_repr_inner_eq {d} (p : Space d) (v : EuclideanSpace ℝ (Fin d)) :
-    ⟪basis.repr p, v⟫_ℝ = ⟪p, basis.repr.symm v⟫_ℝ := by
-  exact LinearIsometryEquiv.inner_map_eq_flip basis.repr p v
-
-instance {d : ℕ} : FiniteDimensional ℝ (Space d) :=
-  Module.Basis.finiteDimensional_of_finite (h := basis.toBasis)
-
-@[simp]
-lemma finrank_eq_dim {d : ℕ} : Module.finrank ℝ (Space d) = d := by
-  simp [Module.finrank_eq_nat_card_basis (basis.toBasis)]
-
-@[simp]
-lemma rank_eq_dim {d : ℕ} : Module.rank ℝ (Space d) = d := by
-  simp [rank_eq_card_basis (basis.toBasis)]
-
-@[simp]
-lemma fderiv_basis_repr {d} (p : Space d) :
-    fderiv ℝ basis.repr p = basis.repr.toContinuousLinearMap := by
-  change fderiv ℝ basis.repr.toContinuousLinearMap p = _
-  rw [ContinuousLinearMap.fderiv]
-
-@[simp]
-lemma fderiv_basis_repr_symm {d} (v : EuclideanSpace ℝ (Fin d)) :
-    fderiv ℝ basis.repr.symm v = basis.repr.symm.toContinuousLinearMap := by
-  change fderiv ℝ basis.repr.symm.toContinuousLinearMap v = _
-  rw [ContinuousLinearMap.fderiv]
 
 /-!
 
-## Coordinates
+## B.4. PseudoMetricSpace
 
 -/
 
-/-- The standard coordinate functions of Space based on `Fin d`.
-
-The notation `𝔁 μ p` can be used for this. -/
-noncomputable def coord (μ : Fin d) (p : Space d) : ℝ :=
-  inner ℝ p (basis μ)
-
-lemma coord_apply (μ : Fin d) (p : Space d) :
-    coord μ p = p μ := by
-  simp [coord]
-
-/-- The standard coordinate functions of Space based on `Fin d`, as a continuous linear map. -/
-noncomputable def coordCLM {d} (μ : Fin d) : Space d →L[ℝ] ℝ where
-  toFun := coord μ
-  map_add' := fun p q => by
-    simp [coord, basis, inner_add_left]
-  map_smul' := fun c p => by
-    simp [coord, basis, inner_smul_left]
-  cont := by
-    unfold coord
-    fun_prop
-
-open ContDiff
-
-@[fun_prop]
-lemma coord_contDiff {i} : ContDiff ℝ ∞ (fun x : Space d => x.coord i) := by
-  change ContDiff ℝ ∞ (coordCLM i)
-  fun_prop
-
-lemma coordCLM_apply (μ : Fin d) (p : Space d) :
-    coordCLM μ p = coord μ p := by
-  rfl
-
-@[inherit_doc coord]
-scoped notation "𝔁" => coord
-
-@[fun_prop]
-lemma eval_continuous {d} (i : Fin d) :
-    Continuous (fun p : Space d => p i) := by
-  convert (coordCLM i).continuous
-  simp [coordCLM_apply, coord]
-
-@[fun_prop]
-lemma eval_differentiable {d} (i : Fin d) :
-    Differentiable ℝ (fun p : Space d => p i) := by
-  convert (coordCLM i).differentiable
-  simp [coordCLM_apply, coord]
-
-@[fun_prop]
-lemma eval_contDiff {d n} (i : Fin d) :
-    ContDiff ℝ n (fun p : Space d => p i) := by
-  convert (coordCLM i).contDiff
-  simp [coordCLM_apply, coord]
-
-/-- The continuous linear equivalence between `Space d` and the corresponding `Pi` type. -/
-def equivPi (d : ℕ) :
-    Space d ≃L[ℝ] Π (_ : Fin d), ℝ := LinearEquiv.toContinuousLinearEquiv <|
-  {
-    toFun := fun p i => p i
-    map_add' p1 p2 := by funext i; simp
-    map_smul' p r := by funext i; simp
-    invFun := fun f => ⟨f⟩
-  }
-
-@[fun_prop]
-lemma mk_continuous {d : ℕ} :
-    Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous
-
-@[fun_prop]
-lemma mk_differentiable {d : ℕ} :
-    Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable
-
-@[fun_prop]
-lemma mk_contDiff {d n : ℕ} :
-    ContDiff ℝ n (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.contDiff
+noncomputable instance {d} : Dist (Space d) where
+  dist p q := √ (∑ i, (p i - q i) ^ 2)
 
-@[simp]
-lemma fderiv_mk {d : ℕ} (f : Fin d → ℝ) :
-    fderiv ℝ Space.mk f = (equivPi d).symm := by
-  change fderiv ℝ (equivPi d).symm f = _
-  rw [@ContinuousLinearEquiv.fderiv]
+lemma dist_eq {d} (p q : Space d) :
+    dist p q = √ (∑ i, (p i - q i) ^ 2) := rfl
 
-@[simp]
-lemma fderiv_val {d : ℕ} (p : Space d) :
-    fderiv ℝ Space.val p = (equivPi d) := by
-  change fderiv ℝ (equivPi d) p = _
-  rw [@ContinuousLinearEquiv.fderiv]
+noncomputable instance {d} : PseudoMetricSpace (Space d) where
+  dist_self x := by simp [dist_eq]
+  dist_comm x y := by grind [dist_eq]
+  dist_triangle x y z := by
+    convert dist_triangle (WithLp.toLp 2 fun i => x i) (WithLp.toLp 2 fun i => y i)
+      (WithLp.toLp 2 fun i => z i)
+    all_goals
+    · rw [EuclideanSpace.dist_eq]
+      simp only [dist, sq_abs]
 
 /-!
 
-## Directions
+## B.5. NormAddTorsor instance
 
 -/
 
-/-- Notion of direction where `unit` returns a unit vector in the direction specified. -/
-structure Direction (d : ℕ := 3) where
-  /-- Unit vector specifying the direction. -/
-  unit : Space d
-  norm : ‖unit‖ = 1
-
-/-- Direction of a `Space` value with respect to the origin. -/
-noncomputable def toDirection {d : ℕ} (x : Space d) (h : x ≠ 0) : Direction d where
-  unit := (‖x‖⁻¹) • x
-  norm := norm_smul_inv_norm h
-
-@[simp]
-lemma direction_unit_sq_sum {d} (s : Direction d) :
-    ∑ i : Fin d, (s.unit i) ^ 2 = 1 := by
-  trans (‖s.unit‖) ^ 2
-  · rw [norm_sq_eq]
-  · rw [s.norm]
-    simp
+noncomputable instance : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
+  dist_eq_norm' p q := by simp [dist, EuclideanSpace.norm_eq]
 
 /-!
 
-## One equiv
+## B.6. Metric space instance
 
 -/
 
-/-- The linear isometric equivalence between `Space 1` and `ℝ`. -/
-noncomputable def oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ where
-  toFun x := x 0
-  invFun x := ⟨fun _ => x⟩
-  left_inv x := by
-    ext i; fin_cases i; simp
-  right_inv x := by simp
-  map_add' x y := by rfl
-  map_smul' c x := by rfl
-  norm_map' x := by
-    simp only [Fin.isValue, LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, Real.norm_eq_abs]
-    rw [norm_eq]
-    simp only [Fin.isValue, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
-    exact Eq.symm (Real.sqrt_sq_eq_abs (x 0))
-
-lemma oneEquiv_coe :
-    (oneEquiv : Space 1 → ℝ) = fun x => x 0 := by
-  rfl
-
-lemma oneEquiv_symm_coe :
-    (oneEquiv.symm : ℝ → Space 1) = (fun x => ⟨fun _ => x⟩) := by
-  rfl
-
-lemma oneEquiv_symm_apply (x : ℝ) (i : Fin 1) :
-    oneEquiv.symm x i = x := by
-  fin_cases i
-  rfl
-
-lemma oneEquiv_continuous :
-    Continuous (oneEquiv : Space 1 → ℝ) := by
-  simp [oneEquiv_coe]
-  fun_prop
-
-lemma oneEquiv_symm_continuous :
-    Continuous (oneEquiv.symm : ℝ → Space 1) := by
-  simp [oneEquiv_symm_coe]
-  fun_prop
-
-/-- The continuous linear equivalence between `Space 1` and `ℝ`. -/
-noncomputable def oneEquivCLE : Space 1 ≃L[ℝ] ℝ where
-  toLinearEquiv := oneEquiv
-  continuous_toFun := by
-    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe]
-    erw [oneEquiv_coe]
-    fun_prop
-  continuous_invFun := by
-    simp only [LinearEquiv.invFun_eq_symm]
-    erw [oneEquiv_symm_coe]
-    fun_prop
-
-open MeasureTheory
-lemma oneEquiv_measurableEmbedding : MeasurableEmbedding oneEquiv where
-  injective := oneEquiv.injective
-  measurable := by fun_prop
-  measurableSet_image' := by
-    intro s hs
-    change MeasurableSet (⇑oneEquivCLE '' s)
-    rw [ContinuousLinearEquiv.image_eq_preimage_symm]
-    exact oneEquiv.symm.continuous.measurable hs
-
-lemma oneEquiv_symm_measurableEmbedding : MeasurableEmbedding oneEquiv.symm where
-  injective := oneEquiv.symm.injective
-  measurable := by fun_prop
-  measurableSet_image' := by
-    intro s hs
-    change MeasurableSet (⇑oneEquivCLE.symm '' s)
-    rw [ContinuousLinearEquiv.image_eq_preimage_symm]
-    exact oneEquiv.continuous.measurable hs
-
-lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
-  LinearIsometryEquiv.measurePreserving oneEquiv
-
-lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
-  exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
+noncomputable instance {d} : MetricSpace (Space d) where
+  eq_of_dist_eq_zero {p q} := by simp [NormedAddTorsor.dist_eq_norm']
 
-instance {d : ℕ} : Nontrivial (Space d.succ) := by
-  refine { exists_pair_ne := ?_ }
-  use 0, basis 0
-  simp only [Nat.succ_eq_add_one, ne_eq]
-  by_contra hn
-  have h0 : (basis 0 : Space d.succ) 0 = 1 := by simp
-  rw [← hn] at h0
-  simp at h0
-
-instance : Subsingleton (Space 0) := by
-  apply Subsingleton.intro
-  intro x y
-  ext i
-  fin_cases i
 end Space
diff --git a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
index e05b988e5..3a005b363 100644
--- a/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Integrals/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import PhysLean.SpaceAndTime.Space.Basic
+import PhysLean.SpaceAndTime.Space.Module
 /-!
 
 # Integrals in Space
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
new file mode 100644
index 000000000..c5286bee1
--- /dev/null
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -0,0 +1,603 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import PhysLean.SpaceAndTime.Space.Basic
+/-!
+
+# The strucutre of a module on Space
+
+The scope of this module is to define on `Space d` the structure of a `Module`
+(aka vector space), a `Norm` and an `InnerProductSpace`, and give properties of these structures.
+
+These instances require certain non-canonical choices to be made, for example the choice
+of a zero and for a basis, a choice of orientation.
+
+-/
+
+namespace Space
+
+/-!
+
+## A.1. Instance of an additive commutative monoid
+
+-/
+
+instance {d} : Add (Space d) where
+  add p q := ⟨fun i => p.val i + q.val i⟩
+
+@[simp]
+lemma add_val {d: ℕ} (x y : Space d) :
+    (x + y).val = x.val + y.val := rfl
+
+@[simp]
+lemma add_apply {d : ℕ} (x y : Space d) (i : Fin d) :
+    (x + y) i = x i + y i := by
+  simp [add_val]
+
+instance {d} : Zero (Space d) where
+  zero := ⟨fun _ => 0⟩
+
+@[simp]
+lemma zero_val {d : ℕ} : (0 : Space d).val = fun _ => 0 := rfl
+
+@[simp]
+lemma zero_apply {d : ℕ} (i : Fin d) :
+    (0 : Space d) i = 0 := by
+  simp [zero_val]
+
+instance {d} : AddCommMonoid (Space d) where
+  add_assoc a b c:= by
+    apply eq_of_val
+    simp only [add_val]
+    ring
+  zero_add a := by
+    apply eq_of_val
+    simp only [zero_val, add_val, add_eq_right]
+    rfl
+  add_zero a := by
+    apply eq_of_val
+    simp only [zero_val, add_val, add_eq_left]
+    rfl
+  add_comm a b := by
+    apply eq_of_val
+    simp only [add_val]
+    ring
+  nsmul n a := ⟨fun i => n • a.val i⟩
+
+@[simp]
+lemma nsmul_val {d : ℕ} (n : ℕ) (a : Space d) :
+    (n • a).val = fun i => n • a.val i := rfl
+
+@[simp]
+lemma nsmul_apply {d : ℕ} (n : ℕ) (a : Space d) (i : Fin d) :
+    (n • a) i = n • (a i) := by rfl
+
+
+lemma eq_vadd_zero {d} (s : Space d) :
+    ∃ v : EuclideanSpace ℝ (Fin d), s = v +ᵥ (0 : Space d) := by
+  obtain ⟨v, h⟩ := vadd_transitive 0 s
+  use v
+  rw [h]
+
+@[simp]
+lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
+    (v1 +ᵥ (0 : Space d)) + (v2 +ᵥ (0 : Space d)) = (v1 + v2) +ᵥ (0 : Space d) := by
+  ext i
+  simp
+
+/-!
+
+## A.2. Instance of a module over `ℝ`
+
+-/
+
+instance {d} : SMul ℝ (Space d) where
+  smul c p := ⟨fun i => c * p.val i⟩
+
+@[simp]
+lemma smul_val {d : ℕ} (c : ℝ) (p : Space d) :
+    (c • p).val = fun i => c * p.val i := rfl
+
+@[simp]
+lemma smul_apply {d : ℕ} (c : ℝ) (p : Space d) (i : Fin d) :
+    (c • p) i = c * (p i) := by rfl
+
+@[simp]
+lemma smul_vadd_zero {d} (k : ℝ) (v : EuclideanSpace ℝ (Fin d)) :
+    k • (v +ᵥ (0 : Space d)) = (k • v) +ᵥ (0 : Space d) := by
+  ext i
+  simp
+
+instance {d} : Module ℝ (Space d) where
+  one_smul x := by
+    ext i
+    simp
+  mul_smul a b x := by
+    ext i
+    simp only [smul_apply]
+    ring
+  smul_add a x y := by
+    ext i
+    simp only [smul_apply, add_apply]
+    ring
+  smul_zero a := by
+    ext i
+    simp
+  add_smul a b x := by
+    ext i
+    simp only [smul_apply, add_apply]
+    ring
+  zero_smul x := by
+    ext i
+    simp
+
+
+/-!
+
+## A.3. Instance of an inner product space
+
+-/
+
+noncomputable instance {d} : Norm (Space d) where
+  norm p := √ (∑ i, (p i)^2)
+
+lemma norm_eq {d} (p : Space d) : ‖p‖ = √ (∑ i, (p i) ^ 2) := by
+  rfl
+
+@[simp]
+lemma abs_eval_le_norm {d} (p : Space d) (i : Fin d) :
+    |p i| ≤ ‖p‖ := by
+  simp [norm_eq]
+  refine Real.abs_le_sqrt ?_
+  trans ∑ j ∈ {i}, (p j) ^ 2
+  · simp
+  refine Finset.sum_le_univ_sum_of_nonneg (fun i => by positivity)
+
+lemma norm_sq_eq {d} (p : Space d) :
+    ‖p‖ ^ 2 = ∑ i, (p i) ^ 2 := by
+  rw [norm_eq]
+  refine Real.sq_sqrt ?_
+  positivity
+
+lemma point_dim_zero_eq (p : Space 0) : p = 0 := by
+  ext i
+  fin_cases i
+
+@[simp]
+lemma norm_vadd_zero {d} (v : EuclideanSpace ℝ (Fin d)) :
+    ‖v +ᵥ (0 : Space d)‖ = ‖v‖ := by
+  simp [norm_eq, PiLp.norm_eq_of_L2]
+
+instance : Neg (Space d) where
+  neg p := ⟨fun i => - (p.val i)⟩
+
+@[simp]
+lemma neg_val {d : ℕ} (p : Space d) :
+    (-p).val = fun i => - (p.val i) := rfl
+
+@[simp]
+lemma neg_apply {d : ℕ} (p : Space d) (i : Fin d) :
+    (-p) i = - (p i) := by rfl
+
+noncomputable instance {d} : AddCommGroup (Space d) where
+  zsmul z p := ⟨fun i => z * p.val i⟩
+  neg_add_cancel p := by
+    ext i
+    simp
+  zsmul_zero' p := by
+    ext i
+    simp
+  zsmul_succ' n p := by
+    ext i
+    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, Int.cast_add, Int.cast_natCast,
+      Int.cast_one, add_apply]
+    ring
+  zsmul_neg' n p := by
+    ext i
+    simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, Nat.succ_eq_add_one,
+      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_apply]
+    ring
+
+@[simp]
+lemma sub_apply {d} (p q : Space d) (i : Fin d) :
+    (p - q) i = p i - q i := by
+  simp [sub_eq_add_neg, neg_apply, add_apply]
+
+@[simp]
+lemma sub_val {d} (p q : Space d) :
+    (p - q).val = fun i => p.val i - q.val i := by rfl
+
+@[simp]
+lemma vadd_zero_sub_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
+    (v1 +ᵥ (0 : Space d)) - (v2 +ᵥ (0 : Space d)) = (v1 - v2) +ᵥ (0 : Space d) := by
+  ext i
+  simp [sub_apply, vadd_apply]
+
+noncomputable instance {d} : SeminormedAddCommGroup (Space d) where
+
+@[simp]
+lemma dist_eq_norm {d} (p q : Space d) :
+    dist p q = ‖p - q‖ := rfl
+
+noncomputable instance : NormedAddCommGroup (Space d) where
+
+
+instance {d} : Inner ℝ (Space d) where
+  inner p q := ∑ i, p i * q i
+
+@[simp]
+lemma inner_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
+    inner ℝ (v1 +ᵥ (0 : Space d)) (v2 +ᵥ (0 : Space d)) = Inner.inner ℝ v1 v2 := by
+  simp [inner, vadd_apply]
+  apply Finset.sum_congr rfl
+  intro i hi
+  ring
+
+lemma inner_apply {d} (p q : Space d) :
+    inner ℝ p q = ∑ i, p i * q i := by rfl
+
+instance {d} : InnerProductSpace ℝ (Space d) where
+  norm_smul_le a x := by
+    obtain ⟨v, rfl⟩ := eq_vadd_zero x
+    simp only [smul_vadd_zero, norm_vadd_zero, Real.norm_eq_abs]
+    exact norm_smul_le a v
+  norm_sq_eq_re_inner x := by
+    obtain ⟨v, rfl⟩ := eq_vadd_zero x
+    simp
+  conj_inner_symm x y := by
+    simp [inner_apply]
+    congr
+    funext i
+    ring
+  add_left x y z := by
+    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
+    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
+    obtain ⟨v3, rfl⟩ := eq_vadd_zero z
+    simp only [add_vadd_zero, inner_vadd_zero]
+    exact InnerProductSpace.add_left v1 v2 v3
+  smul_left x y a := by
+    obtain ⟨v1, rfl⟩ := eq_vadd_zero x
+    obtain ⟨v2, rfl⟩ := eq_vadd_zero y
+    simp only [smul_vadd_zero, inner_vadd_zero, conj_trivial]
+    exact InnerProductSpace.smul_left v1 v2 a
+
+/-!
+
+## A.4. Instance of a measurable space
+
+-/
+
+instance {d : ℕ} : MeasurableSpace (Space d) := borel (Space d)
+
+instance {d : ℕ} : BorelSpace (Space d) where
+  measurable_eq := by rfl
+
+TODO "HB6YZ" "In the above documentation describe what an instance is, and why
+  it is useful to have instances for `Space d`."
+
+TODO "HB6WN" "After TODO 'HB6VC', give `Space d` the necessary instances
+  using `inferInstanceAs`."
+/-!
+
+## The norm on `Space`
+
+-/
+
+/-!
+
+## Inner product
+
+-/
+
+lemma inner_eq_sum {d} (p q : Space d) :
+    inner ℝ p q = ∑ i, p i * q i := by
+  simp [inner]
+
+@[simp]
+lemma sum_apply {ι : Type} [Fintype ι] (f : ι → Space d) (i : Fin d) :
+    (∑ x, f x) i = ∑ x, f x i := by
+  let P (ι : Type) [Fintype ι] : Prop := ∀ (f : ι → Space d) (i : Fin d), (∑ x, f x) i = ∑ x, f x i
+  have h1 : P ι := by
+    apply Fintype.induction_empty_option
+    · intro α β h e h f i
+      rw [← @e.sum_comp _, h, ← @e.sum_comp _]
+    · simp [P]
+    · intro α _ h f i
+      simp only [Fintype.sum_option, add_apply, add_right_inj]
+      rw [h]
+  exact h1 f i
+
+/-!
+
+## Basis
+
+-/
+
+TODO "HB6Z4" "In the above documentation describe the notion of a basis
+  in Lean."
+
+/-- The standard basis of Space based on `Fin d`. -/
+noncomputable def basis {d} : OrthonormalBasis (Fin d) ℝ (Space d) where
+  repr := {
+    toFun p := WithLp.toLp 2 fun i => p i
+    invFun := fun v => ⟨v⟩
+    left_inv := by
+      intro p
+      rfl
+    right_inv := by
+      intro v
+      rfl
+    map_add' := by
+      intro v1 v2
+      rfl
+    map_smul' := by
+      intro c v
+      rfl
+    norm_map' := by
+      intro x
+      simp [norm_eq, PiLp.norm_eq_of_L2]}
+
+lemma apply_eq_basis_repr_apply {d} (p : Space d) (i : Fin d) :
+    p i = basis.repr p i := by
+  simp [basis]
+
+@[simp]
+lemma basis_repr_apply {d} (p : Space d) (i : Fin d) :
+    basis.repr p i = p i := by
+  simp [apply_eq_basis_repr_apply]
+
+@[simp]
+lemma basis_repr_symm_apply {d} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) :
+    basis.repr.symm v i = v i := by rfl
+
+lemma basis_apply {d} (i j : Fin d) :
+    basis i j = if i = j then 1 else 0 := by
+  simp [apply_eq_basis_repr_apply]
+  congr 1
+  exact Lean.Grind.eq_congr' rfl rfl
+
+@[simp]
+lemma basis_self {d} (i : Fin d) : basis i i = 1 := by
+  simp [basis_apply]
+
+@[simp high]
+lemma inner_basis {d} (p : Space d) (i : Fin d) :
+    inner ℝ p (basis i) = p i := by
+  simp [inner_eq_sum, basis_apply]
+
+@[simp high]
+lemma basis_inner {d} (i : Fin d) (p : Space d) :
+    inner ℝ (basis i) p = p i := by
+  simp [inner_eq_sum, basis_apply]
+
+open InnerProductSpace
+
+lemma basis_repr_inner_eq {d} (p : Space d) (v : EuclideanSpace ℝ (Fin d)) :
+    ⟪basis.repr p, v⟫_ℝ = ⟪p, basis.repr.symm v⟫_ℝ := by
+  exact LinearIsometryEquiv.inner_map_eq_flip basis.repr p v
+
+instance {d : ℕ} : FiniteDimensional ℝ (Space d) :=
+  Module.Basis.finiteDimensional_of_finite (h := basis.toBasis)
+
+@[simp]
+lemma finrank_eq_dim {d : ℕ} : Module.finrank ℝ (Space d) = d := by
+  simp [Module.finrank_eq_nat_card_basis (basis.toBasis)]
+
+@[simp]
+lemma rank_eq_dim {d : ℕ} : Module.rank ℝ (Space d) = d := by
+  simp [rank_eq_card_basis (basis.toBasis)]
+
+@[simp]
+lemma fderiv_basis_repr {d} (p : Space d) :
+    fderiv ℝ basis.repr p = basis.repr.toContinuousLinearMap := by
+  change fderiv ℝ basis.repr.toContinuousLinearMap p = _
+  rw [ContinuousLinearMap.fderiv]
+
+@[simp]
+lemma fderiv_basis_repr_symm {d} (v : EuclideanSpace ℝ (Fin d)) :
+    fderiv ℝ basis.repr.symm v = basis.repr.symm.toContinuousLinearMap := by
+  change fderiv ℝ basis.repr.symm.toContinuousLinearMap v = _
+  rw [ContinuousLinearMap.fderiv]
+
+/-!
+
+## Coordinates
+
+-/
+
+/-- The standard coordinate functions of Space based on `Fin d`.
+
+The notation `𝔁 μ p` can be used for this. -/
+noncomputable def coord (μ : Fin d) (p : Space d) : ℝ :=
+  inner ℝ p (basis μ)
+
+lemma coord_apply (μ : Fin d) (p : Space d) :
+    coord μ p = p μ := by
+  simp [coord]
+
+/-- The standard coordinate functions of Space based on `Fin d`, as a continuous linear map. -/
+noncomputable def coordCLM {d} (μ : Fin d) : Space d →L[ℝ] ℝ where
+  toFun := coord μ
+  map_add' := fun p q => by
+    simp [coord, basis, inner_add_left]
+  map_smul' := fun c p => by
+    simp [coord, basis, inner_smul_left]
+  cont := by
+    unfold coord
+    fun_prop
+
+open ContDiff
+
+@[fun_prop]
+lemma coord_contDiff {i} : ContDiff ℝ ∞ (fun x : Space d => x.coord i) := by
+  change ContDiff ℝ ∞ (coordCLM i)
+  fun_prop
+
+lemma coordCLM_apply (μ : Fin d) (p : Space d) :
+    coordCLM μ p = coord μ p := by
+  rfl
+
+@[inherit_doc coord]
+scoped notation "𝔁" => coord
+
+@[fun_prop]
+lemma eval_continuous {d} (i : Fin d) :
+    Continuous (fun p : Space d => p i) := by
+  convert (coordCLM i).continuous
+  simp [coordCLM_apply, coord]
+
+@[fun_prop]
+lemma eval_differentiable {d} (i : Fin d) :
+    Differentiable ℝ (fun p : Space d => p i) := by
+  convert (coordCLM i).differentiable
+  simp [coordCLM_apply, coord]
+
+@[fun_prop]
+lemma eval_contDiff {d n} (i : Fin d) :
+    ContDiff ℝ n (fun p : Space d => p i) := by
+  convert (coordCLM i).contDiff
+  simp [coordCLM_apply, coord]
+
+/-- The continuous linear equivalence between `Space d` and the corresponding `Pi` type. -/
+def equivPi (d : ℕ) :
+    Space d ≃L[ℝ] Π (_ : Fin d), ℝ := LinearEquiv.toContinuousLinearEquiv <|
+  {
+    toFun := fun p i => p i
+    map_add' p1 p2 := by funext i; simp
+    map_smul' p r := by funext i; simp
+    invFun := fun f => ⟨f⟩
+  }
+
+@[fun_prop]
+lemma mk_continuous {d : ℕ} :
+    Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous
+
+@[fun_prop]
+lemma mk_differentiable {d : ℕ} :
+    Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable
+
+@[fun_prop]
+lemma mk_contDiff {d n : ℕ} :
+    ContDiff ℝ n (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.contDiff
+
+@[simp]
+lemma fderiv_mk {d : ℕ} (f : Fin d → ℝ) :
+    fderiv ℝ Space.mk f = (equivPi d).symm := by
+  change fderiv ℝ (equivPi d).symm f = _
+  rw [@ContinuousLinearEquiv.fderiv]
+
+@[simp]
+lemma fderiv_val {d : ℕ} (p : Space d) :
+    fderiv ℝ Space.val p = (equivPi d) := by
+  change fderiv ℝ (equivPi d) p = _
+  rw [@ContinuousLinearEquiv.fderiv]
+
+/-!
+
+## Directions
+
+-/
+
+/-- Notion of direction where `unit` returns a unit vector in the direction specified. -/
+structure Direction (d : ℕ := 3) where
+  /-- Unit vector specifying the direction. -/
+  unit : Space d
+  norm : ‖unit‖ = 1
+
+/-- Direction of a `Space` value with respect to the origin. -/
+noncomputable def toDirection {d : ℕ} (x : Space d) (h : x ≠ 0) : Direction d where
+  unit := (‖x‖⁻¹) • x
+  norm := norm_smul_inv_norm h
+
+@[simp]
+lemma direction_unit_sq_sum {d} (s : Direction d) :
+    ∑ i : Fin d, (s.unit i) ^ 2 = 1 := by
+  trans (‖s.unit‖) ^ 2
+  · rw [norm_sq_eq]
+  · rw [s.norm]
+    simp
+
+/-!
+
+## One equiv
+
+-/
+
+/-- The linear isometric equivalence between `Space 1` and `ℝ`. -/
+noncomputable def oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ where
+  toFun x := x 0
+  invFun x := ⟨fun _ => x⟩
+  left_inv x := by
+    ext i; fin_cases i; simp
+  right_inv x := by simp
+  map_add' x y := by rfl
+  map_smul' c x := by rfl
+  norm_map' x := by
+    simp only [Fin.isValue, LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, Real.norm_eq_abs]
+    rw [norm_eq]
+    simp only [Fin.isValue, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton]
+    exact Eq.symm (Real.sqrt_sq_eq_abs (x 0))
+
+lemma oneEquiv_coe :
+    (oneEquiv : Space 1 → ℝ) = fun x => x 0 := by
+  rfl
+
+lemma oneEquiv_symm_coe :
+    (oneEquiv.symm : ℝ → Space 1) = (fun x => ⟨fun _ => x⟩) := by
+  rfl
+
+lemma oneEquiv_symm_apply (x : ℝ) (i : Fin 1) :
+    oneEquiv.symm x i = x := by
+  fin_cases i
+  rfl
+
+lemma oneEquiv_continuous :
+    Continuous (oneEquiv : Space 1 → ℝ) := by
+  simp [oneEquiv_coe]
+  fun_prop
+
+lemma oneEquiv_symm_continuous :
+    Continuous (oneEquiv.symm : ℝ → Space 1) := by
+  simp [oneEquiv_symm_coe]
+  fun_prop
+
+/-- The continuous linear equivalence between `Space 1` and `ℝ`. -/
+noncomputable def oneEquivCLE : Space 1 ≃L[ℝ] ℝ where
+  toLinearEquiv := oneEquiv
+  continuous_toFun := by
+    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_coe]
+    erw [oneEquiv_coe]
+    fun_prop
+  continuous_invFun := by
+    simp only [LinearEquiv.invFun_eq_symm]
+    erw [oneEquiv_symm_coe]
+    fun_prop
+
+open MeasureTheory
+lemma oneEquiv_measurableEmbedding : MeasurableEmbedding oneEquiv where
+  injective := oneEquiv.injective
+  measurable := by fun_prop
+  measurableSet_image' := by
+    intro s hs
+    change MeasurableSet (⇑oneEquivCLE '' s)
+    rw [ContinuousLinearEquiv.image_eq_preimage_symm]
+    exact oneEquiv.symm.continuous.measurable hs
+
+lemma oneEquiv_symm_measurableEmbedding : MeasurableEmbedding oneEquiv.symm where
+  injective := oneEquiv.symm.injective
+  measurable := by fun_prop
+  measurableSet_image' := by
+    intro s hs
+    change MeasurableSet (⇑oneEquivCLE.symm '' s)
+    rw [ContinuousLinearEquiv.image_eq_preimage_symm]
+    exact oneEquiv.continuous.measurable hs
+
+lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
+  LinearIsometryEquiv.measurePreserving oneEquiv
+
+lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
+  exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
+
+end Space

From a8da78242f93cca6f4ba094f46006ba73daed987 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 5 Mar 2026 10:13:05 +0000
Subject: [PATCH 4/6] refactor: Fix spelling

---
 PhysLean/SpaceAndTime/Space/Module.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index c5286bee1..472d178cb 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import PhysLean.SpaceAndTime.Space.Basic
 /-!
 
-# The strucutre of a module on Space
+# The structure of a module on Space
 
 The scope of this module is to define on `Space d` the structure of a `Module`
 (aka vector space), a `Norm` and an `InnerProductSpace`, and give properties of these structures.

From 2a4c47b0c2f42989cb7ec0686b0c5852fbcb908f Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 6 Mar 2026 08:35:10 +0000
Subject: [PATCH 5/6] feat: Fix def-eq abuse

Thanks to @YanYablonovskiy for pointing this out.
---
 PhysLean/SpaceAndTime/Space/Basic.lean | 35 +++++++++++++++-----------
 1 file changed, 20 insertions(+), 15 deletions(-)

diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index ee3c70231..e8d50b83a 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -134,18 +134,11 @@ lemma eq_of_apply {d} {p q : Space d}
 
 -/
 
-instance {d} : Nonempty (Space d) := Nonempty.intro ⟨fun _ => 0⟩
+instance {d} : Nonempty (Space d) := Nonempty.intro
+  ⟨fun _ => Classical.choice instNonemptyOfInhabited⟩
 
-instance {d : ℕ} : Nontrivial (Space d.succ) := by
-  refine { exists_pair_ne := ?_ }
-  use ⟨fun _ => 0⟩, ⟨fun _ => 1⟩
-  simp only [Nat.succ_eq_add_one, ne_eq, mk.injEq]
-  refine Function.ne_iff.mpr ⟨0, ?_⟩
-  simp
-
-instance : Subsingleton (Space 0) := Subsingleton.intro <| fun x y => by
-  ext i
-  fin_cases i
+instance : Subsingleton (Space 0) := Subsingleton.intro <| fun _ _ =>
+   eq_of_apply <| fun i => Fin.elim0 i
 
 /-!
 
@@ -217,8 +210,7 @@ noncomputable instance {d} : AddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) wh
 noncomputable instance {d} : Dist (Space d) where
   dist p q := √ (∑ i, (p i - q i) ^ 2)
 
-lemma dist_eq {d} (p q : Space d) :
-    dist p q = √ (∑ i, (p i - q i) ^ 2) := rfl
+lemma dist_eq {d} (p q : Space d) : dist p q = √ (∑ i, (p i - q i) ^ 2) := rfl
 
 noncomputable instance {d} : PseudoMetricSpace (Space d) where
   dist_self x := by simp [dist_eq]
@@ -227,7 +219,7 @@ noncomputable instance {d} : PseudoMetricSpace (Space d) where
     convert dist_triangle (WithLp.toLp 2 fun i => x i) (WithLp.toLp 2 fun i => y i)
       (WithLp.toLp 2 fun i => z i)
     all_goals
-    · rw [EuclideanSpace.dist_eq]
+      rw [EuclideanSpace.dist_eq]
       simp only [dist, sq_abs]
 
 /-!
@@ -236,7 +228,7 @@ noncomputable instance {d} : PseudoMetricSpace (Space d) where
 
 -/
 
-noncomputable instance : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
+noncomputable instance {d} : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d) where
   dist_eq_norm' p q := by simp [dist, EuclideanSpace.norm_eq]
 
 /-!
@@ -248,4 +240,17 @@ noncomputable instance : NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d)
 noncomputable instance {d} : MetricSpace (Space d) where
   eq_of_dist_eq_zero {p q} := by simp [NormedAddTorsor.dist_eq_norm']
 
+/-!
+
+## B.7. Non-trivality
+
+-/
+
+instance {d : ℕ} : Nontrivial (Space d.succ) where
+  exists_pair_ne := by
+    obtain k := Classical.choice Space.instNonempty
+    obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d.succ))
+    use k, v1 +ᵥ k
+    simpa only [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm
+
 end Space

From 8f236b2d3ae9399af2f78f2d12b876a0ea02357c Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 6 Mar 2026 09:03:31 +0000
Subject: [PATCH 6/6] feat: Add structure of manifold

---
 PhysLean/SpaceAndTime/Space/Basic.lean | 31 ++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index e8d50b83a..01c396911 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -253,4 +253,35 @@ instance {d : ℕ} : Nontrivial (Space d.succ) where
     use k, v1 +ᵥ k
     simpa only [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm
 
+/-!
+
+## C. Model structure (i.e. structure of a manifold)
+
+-/
+
+/-- The manifold structure on `Space d`. -/
+noncomputable def manifoldStructure (d : ℕ) :
+    ModelWithCorners ℝ (EuclideanSpace ℝ (Fin d)) (Space d) where
+  toFun := (Equiv.vaddConst (Classical.choice Space.instNonempty)).symm
+  invFun := Equiv.vaddConst (Classical.choice Space.instNonempty)
+  source := Set.univ
+  target := Set.univ
+  map_source' := by simp
+  map_target' := by simp
+  left_inv' := by simp
+  right_inv' := by simp
+  source_eq := by simp
+  convex_range' := by
+    rw [dif_pos (instIsRCLikeNormedField ℝ), Equiv.range_eq_univ]
+    exact fun _ _ _ ↦ by simp
+  nonempty_interior' := by
+    rw [Equiv.range_eq_univ]
+    simp
+  continuous_toFun := by
+    simp only [Equiv.coe_vaddConst_symm]
+    fun_prop
+  continuous_invFun := by
+    simp only [Equiv.coe_vaddConst]
+    fun_prop
+
 end Space