From 874000498fa8475852459a63c471c6a82fda50b3 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:44:00 +0900
Subject: [PATCH 1/9] hbar simp lemmas

---
 .../OneDimension/Basic.lean                   | 27 ++++++++++---------
 Physlib/QuantumMechanics/PlanckConstant.lean  |  3 +++
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean
index bb75635db..c2960cd8d 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/OneDimension/Basic.lean
@@ -8,7 +8,6 @@ module
 public import Physlib.QuantumMechanics.Operators.OneDimension.Parity
 public import Physlib.QuantumMechanics.Operators.OneDimension.Momentum
 public import Physlib.QuantumMechanics.Operators.OneDimension.Position
-public import Physlib.Meta.TODO.Basic
 /-!
 
 # 1d Harmonic Oscillator
@@ -77,20 +76,22 @@ open MeasureTheory
 variable (Q : HarmonicOscillator)
 
 @[simp]
-lemma m_mul_ω_div_two_ℏ_pos : 0 < Q.m * Q.ω / (2 * ℏ) := by
-  apply div_pos
-  · exact mul_pos Q.hm Q.hω
-  · exact mul_pos (by norm_num) ℏ_pos
+lemma m_pos : 0 < Q.m := Q.hm
 
 @[simp]
-lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / ℏ := by
-  apply div_pos
-  · exact mul_pos Q.hm Q.hω
-  · exact ℏ_pos
+lemma m_nonneg : 0 ≤ Q.m := Q.hm.le
+
+@[simp]
+lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne'
+
+@[simp]
+lemma ω_pos : 0 < Q.ω := Q.hω
 
-lemma m_ne_zero : Q.m ≠ 0 := by
-  have h1 := Q.hm
-  linarith
+@[simp]
+lemma ω_nonneg : 0 ≤ Q.ω := Q.hω.le
+
+@[simp]
+lemma ω_ne_zero : Q.ω ≠ 0 := Q.hω.ne'
 
 /-!
 
@@ -137,7 +138,7 @@ lemma ξ_inverse : Q.ξ⁻¹ = √(Q.m * Q.ω / ℏ) := by
 
 lemma one_over_ξ_sq : (1/Q.ξ)^2 = Q.m * Q.ω / ℏ := by
   rw [one_over_ξ]
-  refine Real.sq_sqrt (le_of_lt Q.m_mul_ω_div_ℏ_pos)
+  exact Real.sq_sqrt (by simp [div_nonneg])
 
 @[inherit_doc momentumOperator]
 scoped[QuantumMechanics.OneDimension.HarmonicOscillator] notation "Pᵒᵖ" => momentumOperator
diff --git a/Physlib/QuantumMechanics/PlanckConstant.lean b/Physlib/QuantumMechanics/PlanckConstant.lean
index 07030713e..5c76eb301 100644
--- a/Physlib/QuantumMechanics/PlanckConstant.lean
+++ b/Physlib/QuantumMechanics/PlanckConstant.lean
@@ -24,12 +24,15 @@ namespace Constants
 def ℏ : Subtype fun x : ℝ => 0 < x := ⟨1.054571817e-34, by norm_num⟩
 
 /-- Planck's constant is positive. -/
+@[simp]
 lemma ℏ_pos : 0 < (ℏ : ℝ) := ℏ.2
 
 /-- Planck's constant is non-negative. -/
+@[simp]
 lemma ℏ_nonneg : 0 ≤ (ℏ : ℝ) := le_of_lt ℏ.2
 
 /-- Planck's constant is not equal to zero. -/
+@[simp]
 lemma ℏ_ne_zero : (ℏ : ℝ) ≠ 0 := ne_of_gt ℏ.2
 
 end Constants

From 6d535f096fa2324351ee181aeb62086f0907c865 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:45:21 +0900
Subject: [PATCH 2/9] QHO basic

---
 .../HarmonicOscillator/Basic.lean             | 57 ++++++++++++++++++-
 1 file changed, 56 insertions(+), 1 deletion(-)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index e28fa0c1b..5cdac68ef 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -5,7 +5,10 @@ Authors: Gregory J. Loges
 -/
 module
 
-public import Physlib.Meta.TODO.Basic
+public import Physlib.Meta.Informal.Basic
+public import Physlib.QuantumMechanics.Operators.Momentum
+public import Physlib.QuantumMechanics.Operators.Multiplication
+public import Physlib.QuantumMechanics.QuantumSystem.Basic
 /-!
 
 # The quantum harmonic oscillator
@@ -33,3 +36,55 @@ TODO "Determine the energy eigenstates of the quantum harmonic oscillator
 
 TODO "Determine the energy eigenstates of the isotropic quantum harmonic oscillator
   in the 'spherical basis' in terms of spherical harmonics."
+
+noncomputable section
+namespace QuantumMechanics
+
+/-- The `d`-dimensional quantum harmonic oscillator. -/
+structure HarmonicOscillator (d : ℕ) where
+  /-- The mass (positive). -/
+  m : ℝ
+  hm : 0 < m
+  /-- The natural frequencies (positive). -/
+  ω : Fin d → ℝ
+  hω : ∀ i, 0 < ω i
+
+variable {d : ℕ} (Q : HarmonicOscillator d) (i : Fin d)
+
+namespace HarmonicOscillator
+
+open Constants SpaceDHilbertSpace MeasureTheory
+
+/-!
+## A. Basic properties
+-/
+
+/-!
+### A.1. Positive mass
+-/
+
+@[simp]
+lemma m_pos : 0 < Q.m := Q.hm
+
+@[simp]
+lemma m_nonneg : 0 ≤ Q.m := Q.hm.le
+
+@[simp]
+lemma m_ne_zero : Q.m ≠ 0 := Q.hm.ne'
+
+/-!
+### A.2. Positive natural frequencies
+-/
+
+@[simp]
+lemma ω_pos : 0 < Q.ω i := Q.hω i
+
+@[simp]
+lemma ω_nonneg : 0 ≤ Q.ω i := (Q.hω i).le
+
+@[simp]
+lemma ω_ne_zero : Q.ω i ≠ 0 := (Q.hω i).ne'
+
+end HarmonicOscillator
+end QuantumMechanics
+end

From 17b03e2d815e5418e532ae60c7e51e154921f40c Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:45:41 +0900
Subject: [PATCH 3/9] char lengths

---
 .../HarmonicOscillator/Basic.lean             | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 5cdac68ef..2d49640bf 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -85,6 +85,30 @@ lemma ω_nonneg : 0 ≤ Q.ω i := (Q.hω i).le
 @[simp]
 lemma ω_ne_zero : Q.ω i ≠ 0 := (Q.hω i).ne'
 
+/-!
+## B. Characteristic lengths
+-/
+
+/-- The characteristic length `ξ i ≔ √ℏ / (√Q.m * √(Q.ω i))`. -/
+def ξ : ℝ := √ℏ / (√Q.m * √(Q.ω i))
+
+lemma ξ_eq : Q.ξ i = √ℏ / (√Q.m * √(Q.ω i)) := rfl
+
+@[simp]
+lemma ξ_pos : 0 < Q.ξ i := by simp [ξ_eq]
+
+@[simp]
+lemma ξ_nonneg : 0 ≤ Q.ξ i := (Q.ξ_pos i).le
+
+@[simp]
+lemma ξ_ne_zero : Q.ξ i ≠ 0 := (Q.ξ_pos i).ne'
+
+lemma ξ_sq : (Q.ξ i) ^ 2 = ℏ / (Q.m * Q.ω i) := by rw [Q.ξ_eq]; field_simp; simp [← mul_rotate]
+
+lemma ξ_inv : (Q.ξ i)⁻¹ = √Q.m * √(Q.ω i) / √ℏ := by simp [ξ_eq]
+
+lemma ξ_inv' : (Q.ξ i)⁻¹ = Q.m * Q.ω i * Q.ξ i / ℏ := by field_simp; simp [ξ_sq, mul_assoc]
+
 end HarmonicOscillator
 end QuantumMechanics
 end

From 771e36f2de414a95b3344ad4d3efaf758c5832fa Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:46:04 +0900
Subject: [PATCH 4/9] potential function

---
 .../HarmonicOscillator/Basic.lean             | 50 +++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 2d49640bf..0706a9978 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -109,6 +109,56 @@ lemma ξ_inv : (Q.ξ i)⁻¹ = √Q.m * √(Q.ω i) / √ℏ := by simp [ξ_eq]
 
 lemma ξ_inv' : (Q.ξ i)⁻¹ = Q.m * Q.ω i * Q.ξ i / ℏ := by field_simp; simp [ξ_sq, mul_assoc]
 
+/-!
+## C. The quadratic potential function
+-/
+
+section
+
+open Matrix
+
+/-!
+### C.1. Positive-definite matrix
+-/
+
+/-- The positive-definite matrix defining the quadratic potential function. -/
+def potentialMatrix : Matrix (Fin d) (Fin d) ℝ := diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2)
+
+lemma potentialMatrix_eq : Q.potentialMatrix = diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2) := rfl
+
+-- lemma potentialMatrix_isSymm : Q.potentialMatrix.IsSymm := by simp [potentialMatrix_eq]
+
+lemma potentialMatrix_isHermitian : Q.potentialMatrix.IsHermitian := by simp [potentialMatrix_eq]
+
+@[simp]
+lemma potentialMatrix_mulVec (v : Fin d → ℝ) :
+    Q.potentialMatrix *ᵥ v = (2⁻¹ * Q.m) • (Q.ω ^ 2 * v) := by
+  ext
+  simp [potentialMatrix_eq, smul_mulVec, mulVec_diagonal]
+
+/-!
+### C.2. Quadratic form
+-/
+
+/-- The positive-definite quadratic form associated to the potential matrix. -/
+def potentialQuadraticForm : QuadraticForm ℝ (Fin d → ℝ) := Q.potentialMatrix.toQuadraticForm'
+
+/-!
+### C.3. Potential function
+-/
+
+/-- The quadratic potential function, `½m · ∑ i, ωᵢ²·xᵢ²`. -/
+def potentialFunction : Space d → ℝ := Q.potentialQuadraticForm ∘ Space.val
+
+lemma potentialFunction_eq : Q.potentialFunction = Q.potentialQuadraticForm ∘ Space.val := rfl
+
+/-- The potential function for the harmonic oscillator is a.e. strongly measurable. -/
+informal_lemma potentialFunction_aestronglyMeasurable where
+  deps := [``HarmonicOscillator]
+  tag := "QM-HO-potAESM"
+
+end
+
 end HarmonicOscillator
 end QuantumMechanics
 end

From 2b997e6c28b2d57c62cbe673ae32339230a29845 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:46:20 +0900
Subject: [PATCH 5/9] isotropic property

---
 .../QuantumMechanics/HarmonicOscillator/Basic.lean    | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 0706a9978..d953f8141 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -159,6 +159,17 @@ informal_lemma potentialFunction_aestronglyMeasurable where
 
 end
 
+/-!
+## C. Isotropic oscillators
+-/
+
+/-- A Harmonic oscillator is isotropic if all natural frequencies are equal. -/
+def IsIsotropic : Prop := ∀ i j, Q.ω i = Q.ω j
+
+lemma isIsotropic_def : Q.IsIsotropic ↔ ∀ i j, Q.ω i = Q.ω j := Iff.rfl
+
+lemma isIsotropic_of_one (Q : HarmonicOscillator 1) : Q.IsIsotropic := by simp [isIsotropic_def]
+
 end HarmonicOscillator
 end QuantumMechanics
 end

From edbf32fe3ccca49df321b10a03c448db79a0bde9 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:46:58 +0900
Subject: [PATCH 6/9] operators

---
 .../HarmonicOscillator/Basic.lean             | 61 +++++++++++++++++++
 1 file changed, 61 insertions(+)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index d953f8141..e3a3221e9 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -170,6 +170,67 @@ lemma isIsotropic_def : Q.IsIsotropic ↔ ∀ i j, Q.ω i = Q.ω j := Iff.rfl
 
 lemma isIsotropic_of_one (Q : HarmonicOscillator 1) : Q.IsIsotropic := by simp [isIsotropic_def]
 
+/-!
+## D. Hilbert space
+-/
+
+/-- The Hilbert space for the free particle. -/
+@[nolint unusedArguments]
+abbrev HS (_ : HarmonicOscillator d) : Type _ := SpaceDHilbertSpace d
+
+/-!
+## E. Operators
+-/
+
+/-!
+### E.1. Kinetic energy
+-/
+
+/-- The kinetic energy operator, `p²/2m`. -/
+def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOperator
+
+/-!
+### E.2. Potential energy
+-/
+
+section
+
+open MeasureTheory Complex
+
+/-- The potential operator which maps `ψ` to `Q.potentialFunction • ψ`. -/
+def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (ofReal ∘ Q.potentialFunction)
+
+/-- The potential operators for the harmonic oscillator is self-adjoint. -/
+informal_lemma potentialOperator_isSelfAdjoint where
+  deps := [``HarmonicOscillator.potentialFunction_aestronglyMeasurable]
+  tag := "QM-HO-potSA"
+
+end
+
+/-!
+### E.3. Hamiltonian
+-/
+
+/-- The Hamiltonian for the harmonic oscillator. -/
+def hamiltonian : Q.HS →ₗ.[ℂ] Q.HS := Q.kineticOperator + Q.potentialOperator
+
+lemma hamiltonain_eq : Q.hamiltonian = Q.kineticOperator + Q.potentialOperator := rfl
+
+/-- The Hamiltonian for the harmonic oscillator is essentially self-adjoint. -/
+informal_lemma hamiltonian_essentially_self_adjoint where
+  deps := [``HarmonicOscillator.hamiltonian]
+  tag := "QM-HO-hamESA"
+
+/-!
+## F. As a quantum system
+-/
+
+/-- The `d`-dimensional harmonic oscillator as a quantum system
+  (self-adjoint Hamiltonian acting on a Hilbert space). -/
+informal_definition toQuantumSystem where
+  deps := [``HarmonicOscillator.hamiltonian_essentially_self_adjoint]
+  tag := "QM-HO-sys"
+
 end HarmonicOscillator
 end QuantumMechanics
 end

From ae5fdcbc6ad6be72217255b3a893c5ce6ce6be34 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:47:29 +0900
Subject: [PATCH 7/9] TOC

---
 .../HarmonicOscillator/Basic.lean             | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index e3a3221e9..6b9a58e69 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -13,6 +13,29 @@ public import Physlib.QuantumMechanics.QuantumSystem.Basic
 
 # The quantum harmonic oscillator
 
+## i. Overview
+
+## ii. Key results
+
+## iii. Table of contents
+
+- A. Basic properties
+  - A.1. Positive mass
+  - A.2. Positive natural frequencies
+- B. Characteristic lengths
+- C. The quadratic potential function
+  - C.1. Positive-definite matrix
+  - C.2. Quadratic form
+  - C.3. Potential function
+- D. Hilbert space
+- E. Operators
+  - E.1. Kinetic energy
+  - E.2. Potential energy
+  - E.3. Hamiltonian
+- F. As a quantum system
+
+## iv. References
+
 -/
 
 @[expose] public section

From cbb07990424861349732f0ffa15f9b6550f44f0f Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 12:47:56 +0900
Subject: [PATCH 8/9] ladder operator file + TODOs

---
 Physlib.lean                                  |  1 +
 .../HarmonicOscillator/Basic.lean             | 15 +-----
 .../HarmonicOscillator/LadderOperators.lean   | 54 +++++++++++++++++++
 3 files changed, 57 insertions(+), 13 deletions(-)
 create mode 100644 Physlib/QuantumMechanics/HarmonicOscillator/LadderOperators.lean

diff --git a/Physlib.lean b/Physlib.lean
index b14473ecb..981f36e36 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -280,6 +280,7 @@ public import Physlib.QFT.QED.AnomalyCancellation.VectorLike
 public import Physlib.QuantumMechanics.FiniteTarget
 public import Physlib.QuantumMechanics.FreeParticle.Basic
 public import Physlib.QuantumMechanics.HarmonicOscillator.Basic
+public import Physlib.QuantumMechanics.HarmonicOscillator.LadderOperators
 public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Basic
 public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Completeness
 public import Physlib.QuantumMechanics.HarmonicOscillator.OneDimension.Eigenfunction
diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 6b9a58e69..9e99e9d56 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -40,19 +40,8 @@ public import Physlib.QuantumMechanics.QuantumSystem.Basic
 
 @[expose] public section
 
-TODO "Define `HarmonicOscillator` as a structure extending `SpaceDQuantumSystem`
-  (c.f. `Hydrogen.Basic.lean` for an example). In general the potential is determined by
-  a positive-definite, real symmetric matrix `V = ½m(xᵗ·A·x)`.
-  Note that such matrices can always be diagonalized so perhaps it suffices to take `A` diagonal.
-  A special case with enhanced symmetry is the isotropic harmonic oscillator with `A = ω²·𝕀`."
-
-TODO "Define the raising/lowering/number operators for the quantum harmonic oscillator."
-
-TODO "Prove the commutation relations for the raising/lowering/number/Hamiltonian operators
-  of the quantum harmonic oscillator."
-
-TODO "Determine the spectrum of the quantum harmonic oscillator in terms of the eigenvalues
-  of the matrix `A ≻ 0` appearing in the potential."
+TODO "Determine the spectrum of the quantum harmonic oscillator in terms of
+  the natural frequencies and integer quantum numbers."
 
 TODO "Determine the energy eigenstates of the quantum harmonic oscillator
   in the 'Cartesian basis' in terms of Hermite polynomials."
diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/LadderOperators.lean b/Physlib/QuantumMechanics/HarmonicOscillator/LadderOperators.lean
new file mode 100644
index 000000000..55192434d
--- /dev/null
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/LadderOperators.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Gregory J. Loges. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gregory J. Loges
+-/
+module
+
+public import Physlib.QuantumMechanics.HarmonicOscillator.Basic
+/-!
+
+# Ladder operators
+
+This is currently a stub, intended to house the ladder operators of the quantum harmonic oscillator.
+
+-/
+
+@[expose] public section
+
+/-!
+## A. Ladder operators
+-/
+
+TODO "Define the raising/lowering operators for the quantum harmonic oscillator."
+
+TODO "Prove that the raising/lowering operators are adjoints of one another (tag as simp?)."
+
+TODO "Prove the commutation relations for the ladder operators, `[a, a†] = δ`."
+
+/-!
+## B. Number operators
+-/
+
+TODO "Define the number operators for the quantum harmonic oscillator
+  in terms of the ladder operators."
+
+TODO "Prove that the number operators are symmetric/self-adjoint."
+
+TODO "Prove the commutation relations for the number operators, `[N i, N j] = 0`."
+
+TODO "Prove the commutation relations between number and ladder operators,
+  `[N, a] = -δ a` and `[N, a†] = δ a†`."
+
+/-!
+## C. Hamiltonian
+-/
+
+TODO "Define a Hamiltonian in terms of the number operators."
+
+TODO "Prove the commutation relations between the Hamiltonian and ladder/number operators."
+
+TODO "Relate the 'number operator' Hamiltonian to the 'K + T' Hamiltonian
+  (=/≤/≥ depending on their domains)."
+
+TODO "Prove that the two Hamiltonians define the same quantum system."

From a64bd52d59ab6517b8ccccefccbef0e840b95422 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Sun, 19 Jul 2026 13:15:01 +0900
Subject: [PATCH 9/9] basic overview

---
 .../HarmonicOscillator/Basic.lean             | 34 ++++++++++++-------
 1 file changed, 21 insertions(+), 13 deletions(-)

diff --git a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
index 9e99e9d56..d756ac890 100644
--- a/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
+++ b/Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean
@@ -15,6 +15,15 @@ public import Physlib.QuantumMechanics.QuantumSystem.Basic
 
 ## i. Overview
 
+The harmonic oscillator is one of the most important examples in non-relativistic quantum mechanics.
+It describes a particle of mass `m` subject to a positive-definite quadratic potential
+in `d` dimensions.
+
+- `Basic.lean` : Properties of the potential, definition of isotropic oscillators,
+    kinetic, potential and Hamiltonian operators.
+- `LadderOperators.lean` : Definitions of the raising/lowering/number operators
+    and their algebraic properties.
+
 ## ii. Key results
 
 ## iii. Table of contents
@@ -27,12 +36,13 @@ public import Physlib.QuantumMechanics.QuantumSystem.Basic
   - C.1. Positive-definite matrix
   - C.2. Quadratic form
   - C.3. Potential function
-- D. Hilbert space
-- E. Operators
+- D. Isotropic oscillators
+- E. Hilbert space
+- F. Operators
   - E.1. Kinetic energy
   - E.2. Potential energy
   - E.3. Hamiltonian
-- F. As a quantum system
+- G. As a quantum system
 
 ## iv. References
 
@@ -138,8 +148,6 @@ def potentialMatrix : Matrix (Fin d) (Fin d) ℝ := diagonal ((2⁻¹ * Q.m) •
 
 lemma potentialMatrix_eq : Q.potentialMatrix = diagonal ((2⁻¹ * Q.m) • Q.ω ^ 2) := rfl
 
--- lemma potentialMatrix_isSymm : Q.potentialMatrix.IsSymm := by simp [potentialMatrix_eq]
-
 lemma potentialMatrix_isHermitian : Q.potentialMatrix.IsHermitian := by simp [potentialMatrix_eq]
 
 @[simp]
@@ -172,7 +180,7 @@ informal_lemma potentialFunction_aestronglyMeasurable where
 end
 
 /-!
-## C. Isotropic oscillators
+## D. Isotropic oscillators
 -/
 
 /-- A Harmonic oscillator is isotropic if all natural frequencies are equal. -/
@@ -183,26 +191,26 @@ lemma isIsotropic_def : Q.IsIsotropic ↔ ∀ i j, Q.ω i = Q.ω j := Iff.rfl
 lemma isIsotropic_of_one (Q : HarmonicOscillator 1) : Q.IsIsotropic := by simp [isIsotropic_def]
 
 /-!
-## D. Hilbert space
+## E. Hilbert space
 -/
 
-/-- The Hilbert space for the free particle. -/
+/-- The Hilbert space for the quantum harmonic oscillator. -/
 @[nolint unusedArguments]
 abbrev HS (_ : HarmonicOscillator d) : Type _ := SpaceDHilbertSpace d
 
 /-!
-## E. Operators
+## F. Operators
 -/
 
 /-!
-### E.1. Kinetic energy
+### F.1. Kinetic energy
 -/
 
 /-- The kinetic energy operator, `p²/2m`. -/
 def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOperator
 
 /-!
-### E.2. Potential energy
+### F.2. Potential energy
 -/
 
 section
@@ -220,7 +228,7 @@ informal_lemma potentialOperator_isSelfAdjoint where
 end
 
 /-!
-### E.3. Hamiltonian
+### F.3. Hamiltonian
 -/
 
 /-- The Hamiltonian for the harmonic oscillator. -/
@@ -234,7 +242,7 @@ informal_lemma hamiltonian_essentially_self_adjoint where
   tag := "QM-HO-hamESA"
 
 /-!
-## F. As a quantum system
+## G. As a quantum system
 -/
 
 /-- The `d`-dimensional harmonic oscillator as a quantum system