From 2459d57b39ad6dd436d543df12ca6563792689a1 Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Wed, 1 Apr 2026 18:11:43 +0200
Subject: [PATCH 1/3] Add MultiIndex API for local field-theory foundations

---
 Physlib.lean                                  |   1 +
 .../DataStructures/MultiIndex.lean            | 114 ++++++++++++++++++
 2 files changed, 115 insertions(+)
 create mode 100644 Physlib/Mathematics/DataStructures/MultiIndex.lean

diff --git a/Physlib.lean b/Physlib.lean
index 750da9136..a98e06f3d 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -51,6 +51,7 @@ public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
 public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
+public import Physlib.Mathematics.DataStructures.MultiIndex
 public import Physlib.Mathematics.Distribution.Basic
 public import Physlib.Mathematics.Distribution.PowMul
 public import Physlib.Mathematics.FDerivCurry
diff --git a/Physlib/Mathematics/DataStructures/MultiIndex.lean b/Physlib/Mathematics/DataStructures/MultiIndex.lean
new file mode 100644
index 000000000..06401aaa5
--- /dev/null
+++ b/Physlib/Mathematics/DataStructures/MultiIndex.lean
@@ -0,0 +1,114 @@
+ /-
+ Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Authors: Juan Jose Fernandez Morales
+ -/
+ 
+ module
+ 
+ public import Mathlib.Algebra.BigOperators.Pi
+ /-!
+ # Multi-indices
+ 
+ ## i. Overview
+ 
+ This module defines the basic type of multi-indices used to index iterated partial derivatives.
+ 
+ The implementation is intentionally minimal. A multi-index on `n` source coordinates is represented
+ as a function `Fin n → Nat`, together with the first basic operations needed later in the local
+ Classical Field Theory development.
+ 
+ ## ii. Key results
+ 
+ - `Physlib.MultiIndex` : multi-indices on `n` coordinates.
+ - `MultiIndex.order` : the order `|I|` of a multi-index.
+ - `MultiIndex.increment` : increment a single coordinate of a multi-index.
+ 
+ ## iii. Table of contents
+ 
+ - A. The basic type of multi-indices
+   - A.1. Basic operations
+   - A.2. Basic lemmas
+ 
+ ## iv. References
+ 
+ -/
+ 
+ @[expose] public section
+ 
+ open scoped BigOperators
+ 
+ namespace Physlib
+ 
+ /-!
+ ## A. The basic type of multi-indices
+ 
+ -/
+ 
+ /-- A multi-index on `n` source coordinates. -/
+ abbrev MultiIndex (n : ℕ) := Fin n → ℕ
+ 
+ namespace MultiIndex
+ 
+ variable {n : ℕ}
+ 
+ instance : DecidableEq (MultiIndex n) := inferInstance
+ 
+ /-!
+ ### A.1. Basic operations
+ 
+ -/
+ 
+ /-- The order `|I|` of a multi-index `I`, defined as the sum of its components. -/
+ def order (I : MultiIndex n) : Nat := ∑ i, I i
+ 
+ /-- Increment the `i`-th coordinate of a multi-index by one. -/
+ def increment (I : MultiIndex n) (i : Fin n) : MultiIndex n := I + Pi.single i 1
+ 
+ /-!
+ ### A.2. Basic lemmas
+ 
+ -/
+ 
+ @[ext]
+ lemma ext {I J : MultiIndex n} (h : ∀ i, I i = J i) : I = J := funext h
+ 
+ @[simp]
+ lemma zero_apply (i : Fin n) : (0 : MultiIndex n) i = 0 := rfl
+ 
+ @[simp]
+ lemma increment_apply_same (I : MultiIndex n) (i : Fin n) :
+     increment I i i = I i + 1 := by
+   simp [increment]
+ 
+ @[simp]
+ lemma increment_apply_ne (I : MultiIndex n) {i j : Fin n} (h : j ≠ i) :
+     increment I i j = I j := by
+   simp [increment, Pi.single_eq_of_ne h]
+ 
+ @[simp]
+ lemma order_zero : order (0 : MultiIndex n) = 0 := by
+   simp [order]
+ 
+ lemma order_add (I J : MultiIndex n) : order (I + J) = order I + order J := by
+   simp [order, Finset.sum_add_distrib]
+ 
+ @[simp]
+ lemma order_single (i : Fin n) : order (Pi.single i 1 : MultiIndex n) = 1 := by
+   classical
+   unfold order
+   rw [Finset.sum_eq_single i]
+   · simp
+   · intro j _ hj
+     simp [Pi.single_eq_of_ne hj]
+   · intro hi
+     simp at hi
+ 
+ @[simp]
+ lemma order_increment (I : MultiIndex n) (i : Fin n) :
+     order (increment I i) = order I + 1 := by
+   rw [increment, order_add, order_single]
+ 
+ end MultiIndex
+ 
+ end Physlib

From 5e2d9865f01ee2861fd347910f58c39666c97d0d Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Sat, 4 Apr 2026 12:14:57 +0200
Subject: [PATCH 2/3] Rework MultiIndex as a structure under Space.Derivatives

---
 Physlib.lean                                  |   2 +-
 .../DataStructures/MultiIndex.lean            | 114 ---------------
 .../Space/Derivatives/MultiIndex.lean         | 131 ++++++++++++++++++
 3 files changed, 132 insertions(+), 115 deletions(-)
 delete mode 100644 Physlib/Mathematics/DataStructures/MultiIndex.lean
 create mode 100644 Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean

diff --git a/Physlib.lean b/Physlib.lean
index a98e06f3d..616caa334 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -51,7 +51,6 @@ public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
 public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
-public import Physlib.Mathematics.DataStructures.MultiIndex
 public import Physlib.Mathematics.Distribution.Basic
 public import Physlib.Mathematics.Distribution.PowMul
 public import Physlib.Mathematics.FDerivCurry
@@ -351,6 +350,7 @@ public import Physlib.SpaceAndTime.Space.Derivatives.Curl
 public import Physlib.SpaceAndTime.Space.Derivatives.Div
 public import Physlib.SpaceAndTime.Space.Derivatives.Grad
 public import Physlib.SpaceAndTime.Space.Derivatives.Laplacian
+public import Physlib.SpaceAndTime.Space.Derivatives.MultiIndex
 public import Physlib.SpaceAndTime.Space.DistConst
 public import Physlib.SpaceAndTime.Space.DistOfFunction
 public import Physlib.SpaceAndTime.Space.Integrals.Basic
diff --git a/Physlib/Mathematics/DataStructures/MultiIndex.lean b/Physlib/Mathematics/DataStructures/MultiIndex.lean
deleted file mode 100644
index 06401aaa5..000000000
--- a/Physlib/Mathematics/DataStructures/MultiIndex.lean
+++ /dev/null
@@ -1,114 +0,0 @@
- /-
- Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
- Released under Apache 2.0 license as described in the file LICENSE.
- Authors: Juan Jose Fernandez Morales
- -/
- 
- module
- 
- public import Mathlib.Algebra.BigOperators.Pi
- /-!
- # Multi-indices
- 
- ## i. Overview
- 
- This module defines the basic type of multi-indices used to index iterated partial derivatives.
- 
- The implementation is intentionally minimal. A multi-index on `n` source coordinates is represented
- as a function `Fin n → Nat`, together with the first basic operations needed later in the local
- Classical Field Theory development.
- 
- ## ii. Key results
- 
- - `Physlib.MultiIndex` : multi-indices on `n` coordinates.
- - `MultiIndex.order` : the order `|I|` of a multi-index.
- - `MultiIndex.increment` : increment a single coordinate of a multi-index.
- 
- ## iii. Table of contents
- 
- - A. The basic type of multi-indices
-   - A.1. Basic operations
-   - A.2. Basic lemmas
- 
- ## iv. References
- 
- -/
- 
- @[expose] public section
- 
- open scoped BigOperators
- 
- namespace Physlib
- 
- /-!
- ## A. The basic type of multi-indices
- 
- -/
- 
- /-- A multi-index on `n` source coordinates. -/
- abbrev MultiIndex (n : ℕ) := Fin n → ℕ
- 
- namespace MultiIndex
- 
- variable {n : ℕ}
- 
- instance : DecidableEq (MultiIndex n) := inferInstance
- 
- /-!
- ### A.1. Basic operations
- 
- -/
- 
- /-- The order `|I|` of a multi-index `I`, defined as the sum of its components. -/
- def order (I : MultiIndex n) : Nat := ∑ i, I i
- 
- /-- Increment the `i`-th coordinate of a multi-index by one. -/
- def increment (I : MultiIndex n) (i : Fin n) : MultiIndex n := I + Pi.single i 1
- 
- /-!
- ### A.2. Basic lemmas
- 
- -/
- 
- @[ext]
- lemma ext {I J : MultiIndex n} (h : ∀ i, I i = J i) : I = J := funext h
- 
- @[simp]
- lemma zero_apply (i : Fin n) : (0 : MultiIndex n) i = 0 := rfl
- 
- @[simp]
- lemma increment_apply_same (I : MultiIndex n) (i : Fin n) :
-     increment I i i = I i + 1 := by
-   simp [increment]
- 
- @[simp]
- lemma increment_apply_ne (I : MultiIndex n) {i j : Fin n} (h : j ≠ i) :
-     increment I i j = I j := by
-   simp [increment, Pi.single_eq_of_ne h]
- 
- @[simp]
- lemma order_zero : order (0 : MultiIndex n) = 0 := by
-   simp [order]
- 
- lemma order_add (I J : MultiIndex n) : order (I + J) = order I + order J := by
-   simp [order, Finset.sum_add_distrib]
- 
- @[simp]
- lemma order_single (i : Fin n) : order (Pi.single i 1 : MultiIndex n) = 1 := by
-   classical
-   unfold order
-   rw [Finset.sum_eq_single i]
-   · simp
-   · intro j _ hj
-     simp [Pi.single_eq_of_ne hj]
-   · intro hi
-     simp at hi
- 
- @[simp]
- lemma order_increment (I : MultiIndex n) (i : Fin n) :
-     order (increment I i) = order I + 1 := by
-   rw [increment, order_add, order_single]
- 
- end MultiIndex
- 
- end Physlib
diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
new file mode 100644
index 000000000..3d46e9a9a
--- /dev/null
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Juan Jose Fernandez Morales
+-/
+
+module
+
+public import Mathlib.Algebra.BigOperators.Pi
+
+/-!
+# Multi-indices
+
+## i. Overview
+
+This module defines the basic type of multi-indices used to index iterated partial derivatives.
+
+A multi-index on `n` source coordinates is represented as a structure with an underlying function
+`Fin n → ℕ`, together with the first basic operations needed later in the local Classical Field
+Theory development.
+
+## ii. Key results
+
+- `Physlib.MultiIndex` : multi-indices on `n` coordinates.
+- `MultiIndex.order` : the order `|I|` of a multi-index.
+- `MultiIndex.increment` : increment a single coordinate of a multi-index.
+
+## iii. Table of contents
+
+- A. The basic type of multi-indices
+  - A.1. Basic operations
+  - A.2. Basic lemmas
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+open scoped BigOperators
+
+namespace Physlib
+
+/-!
+## A. The basic type of multi-indices
+
+-/
+
+/-- A multi-index on `n` source coordinates. -/
+structure MultiIndex (n : ℕ) where
+  /-- The coordinates of the multi-index. -/
+  toFun : Fin n → ℕ
+deriving DecidableEq
+
+namespace MultiIndex
+
+variable {n : ℕ}
+
+instance : CoeFun (MultiIndex n) (fun _ => Fin n → ℕ) := ⟨MultiIndex.toFun⟩
+
+instance : Zero (MultiIndex n) := ⟨⟨0⟩⟩
+
+instance : Add (MultiIndex n) := ⟨fun I J => ⟨I.toFun + J.toFun⟩⟩
+
+/-!
+### A.1. Basic operations
+
+-/
+
+/-- The order `|I|` of a multi-index `I`, defined as the sum of its components. -/
+def order (I : MultiIndex n) : Nat := ∑ i, I i
+
+/-- Increment the `i`-th coordinate of a multi-index by one. -/
+def increment (I : MultiIndex n) (i : Fin n) : MultiIndex n := ⟨I.toFun + Pi.single i 1⟩
+
+/-!
+### A.2. Basic lemmas
+
+-/
+
+@[ext]
+lemma ext {I J : MultiIndex n} (h : ∀ i, I i = J i) : I = J := by
+  cases I
+  cases J
+  simp only at h
+  congr
+  funext i
+  exact h i
+
+@[simp]
+lemma zero_apply (i : Fin n) : (0 : MultiIndex n) i = 0 := rfl
+
+@[simp]
+lemma add_apply (I J : MultiIndex n) (i : Fin n) : (I + J) i = I i + J i := rfl
+
+@[simp]
+lemma increment_apply_same (I : MultiIndex n) (i : Fin n) :
+    increment I i i = I i + 1 := by
+  simp [increment]
+
+@[simp]
+lemma increment_apply_ne (I : MultiIndex n) {i j : Fin n} (h : j ≠ i) :
+    increment I i j = I j := by
+  simp [increment, Pi.single_eq_of_ne h]
+
+@[simp]
+lemma order_zero : order (0 : MultiIndex n) = 0 := by
+  simp [order]
+
+lemma order_add (I J : MultiIndex n) : order (I + J) = order I + order J := by
+  simp [order, Finset.sum_add_distrib]
+
+@[simp]
+lemma order_single (i : Fin n) : order (⟨Pi.single i 1⟩ : MultiIndex n) = 1 := by
+  classical
+  unfold order
+  rw [Finset.sum_eq_single i]
+  · simp
+  · intro j _ hj
+    simp [Pi.single_eq_of_ne hj]
+  · intro hi
+    simp at hi
+
+@[simp]
+lemma order_increment (I : MultiIndex n) (i : Fin n) :
+    order (increment I i) = order I + 1 := by
+  simp [increment, order, Finset.sum_add_distrib]
+
+end MultiIndex
+
+end Physlib

From 777c9473ecd07e9b6d9cef982d62d5373ca03f20 Mon Sep 17 00:00:00 2001
From: juanjfndz <juanjfndz@gmail.com>
Date: Mon, 6 Apr 2026 14:52:45 +0200
Subject: [PATCH 3/3] Rename MultiIndex dimension parameter to d

---
 .../Space/Derivatives/MultiIndex.lean         | 42 +++++++++----------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
index 3d46e9a9a..f76657402 100644
--- a/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
+++ b/Physlib/SpaceAndTime/Space/Derivatives/MultiIndex.lean
@@ -15,13 +15,13 @@ public import Mathlib.Algebra.BigOperators.Pi
 
 This module defines the basic type of multi-indices used to index iterated partial derivatives.
 
-A multi-index on `n` source coordinates is represented as a structure with an underlying function
-`Fin n → ℕ`, together with the first basic operations needed later in the local Classical Field
+A multi-index on `d` source coordinates is represented as a structure with an underlying function
+`Fin d → ℕ`, together with the first basic operations needed later in the local Classical Field
 Theory development.
 
 ## ii. Key results
 
-- `Physlib.MultiIndex` : multi-indices on `n` coordinates.
+- `Physlib.MultiIndex` : multi-indices on `d` coordinates.
 - `MultiIndex.order` : the order `|I|` of a multi-index.
 - `MultiIndex.increment` : increment a single coordinate of a multi-index.
 
@@ -46,21 +46,21 @@ namespace Physlib
 
 -/
 
-/-- A multi-index on `n` source coordinates. -/
-structure MultiIndex (n : ℕ) where
+/-- A multi-index on `d` source coordinates. -/
+structure MultiIndex (d : ℕ) where
   /-- The coordinates of the multi-index. -/
-  toFun : Fin n → ℕ
+  toFun : Fin d → ℕ
 deriving DecidableEq
 
 namespace MultiIndex
 
-variable {n : ℕ}
+variable {d : ℕ}
 
-instance : CoeFun (MultiIndex n) (fun _ => Fin n → ℕ) := ⟨MultiIndex.toFun⟩
+instance : CoeFun (MultiIndex d) (fun _ => Fin d → ℕ) := ⟨MultiIndex.toFun⟩
 
-instance : Zero (MultiIndex n) := ⟨⟨0⟩⟩
+instance : Zero (MultiIndex d) := ⟨⟨0⟩⟩
 
-instance : Add (MultiIndex n) := ⟨fun I J => ⟨I.toFun + J.toFun⟩⟩
+instance : Add (MultiIndex d) := ⟨fun I J => ⟨I.toFun + J.toFun⟩⟩
 
 /-!
 ### A.1. Basic operations
@@ -68,10 +68,10 @@ instance : Add (MultiIndex n) := ⟨fun I J => ⟨I.toFun + J.toFun⟩⟩
 -/
 
 /-- The order `|I|` of a multi-index `I`, defined as the sum of its components. -/
-def order (I : MultiIndex n) : Nat := ∑ i, I i
+def order (I : MultiIndex d) : Nat := ∑ i, I i
 
 /-- Increment the `i`-th coordinate of a multi-index by one. -/
-def increment (I : MultiIndex n) (i : Fin n) : MultiIndex n := ⟨I.toFun + Pi.single i 1⟩
+def increment (I : MultiIndex d) (i : Fin d) : MultiIndex d := ⟨I.toFun + Pi.single i 1⟩
 
 /-!
 ### A.2. Basic lemmas
@@ -79,7 +79,7 @@ def increment (I : MultiIndex n) (i : Fin n) : MultiIndex n := ⟨I.toFun + Pi.s
 -/
 
 @[ext]
-lemma ext {I J : MultiIndex n} (h : ∀ i, I i = J i) : I = J := by
+lemma ext {I J : MultiIndex d} (h : ∀ i, I i = J i) : I = J := by
   cases I
   cases J
   simp only at h
@@ -88,30 +88,30 @@ lemma ext {I J : MultiIndex n} (h : ∀ i, I i = J i) : I = J := by
   exact h i
 
 @[simp]
-lemma zero_apply (i : Fin n) : (0 : MultiIndex n) i = 0 := rfl
+lemma zero_apply (i : Fin d) : (0 : MultiIndex d) i = 0 := rfl
 
 @[simp]
-lemma add_apply (I J : MultiIndex n) (i : Fin n) : (I + J) i = I i + J i := rfl
+lemma add_apply (I J : MultiIndex d) (i : Fin d) : (I + J) i = I i + J i := rfl
 
 @[simp]
-lemma increment_apply_same (I : MultiIndex n) (i : Fin n) :
+lemma increment_apply_same (I : MultiIndex d) (i : Fin d) :
     increment I i i = I i + 1 := by
   simp [increment]
 
 @[simp]
-lemma increment_apply_ne (I : MultiIndex n) {i j : Fin n} (h : j ≠ i) :
+lemma increment_apply_ne (I : MultiIndex d) {i j : Fin d} (h : j ≠ i) :
     increment I i j = I j := by
   simp [increment, Pi.single_eq_of_ne h]
 
 @[simp]
-lemma order_zero : order (0 : MultiIndex n) = 0 := by
+lemma order_zero : order (0 : MultiIndex d) = 0 := by
   simp [order]
 
-lemma order_add (I J : MultiIndex n) : order (I + J) = order I + order J := by
+lemma order_add (I J : MultiIndex d) : order (I + J) = order I + order J := by
   simp [order, Finset.sum_add_distrib]
 
 @[simp]
-lemma order_single (i : Fin n) : order (⟨Pi.single i 1⟩ : MultiIndex n) = 1 := by
+lemma order_single (i : Fin d) : order (⟨Pi.single i 1⟩ : MultiIndex d) = 1 := by
   classical
   unfold order
   rw [Finset.sum_eq_single i]
@@ -122,7 +122,7 @@ lemma order_single (i : Fin n) : order (⟨Pi.single i 1⟩ : MultiIndex n) = 1
     simp at hi
 
 @[simp]
-lemma order_increment (I : MultiIndex n) (i : Fin n) :
+lemma order_increment (I : MultiIndex d) (i : Fin d) :
     order (increment I i) = order I + 1 := by
   simp [increment, order, Finset.sum_add_distrib]