diff --git a/.codespellignore b/.codespellignore
index 35ba186f6..0ea841340 100644
--- a/.codespellignore
+++ b/.codespellignore
@@ -9,3 +9,4 @@ Breal
 ket
 rIn
 FRO
+Commun
diff --git a/PhysLean/SpaceAndTime/Space/Basic.lean b/PhysLean/SpaceAndTime/Space/Basic.lean
index a5cf96d16..8cd12f8b6 100644
--- a/PhysLean/SpaceAndTime/Space/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Basic.lean
@@ -12,6 +12,7 @@ public import Mathlib.Topology.ContinuousMap.CompactlySupported
 public import Mathlib.Geometry.Manifold.IsManifold.Basic
 public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
 public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Geometry.Manifold.Diffeomorph
 /-!
 
 # Space
@@ -288,4 +289,34 @@ noncomputable def manifoldStructure (d : ℕ) :
     simp only [Equiv.coe_vaddConst]
     fun_prop
 
+@[simp]
+lemma manifoldStructure_comp_manifoldStructure_symm {d : ℕ} :
+    (↑(manifoldStructure d) ∘ ↑(manifoldStructure d).symm) = id := by
+  ext1 x
+  simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
+lemma manifoldStructure_comp_manifoldStructure_symm_apply {d : ℕ}
+    (x : EuclideanSpace ℝ (Fin d)) :
+    (manifoldStructure d) ((manifoldStructure d).symm x) = x := by
+  simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
+@[simp]
+lemma range_manifoldStructure {d : ℕ} :
+    (Set.range ↑(manifoldStructure d)) = Set.univ := by
+  ext x
+  simpa using ⟨(manifoldStructure d).symm x, manifoldStructure_comp_manifoldStructure_symm_apply x⟩
+
+open Manifold in
+lemma contMDiff_vaddConst (d : ℕ) : ContMDiff
+    (manifoldStructure d) (𝓘(ℝ, EuclideanSpace ℝ (Fin d)))  ⊤ (manifoldStructure d).toFun := by
+  rw [contMDiff_iff]
+  refine ⟨(manifoldStructure d).continuous_toFun, fun x y ↦ ?_⟩
+  simp only [extChartAt, OpenPartialHomeomorph.extend, OpenPartialHomeomorph.refl_partialEquiv,
+    PartialEquiv.refl_source, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq,
+    modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialEquiv.refl_coe,
+    ModelWithCorners.toPartialEquiv_coe, PartialEquiv.refl_trans,
+    ModelWithCorners.toPartialEquiv_coe_symm, manifoldStructure_comp_manifoldStructure_symm,
+    CompTriple.comp_eq, ModelWithCorners.target_eq, Set.preimage_univ, Set.inter_univ]
+  exact contDiffOn_id
+
 end Space
diff --git a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
index 2e042d293..6e09fdbdb 100644
--- a/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
+++ b/PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean
@@ -104,6 +104,45 @@ lemma deriv_eq_mfderiv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
   rw [deriv_eq_fderiv_basis, ← mfderiv_eq_fderiv]
   rfl
 
+open Manifold in
+lemma mdifferentiable_manifoldStructure_iff_differentiable {M d} [NormedAddCommGroup M]
+    [NormedSpace ℝ M] {f : Space d → M} {x : Space d} :
+    MDifferentiableAt (Space.manifoldStructure d) 𝓘(ℝ, M) f x ↔ DifferentiableAt ℝ f x := by
+  constructor
+  · intro h
+    rw [← mdifferentiableAt_iff_differentiableAt]
+    apply h.comp (I' := Space.manifoldStructure d)
+    exact (modelDiffeo.symm.mdifferentiable  (WithTop.top_ne_zero)).mdifferentiableAt
+  · intro h
+    apply (mdifferentiableAt_iff_differentiableAt.mpr h).comp (I' := 𝓘(ℝ, Space d))
+    exact (modelDiffeo.mdifferentiable  (WithTop.top_ne_zero)).mdifferentiableAt
+
+
+TODO "3XMN6" "Make the version of the derivative described through
+  `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the
+  equivalence with the current definition, under suitable conditions."
+
+open Manifold in
+/-- The spatial-derivative in terms of the derivative of functions between
+  manifolds with the manifold structure `Space.manifoldStructure d`. -/
+lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+    (μ : Fin d) (f : Space d → M) (x : Space d) :
+    deriv μ f x = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by
+  by_cases hf : DifferentiableAt ℝ f x
+  · rw [deriv_eq_mfderiv]
+    change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
+      (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
+    rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiableAt
+      (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]
+    simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
+      ContinuousLinearMap.coe_comp']
+    rw [basis_eq_mfderiv_modelDiffeo_single]
+    rfl
+  · rw [deriv_eq, fderiv_zero_of_not_differentiableAt hf,
+      mfderiv_zero_of_not_mdifferentiableAt <|
+      mdifferentiable_manifoldStructure_iff_differentiable.mp.mt hf]
+    simp
+
 /-!
 
 ### A.2. Derivative of the constant function
diff --git a/PhysLean/SpaceAndTime/Space/Module.lean b/PhysLean/SpaceAndTime/Space/Module.lean
index 545b568d0..f1457792e 100644
--- a/PhysLean/SpaceAndTime/Space/Module.lean
+++ b/PhysLean/SpaceAndTime/Space/Module.lean
@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 module
 
 public import PhysLean.SpaceAndTime.Space.Basic
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Analysis.Distribution.TemperateGrowth
 /-!
 
 # The structure of a module on Space
@@ -474,6 +476,12 @@ def equivPi (d : ℕ) :
     invFun := fun f => ⟨f⟩
   }
 
+/-!
+
+## Basic differentiablity conditions
+
+-/
+
 @[fun_prop]
 lemma mk_continuous {d : ℕ} :
     Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous
@@ -483,20 +491,54 @@ lemma mk_differentiable {d : ℕ} :
     Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable
 
 @[fun_prop]
-lemma mk_contDiff {d n : ℕ} :
+lemma mk_contDiff {d  : ℕ} {n : WithTop ℕ∞}:
     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]
+  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]
+  rw [ContinuousLinearEquiv.fderiv]
+
+@[fun_prop]
+lemma contDiffOn_vadd (s : Space d) :
+    ContDiffOn ℝ ω (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) Set.univ := by
+  rw [contDiffOn_univ]
+  refine fun_comp ?_ ?_
+  · exact mk_contDiff (n := ω)
+  · fun_prop
+
+@[fun_prop]
+lemma vadd_differentiable {d} (s : Space d) :
+    Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) :=
+  mk_differentiable.comp <| by fun_prop
+
+@[fun_prop]
+lemma contDiffOn_vsub (s1 : Space d) :
+    ContDiffOn ℝ ω (fun (s : Space d) => s -ᵥ s1) Set.univ :=
+  contDiffOn_univ.mpr <| fun_comp (PiLp.contDiff_toLp) (by fun_prop)
+
+@[fun_prop]
+lemma vsub_differentiable {d} (s1 : Space d) :
+    Differentiable ℝ (fun (s : Space d) => s -ᵥ s1) :=
+  (PiLp.contDiff_toLp.differentiable (NeZero.ne' 2).symm).comp (by fun_prop)
+
+lemma fderiv_space_components {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+    (μ : Fin d) (f : M → Space d) (hf : Differentiable ℝ f) (m dm : M):
+    fderiv ℝ f m dm μ  = fderiv ℝ (fun m' => f m' μ) m dm := by
+  trans fderiv ℝ (Space.coordCLM μ ∘ fun m' => f m') m dm
+  · rw [fderiv_comp _ (by fun_prop) (by fun_prop), ContinuousLinearMap.fderiv,
+      ContinuousLinearMap.coe_comp', Function.comp_apply]
+    simp [coordCLM, coord_apply]
+  · congr
+    ext i
+    simp [coordCLM, coord_apply]
 
 /-!
 
@@ -604,4 +646,104 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
 lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
   exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
 
+/-!
+
+## Relation to tangent space
+
+-/
+
+open Manifold in
+/-- A diffeomorphism between the two different manifold structures on `Space d`,
+  that equivalent to `manifoldStructure d` and that equivalent to `𝓘(ℝ, Space d)` -/
+noncomputable def modelDiffeo {d} :
+    Diffeomorph (manifoldStructure d) 𝓘(ℝ, Space d) (Space d) (Space d) ⊤ where
+  toFun p :=  p
+  invFun p :=  p
+  left_inv _ := rfl
+  right_inv _ := rfl
+  contMDiff_toFun := by
+    refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
+    simp [manifoldStructure]
+    fun_prop
+  contMDiff_invFun := by
+    refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
+    simp [manifoldStructure]
+    fun_prop
+
+@[simp]
+lemma modelDiffeo_apply (p : Space d) :
+    modelDiffeo p = p := rfl
+
+open Manifold in
+/-- The derivative of `modelDiffeo` provides an equivalence between
+  `Space d` and `EuclideanSpace ℝ (Fin d)`. This equivalences takes the basis
+  of `EuclideanSpace ℝ (Fin d)` to the basis of `Space d`, and vice versa. -/
+lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
+    basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
+      (EuclideanSpace.single μ 1) := by
+  simp [mfderiv]
+  rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
+  change _ = fderiv ℝ (manifoldStructure d).symm (manifoldStructure d x) (EuclideanSpace.single μ 1)
+  simp [manifoldStructure]
+  ext i
+  rw [fderiv_space_components _ _ (by fun_prop)]
+  simp only [vadd_apply, fderiv_add_const]
+  change _ = fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _) (EuclideanSpace.single μ 1)
+  simp [basis_apply]
+  congr 1
+  exact Eq.propIntro (fun a => Eq.symm a) fun a => (Eq.symm a)
+
+
+/-!
+
+## Properties of vadd with module structure
+
+-/
+
+lemma norm_vadd_le_add {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
+    ‖v +ᵥ s‖ ≤ ‖v‖ + ‖s‖ := by
+  trans ‖s - (-v +ᵥ (0 : Space d))‖
+  · apply le_of_eq
+    congr
+    ext i
+    simp only [vadd_apply, sub_apply, PiLp.neg_apply, zero_apply, add_zero, sub_neg_eq_add]
+    ring
+  · apply (norm_sub_le _ _).trans <| le_of_eq _
+    simp only [norm_vadd_zero, norm_neg]
+    ring
+
+@[fun_prop]
+lemma differentiable_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+    Differentiable ℝ (fun (s : Space d) => v +ᵥ s) :=
+  mk_differentiable.comp <| by fun_prop
+
+@[simp]
+lemma fderiv_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+    fderiv ℝ (fun s => v +ᵥ s) = fun (_ : Space d) => ContinuousLinearMap.id ℝ _ := by
+  ext s ds i
+  change fderiv ℝ (fun s => v +ᵥ s) s ds i = _
+  rw [fderiv_space_components]
+  simp
+  trans fderiv ℝ (coordCLM i) s ds
+  · congr
+    ext j
+    simp [coordCLM, coord_apply]
+  · rw [ContinuousLinearMap.fderiv]
+    simp [coordCLM, coord_apply]
+  · fun_prop
+
+@[fun_prop]
+lemma vadd_hasTemperateGrowth {d} (v : EuclideanSpace ℝ (Fin d)) :
+    Function.HasTemperateGrowth (fun s : Space d => v +ᵥ s) := by
+  apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1 + ‖v‖)
+  · rw [fderiv_vadd]
+    simp
+  · fun_prop
+  · intro x
+    simp
+    apply (norm_vadd_le_add _ _).trans
+    have : 0 ≤ ‖v‖ := by positivity
+    have : 0 ≤ ‖x‖ := by positivity
+    nlinarith
+
 end Space
diff --git a/README.md b/README.md
index b34f96bc4..fae37caaa 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
 
 
 <div align="center">
-<img src="./docs/PhysLeanLogo.jpeg" alt="PhysLean logo" width="500">
+<img src="./docs/PhysLib-logo.jpeg" alt="PhysLean logo" width="500">
 </div>
 
 
@@ -35,7 +35,8 @@
 
 ## Requirements of the project
 
-🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from **physics** formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
+🎯 The project shall contain results (definitions, theorems, lemmas and calculations) from **physics**,
+  including quantum information, formalized (or **digitalized**) into the interactive theorem prover **Lean 4**.
 
 🎯 The project shall be **organized** by **physics**.
 
@@ -45,7 +46,7 @@
 
 🎯 The project shall contain Physics Lean **tactics**, **notation** and **syntax** for physicists.
 
-🎯 The project shall *not* be tied to physics axiomizations (e.g. axiomatic QFT), but rather lexiable enough to accommodate different approaches and starting points.
+🎯 The project shall *not* be tied to physics axiomizations (e.g. axiomatic QFT), but rather flexiable enough to accommodate different approaches and starting points.
 
 🎯 The content of the project shall be carefully **reviewed** and curated, to ensure reusability, readability and fit.
 
@@ -56,71 +57,19 @@
 🎯 The project shall be for **main-stream** physics only.
 
 
-## How to get involved
+## Contributing to PhysLib
 
-See the [Get Involved](https://physlean.com/GetInvolved.html) for more details. Some suggestions:
-
-📣 write **informal** results - no need to learn Lean for this - see the [Getting Started](https://physlean.com/GettingStarted) page for more details,
-
-📣 tackle a [TODO item](https://physlean.com/TODOList),
-
-📣 or, start formalizing an area that you find interesting.
-
-Feel free to come to the [PhysLean zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/) to ask questions and advice.
+PhysLib is open-source and community run, and we welcome contributions from anyone.
+All you need to do is open a pull-request with your changes
+and our team of maintainers will review it and iterate with you on feedback until it
+can be merged.
 
+If you unsure where you would like to contribute, you may find ideas on:
+- our [open issues](https://github.com/leanprover-community/physlib/issues).
+- our [todo list](https://physlean.com/TODOList)
+- our [Get Involved page](https://physlean.com/GetInvolved.html)
 > [!NOTE]
-> When making contributing to PhysLean it is much better to do it with small steps. This makes it easier for us to review, and allows you to get feedback sooner.
-
-
-## Places in the project to start
-
-Good places to start an exploration of the project.
-
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Electromagnetism/MaxwellEquations.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FElectromagnetism%2FMaxwellEquations.lean)
-**Maxwell's equations** in electromagnetism.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FQuantumMechanics%2FOneDimension%2FHarmonicOscillator%2FBasic.lean)
-**Quantum Harmonic Oscillator** in quantum mechanics.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/StatisticalMechanics/CanonicalEnsemble/TwoState.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FStatisticalMechanics%2FCanonicalEnsemble%2FTwoState.lean)
-The two state **canonical ensemble** in statistical mechanics.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/CondensedMatter/TightBindingChain/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FCondensedMatter%2FTightBindingChain%2FBasic.lean)
-The **tight-binding model** in condensed matter physics
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Relativity/Special/TwinParadox/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FRelativity%2FSpecial%2FTwinParadox%2FBasic.lean)
-The **twin paradox** in special relativity.
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Particles/BeyondTheStandardModel/TwoHDM/Basic.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FParticles%2FBeyondTheStandardModel%2FTwoHDM%2FBasic.lean) The **two-Higgs doublet model** in particle physics
-- [🗂️](https://github.com/HEPLean/PhysLean/blob/master/PhysLean/QFT/PerturbationTheory/WickAlgebra/WicksTheorem.lean)
-[💻](https://live.physlean.com/#url=https%3A%2F%2Fraw.githubusercontent.com%2FHEPLean%2FPhysLean%2Frefs%2Fheads%2Fmaster%2FPhysLean%2FQFT%2FPerturbationTheory%2FWickAlgebra%2FWicksTheorem.lean)
-**Wick's theorem** in quantum field theory.
-
-
-## Associated media and publications
-- [📄](https://arxiv.org/abs/2405.08863) Joseph Tooby-Smith,
-__HepLean: Digitalising high energy physics__, Computer Physics Communications, Volume 308,
-2025, 109457, ISSN 0010-4655, https://doi.org/10.1016/j.cpc.2024.109457. \[arXiv:2405.08863\]
-- [📄](https://arxiv.org/abs/2411.07667) Joseph Tooby-Smith, __Formalization of physics index notation in Lean 4__, arXiv:2411.07667
-- [📄](https://arxiv.org/abs/2505.07939) Joseph Tooby-Smith, __Digitalizing Wick's Theorem__, arXiv:2505.07939
-- [🎥](https://www.youtube.com/watch?v=U7Xf5p6jAUU&t=62s) Lean Together 2025: Joseph Tooby-Smith, Physics and Lean
-- [🎥](https://www.youtube.com/watch?v=W2cObnopqas) Seminar recording of "HepLean: Lean and high energy physics" by J. Tooby-Smith
-
-### Papers referencing PhysLean
-- Hu, Jiewen, Thomas Zhu, and Sean Welleck. "miniCTX: Neural Theorem Proving with (Long-) Contexts." arXiv preprint [arXiv:2408.03350](https://www.arxiv.org/abs/2408.03350) (2024). [Project page]( https://cmu-l3.github.io/minictx/)
-
-How PhysLean (then called HepLean) was used: *Theorems from the space-time files of HepLean were included in a data set used to evaluate the ability of models to prove theorems from real-world repositories, which requires working with definitions, theorems, and other context not seen in training.*
-
-## Contributing
-
-We would love to have you involved! See the [Get Involved](https://physlean.com/GetInvolved.html) page to see how you can get involved.
-Any contributions are welcome! If you have any questions or want permission  permission to create a pull-request for this
-repository contact Joseph Tooby-Smith on the [Lean Zulip](https://leanprover.zulipchat.com), or email.
-
-## Installation
-
-If you want to play around with PhysLean, but do not want to download Lean, then you can use [GitPod](https://gitpod.io/#https://github.com/HEPLean/HepLean).
+> If stuck at any point there are lots of people happly to help on the [PhysLib zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib)
 
 ### Installing Lean 4
 
@@ -132,10 +81,82 @@ or
 
 - https://leanprover-community.github.io/get_started.html
 
-### Installing PhysLean
+### Installing PhysLib
 
 - Clone this repository (or download the repository as a Zip file)
 - Open a terminal at the top-level in the corresponding directory.
 - Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean.
 - Run `lake build`.
 - Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).
+
+### Making a pull-request
+
+There are lots of guides on how to make a pull-request on GitHub. The first thing you
+need to do is fork the repository. Once you've made your pull request we will review it:
+- Guide to [PhysLib reviews](https://github.com/leanprover-community/physlib/blob/master/docs/ReviewGuidelines.md).
+It will also undergo a number of automated checks called linters. Sometimes these are easier
+to run locally:
+- Guide to [linters and running them locally](https://github.com/leanprover-community/physlib/blob/master/scripts/README.md).
+
+Most importantly:
+> [!NOTE]
+> When making contributing to PhysLib it is much better to do it with small steps. This makes it easier for us to review, and allows you to get feedback sooner.
+
+## Maintainers
+
+Below are the maintainers of the project, however the best way to reach them is by posting
+on the [Lean Zulip](https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLib)
+
+- Léo Lessa (@Megaleo)
+- Alex Meiburg (@Timeroot)
+- Daniel Morrison (@morrison-daniel)
+- Zhi-Kai Pong (@zhikaip)
+- Rodolfo Soldati (@rodolfor-s)
+- Joseph Tooby-Smith (@jstoobysmith)
+- Winston Yin (@winstonyin)
+
+## Citing the project
+
+If you want to cite the project as a whole please cite:
+
+```
+@misc{physlib,
+  author = {The PhysLib community},
+  title = {PhysLib: The Lean Physics Library},
+  year = {2024},
+  publisher = {GitHub},
+  journal = {GitHub repository},
+  howpublished = {\url{https://github.com/leanprover-community/physlib}},
+}
+```
+
+PhysLib was formed by merging the general physics Lean library PhysLean (formerly called HepLean)
+with the quantum-information library Lean-QuantumInfo. Where appropriate please also consider
+citing the papers associated with the origin of these projects. For the former please use:
+```
+@article{Tooby-Smith:2024vqu,
+    author = "Tooby-Smith, Joseph",
+    title = "{HepLean: Digitalising high energy physics}",
+    eprint = "2405.08863",
+    archivePrefix = "arXiv",
+    primaryClass = "hep-ph",
+    doi = "10.1016/j.cpc.2024.109457",
+    journal = "Comput. Phys. Commun.",
+    volume = "308",
+    pages = "109457",
+    year = "2025"
+}
+```
+and for the latter please use:
+
+```
+@article{Meiburg:2025mwn,
+    author = "Meiburg, Alex and Lessa, Leonardo A. and Soldati, Rodolfo R.",
+    title = "{A Formalization of the Generalized Quantum Stein's Lemma in Lean}",
+    eprint = "2510.08672",
+    archivePrefix = "arXiv",
+    primaryClass = "quant-ph",
+    month = "10",
+    year = "2025"
+}
+```
diff --git a/docs/PhysLib-logo.jpeg b/docs/PhysLib-logo.jpeg
new file mode 100644
index 000000000..0a0cf877c
Binary files /dev/null and b/docs/PhysLib-logo.jpeg differ