diff --git a/Physlib.lean b/Physlib.lean
index 6b52eeb7e..f5f5813b4 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -353,6 +353,7 @@ public import Physlib.QuantumMechanics.Operators.AngularMomentum
 public import Physlib.QuantumMechanics.Operators.Commutation
 public import Physlib.QuantumMechanics.Operators.Covariance
 public import Physlib.QuantumMechanics.Operators.Examples
+public import Physlib.QuantumMechanics.Operators.MixedStateUncertainty
 public import Physlib.QuantumMechanics.Operators.Momentum
 public import Physlib.QuantumMechanics.Operators.Multiplication
 public import Physlib.QuantumMechanics.Operators.OneDimension.Commutation
diff --git a/Physlib/QuantumMechanics/Operators/API-map.yaml b/Physlib/QuantumMechanics/Operators/API-map.yaml
index 6475f635e..6250ef21d 100644
--- a/Physlib/QuantumMechanics/Operators/API-map.yaml
+++ b/Physlib/QuantumMechanics/Operators/API-map.yaml
@@ -161,6 +161,10 @@ Requirements:
     done: true
     location: "Physlib/QuantumMechanics/Operators/Uncertainty.lean (centeredCommutatorExpectation, rawCommutatorExpectation, inner_centered_commutator_of_raw_commutator, state_uncertainty_squared_of_centered_commutator, state_uncertainty_squared_with_covariance_of_centered_commutator, state_uncertainty_of_centered_commutator, state_uncertainty_squared_of_raw_commutator, state_uncertainty_squared_with_covariance_of_raw_commutator, state_uncertainty_of_raw_commutator)"
 
+  - description: "Robertson's uncertainty relation for finite-dimensional mixed states (density matrices) is proved, in both the squared-commutator form and the multiplicative normalized form, via Cauchy-Schwarz on the Hilbert-Schmidt space."
+    done: true
+    location: "Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean (HermitianMat.bracket_mat, MState.robertson_uncertainty, MState.robertson_normalized)"
+
   - description: "The API shall contain the Heisenberg uncertainty relation for position and momentum, that the product of the standard deviations of xᵢ and pᵢ in any unit state of a common domain is at least ℏ/2, which needs the position and momentum operators on a common domain before the present commutator can be fed into the present Robertson bound."
     done: false
     location: N/A
diff --git a/Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean b/Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean
new file mode 100644
index 000000000..841cb87d7
--- /dev/null
+++ b/Physlib/QuantumMechanics/Operators/MixedStateUncertainty.lean
@@ -0,0 +1,267 @@
+/-
+Copyright (c) 2026 Eduardo Nava-Hernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava-Gómez
+-/
+module
+
+public import QuantumInfo.States.Mixed.MState
+public import QuantumInfo.ForMathlib.HermitianMat.Sqrt
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Mathlib.Data.Bracket
+
+/-!
+# Robertson's uncertainty relation for mixed states
+
+## i. Overview
+
+In 1929, H. P. Robertson showed that two Hermitian observables on a quantum state satisfy a
+fundamental trade-off: the sharper one observable is known, the less the other can be known.
+Formally, for observables `G` and `O` on a state `ρ`:
+
+    ⟨i[G,O]⟩² / 4 ≤ Var(G) · Var(O).
+
+This module proves the relation for arbitrary finite-dimensional mixed states (`MState`),
+via Cauchy–Schwarz on the Hilbert–Schmidt space. The pure-state version of this bound, for
+partially defined operators on an inner product space, is in
+`Physlib.QuantumMechanics.Operators.Uncertainty`; the mixed-state formulation here requires
+the density-matrix framework of `MState`, which lives in `QuantumInfo`.
+
+## ii. Key results
+
+- `HermitianMat.bracket_mat` : the commutator bracket `⁅G, O⁆ = i(GO − OG)` on Hermitian
+  matrices.
+- `MState.robertson_uncertainty` : Robertson's relation for mixed states.
+- `MState.robertson_normalized` : the multiplicative form `1 ≤ 4 · Var(O) · Var(G)` under
+  the normalization `⟨i[G,O]⟩ = 1`, free of positivity hypotheses.
+
+## iii. Table of contents
+
+- A. Commutator bracket on Hermitian matrices
+- B. Hilbert–Schmidt embedding
+- C. Centered vectors and the commutator pairing
+- D. Robertson's uncertainty relation
+- E. Normalized form
+
+## iv. References
+
+- [H. P. Robertson, *The Uncertainty Principle* (1929)][robertson1929uncertainty].
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open scoped ComplexConjugate Matrix
+
+namespace HermitianMat
+
+variable {d : Type*} [Fintype d] [DecidableEq d]
+
+/-! ## A. Commutator bracket on Hermitian matrices -/
+
+/-- The commutator bracket `⁅G, O⁆ = i(GO − OG)` of two Hermitian matrices, as a
+`HermitianMat`. -/
+instance : Bracket (HermitianMat d ℂ) (HermitianMat d ℂ) where
+  bracket G O := ⟨Complex.I • (G.mat * O.mat - O.mat * G.mat), by
+    show (Complex.I • (G.mat * O.mat - O.mat * G.mat))ᴴ = _
+    rw [Matrix.conjTranspose_smul, Matrix.conjTranspose_sub, Matrix.conjTranspose_mul,
+      Matrix.conjTranspose_mul, G.H.eq, O.H.eq, Complex.star_def, Complex.conj_I]
+    module⟩
+
+omit [DecidableEq d] in
+@[simp]
+theorem bracket_mat (G O : HermitianMat d ℂ) :
+    ⁅G, O⁆.mat = Complex.I • (G.mat * O.mat - O.mat * G.mat) := by
+  simp only [Bracket.bracket]; rfl
+
+end HermitianMat
+
+namespace MState
+
+variable {d : Type*} [Fintype d] [DecidableEq d]
+
+noncomputable section
+
+/-! ## B. Hilbert–Schmidt embedding
+
+Cauchy–Schwarz is applied to `Tr(G O ρ)`, which requires embedding matrices into an inner
+product space via `hsVec`. The HermitianMat inner product (`Tr(AB)`) gives a different
+bilinear form and does not suffice for this argument. -/
+
+/-- The entries of a matrix, placed into `EuclideanSpace ℂ (d × d)` where Mathlib's inner
+product space API (in particular Cauchy–Schwarz) is available. -/
+private def hsVec (M : Matrix d d ℂ) : EuclideanSpace ℂ (d × d) :=
+  (WithLp.equiv 2 (d × d → ℂ)).symm (fun p => M p.1 p.2)
+
+omit [Fintype d] [DecidableEq d] in
+@[simp]
+private lemma hsVec_apply (M : Matrix d d ℂ) (p : d × d) : hsVec M p = M p.1 p.2 := rfl
+
+omit [DecidableEq d] in
+/-- The EuclideanSpace inner product of two embedded matrices is the Hilbert–Schmidt
+pairing `Tr(Aᴴ B)`. -/
+private lemma hsVec_inner (A B : Matrix d d ℂ) :
+    inner ℂ (hsVec A) (hsVec B) = (Aᴴ * B).trace := by
+  rw [PiLp.inner_apply, Fintype.sum_prod_type, Matrix.trace]
+  simp only [hsVec_apply, RCLike.inner_apply, starRingEnd_apply, Matrix.diag_apply,
+    Matrix.mul_apply, Matrix.conjTranspose_apply]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => ?_
+  exact mul_comm _ _
+
+/-! ## C. Centered vectors and the commutator pairing -/
+
+section observables
+
+variable (ρ : MState d)
+
+/-- The cyclic trace identity `Tr(√ρ X √ρ) = Tr(X ρ)`, the Hilbert–Schmidt engine of the
+mixed-state calculation. -/
+private lemma trace_sqrt_sandwich (X : Matrix d d ℂ) :
+    (ρ.M.sqrt.mat * X * ρ.M.sqrt.mat).trace = (X * ρ.m).trace := by
+  rw [Matrix.trace_mul_cycle, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M,
+    Matrix.trace_mul_comm]
+
+/-- The embedding of `A √ρ` against `√ρ` is the expectation value of `A`. -/
+private lemma inner_sqrt_left (A : HermitianMat d ℂ) :
+    inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec (A.mat * ρ.M.sqrt.mat)) = (ρ.exp_val A : ℂ) := by
+  rw [hsVec_inner, ρ.M.sqrt.H.eq,
+    show ρ.M.sqrt.mat * (A.mat * ρ.M.sqrt.mat) = ρ.M.sqrt.mat * A.mat * ρ.M.sqrt.mat by
+      simp [Matrix.mul_assoc],
+    ρ.trace_sqrt_sandwich, ← exp_val_ℂ, exp_val_ℂ_hermitian]
+
+/-- The embedded `√ρ` is a unit vector in Hilbert–Schmidt space. -/
+private lemma inner_sqrt_self :
+    inner ℂ (hsVec ρ.M.sqrt.mat) (hsVec ρ.M.sqrt.mat) = (1 : ℂ) := by
+  rw [hsVec_inner, ρ.M.sqrt.H.eq, HermitianMat.sqrt_sq ρ.nonneg, MState.mat_M, ρ.tr']
+
+/-- The embedding of `G √ρ` against `O √ρ` is the expectation value of the product `G O`. -/
+private lemma inner_hsVec_hsVec (G O : HermitianMat d ℂ) :
+    inner ℂ (hsVec (G.mat * ρ.M.sqrt.mat)) (hsVec (O.mat * ρ.M.sqrt.mat)) =
+      ρ.exp_val_ℂ (G.mat * O.mat) := by
+  rw [hsVec_inner, Matrix.conjTranspose_mul, ρ.M.sqrt.H.eq, (G.H).eq,
+    show ρ.M.sqrt.mat * G.mat * (O.mat * ρ.M.sqrt.mat) =
+        ρ.M.sqrt.mat * (G.mat * O.mat) * ρ.M.sqrt.mat by
+      simp [Matrix.mul_assoc],
+    ρ.trace_sqrt_sandwich, ← exp_val_ℂ]
+
+/-- The centered vector `A √ρ − ⟨A⟩ √ρ` in Hilbert–Schmidt space. -/
+private def centeredVec (A : HermitianMat d ℂ) : EuclideanSpace ℂ (d × d) :=
+  hsVec (A.mat * ρ.M.sqrt.mat) - (ρ.exp_val A : ℂ) • hsVec ρ.M.sqrt.mat
+
+/-- The squared Hilbert–Schmidt norm of the centered vector is the variance of `A`. -/
+private lemma norm_centered_sq (A : HermitianMat d ℂ) :
+    ‖ρ.centeredVec A‖ ^ 2 = ρ.variance A := by
+  have hself := ρ.inner_sqrt_self
+  have hleft := ρ.inner_sqrt_left A
+  have hright : inner ℂ (hsVec (A.mat * ρ.M.sqrt.mat)) (hsVec ρ.M.sqrt.mat) =
+      (ρ.exp_val A : ℂ) := by
+    rw [← inner_conj_symm, hleft, Complex.conj_ofReal]
+  have hAA := ρ.inner_hsVec_hsVec A A
+  have hAsq : ρ.exp_val_ℂ (A.mat * A.mat) = (ρ.exp_val (A ^ 2) : ℂ) := by
+    rw [← ρ.exp_val_ℂ_hermitian (A ^ 2), HermitianMat.mat_pow, pow_two]
+  have hexpand : (inner ℂ (ρ.centeredVec A) (ρ.centeredVec A) : ℂ) =
+      ρ.exp_val_ℂ (A.mat * A.mat) - (ρ.exp_val A : ℂ) * (ρ.exp_val A : ℂ) := by
+    unfold centeredVec
+    simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right,
+      Complex.conj_ofReal, hself, hleft, hright, hAA]
+    ring
+  have hre : ‖ρ.centeredVec A‖ ^ 2 = (inner ℂ (ρ.centeredVec A) (ρ.centeredVec A) : ℂ).re :=
+    (inner_self_eq_norm_sq (𝕜 := ℂ) (ρ.centeredVec A)).symm
+  rw [hre, hexpand, variance, hAsq, ← Complex.ofReal_mul, ← Complex.ofReal_sub, Complex.ofReal_re]
+  ring
+
+/-- The expectation of a product of Hermitian matrices is conjugate-symmetric in the
+factors. -/
+private lemma exp_val_ℂ_swap (G O : HermitianMat d ℂ) :
+    (starRingEnd ℂ) (ρ.exp_val_ℂ (G.mat * O.mat)) = ρ.exp_val_ℂ (O.mat * G.mat) := by
+  simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose]
+  rw [show ((G.mat * O.mat) * ρ.m)ᴴ = ρ.m * O.mat * G.mat by
+        rw [Matrix.conjTranspose_mul, Matrix.conjTranspose_mul, ρ.Hermitian.eq, (G.H).eq,
+          (O.H).eq, ← Matrix.mul_assoc],
+      Matrix.mul_assoc, Matrix.trace_mul_comm]
+
+/-- The inner product of the centered vectors of `G` and `O` is the covariance pairing
+`⟨GO⟩ − ⟨G⟩⟨O⟩`. -/
+private lemma inner_centered_centered (G O : HermitianMat d ℂ) :
+    (inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) : ℂ) =
+      ρ.exp_val_ℂ (G.mat * O.mat) - (ρ.exp_val G : ℂ) * (ρ.exp_val O : ℂ) := by
+  have hself := ρ.inner_sqrt_self
+  have hGl := ρ.inner_sqrt_left G
+  have hOl := ρ.inner_sqrt_left O
+  have hGr : inner ℂ (hsVec (G.mat * ρ.M.sqrt.mat)) (hsVec ρ.M.sqrt.mat) =
+      (ρ.exp_val G : ℂ) := by
+    rw [← inner_conj_symm, hGl, Complex.conj_ofReal]
+  have hGO := ρ.inner_hsVec_hsVec G O
+  unfold centeredVec
+  simp only [inner_sub_left, inner_sub_right, inner_smul_left, inner_smul_right,
+    Complex.conj_ofReal, hself, hOl, hGr, hGO]
+  ring
+
+/-! ## D. Robertson's uncertainty relation -/
+
+/-- **Robertson's uncertainty relation** (H. P. Robertson, Phys. Rev. **34**, 163–164 (1929)),
+for two Hermitian observables on an arbitrary finite-dimensional mixed state: the product of
+variances dominates a quarter of the squared commutator pairing. -/
+theorem robertson_uncertainty (G O : HermitianMat d ℂ) :
+    (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ρ.variance G * ρ.variance O := by
+  set z : ℂ := inner ℂ (ρ.centeredVec G) (ρ.centeredVec O) with hz
+  have hCS : ‖z‖ ≤ ‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖ := norm_inner_le_norm _ _
+  have hprodsq : (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 = ρ.variance G * ρ.variance O := by
+    rw [mul_pow, ρ.norm_centered_sq G, ρ.norm_centered_sq O]
+  have hz_sub : z - conj z =
+      ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat) := by
+    have hzz : z =
+        ρ.exp_val_ℂ (G.mat * O.mat) - (ρ.exp_val G : ℂ) * (ρ.exp_val O : ℂ) := by
+      rw [hz]; exact ρ.inner_centered_centered G O
+    rw [hzz, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_ofReal, ρ.exp_val_ℂ_swap]
+    ring
+  have hlin : ρ.exp_val_ℂ ⁅G, O⁆.mat =
+      Complex.I * (ρ.exp_val_ℂ (G.mat * O.mat) - ρ.exp_val_ℂ (O.mat * G.mat)) := by
+    rw [HermitianMat.bracket_mat]
+    simp only [MState.exp_val_ℂ, Matrix.smul_mul, Matrix.sub_mul,
+      Matrix.trace_smul, Matrix.trace_sub, smul_eq_mul]
+  have hw : z - conj z = 2 * Complex.I * (z.im : ℂ) := by
+    apply Complex.ext
+    · simp [Complex.sub_re, Complex.conj_re, Complex.mul_re, Complex.mul_im]
+    · simp [Complex.sub_im, Complex.conj_im, Complex.mul_re, Complex.mul_im]
+      ring
+  have hcomm : ρ.exp_val ⁅G, O⁆ = -2 * z.im := by
+    have hval : ρ.exp_val_ℂ ⁅G, O⁆.mat = ((-2 * z.im : ℝ) : ℂ) := by
+      rw [hlin, ← hz_sub, hw]
+      push_cast
+      rw [show Complex.I * (2 * Complex.I * (z.im : ℂ)) =
+          2 * (Complex.I * Complex.I) * (z.im : ℂ) by ring, Complex.I_mul_I]
+      ring
+    rw [show ρ.exp_val ⁅G, O⁆ = (ρ.exp_val_ℂ ⁅G, O⁆.mat).re from by
+      rw [exp_val_ℂ_hermitian]; simp, hval, Complex.ofReal_re]
+  have hnormsq : ‖z‖ ^ 2 = z.re * z.re + z.im * z.im := by
+    rw [sq, Complex.norm_mul_self_eq_normSq, Complex.normSq_apply]
+  have hzim : z.im ^ 2 ≤ ‖z‖ ^ 2 := by
+    rw [hnormsq, sq]; nlinarith [sq_nonneg z.re]
+  have hfinal : (ρ.exp_val ⁅G, O⁆) ^ 2 / 4 ≤ ‖z‖ ^ 2 := by
+    rw [hcomm]; nlinarith [hzim]
+  calc (ρ.exp_val ⁅G, O⁆) ^ 2 / 4
+      ≤ ‖z‖ ^ 2 := hfinal
+    _ ≤ (‖ρ.centeredVec G‖ * ‖ρ.centeredVec O‖) ^ 2 := by gcongr
+    _ = ρ.variance G * ρ.variance O := hprodsq
+
+/-! ## E. Normalized form -/
+
+/-- Robertson's uncertainty relation in **multiplicative form**: under the normalization
+`⟨i[G,O]⟩_ρ = 1`, the product of variances is at least `1/4`. -/
+theorem robertson_normalized (G O : HermitianMat d ℂ)
+    (hnorm : ρ.exp_val ⁅G, O⁆ = 1) :
+    1 ≤ 4 * ρ.variance O * ρ.variance G := by
+  have hR := ρ.robertson_uncertainty G O
+  rw [hnorm] at hR; norm_num at hR
+  nlinarith [ρ.variance_nonneg G, ρ.variance_nonneg O]
+
+end observables
+
+end
+
+end MState
+
+end
diff --git a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean
index 3b2b8b639..be63ab5e1 100644
--- a/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean
+++ b/Physlib/Relativity/LorentzAlgebra/ExponentialMap.lean
@@ -105,7 +105,6 @@ namespace Matrix
 
 variable {n R ι : Type*} [Fintype n]-- [DecidableEq n]
 
-@[simp]
 lemma trace_reindex [Semiring R] [Fintype ι] (e : n ≃ ι) (A : Matrix n n R) :
     trace (A.submatrix e.symm e.symm) = trace A := by
   simp only [trace, diag_apply, submatrix_apply]
diff --git a/QuantumInfo/States/Mixed/MState.lean b/QuantumInfo/States/Mixed/MState.lean
index 2b32fe4b8..b22d998f6 100644
--- a/QuantumInfo/States/Mixed/MState.lean
+++ b/QuantumInfo/States/Mixed/MState.lean
@@ -260,6 +260,40 @@ theorem exp_val_le_exp_val (ρ : MState d) {A B : HermitianMat d ℂ} (h : A ≤
   simp only [MState.exp_val]
   refine inner_mono ρ.nonneg h
 
+/-- `exp_val_ℂ` on a Hermitian matrix is real, and equal to `exp_val`. -/
+@[simp]
+theorem exp_val_ℂ_hermitian (A : HermitianMat d ℂ) :
+    ρ.exp_val_ℂ A.mat = (ρ.exp_val A : ℂ) := by
+  have hreal : (starRingEnd ℂ) (ρ.exp_val_ℂ A.mat) = ρ.exp_val_ℂ A.mat := by
+    simp only [MState.exp_val_ℂ, starRingEnd_apply, ← Matrix.trace_conjTranspose,
+      Matrix.conjTranspose_mul, ρ.Hermitian.eq, (A.H).eq]
+    rw [Matrix.trace_mul_comm]
+  have hre : (ρ.exp_val_ℂ A.mat).re = ρ.exp_val A := by
+    simp only [MState.exp_val_ℂ, MState.exp_val, HermitianMat.inner_eq_re_trace, MState.mat_M]
+    rw [Matrix.trace_mul_comm]
+    simp
+  rw [← hre]
+  exact (Complex.conj_eq_iff_re.mp hreal).symm
+
+/-- The **variance** of a Hermitian observable `A` on the state `ρ`. -/
+def variance (A : HermitianMat d ℂ) : ℝ :=
+  ρ.exp_val (A ^ 2) - (ρ.exp_val A) ^ 2
+
+/-- `Var_ρ(A) ≥ 0`. -/
+theorem variance_nonneg (A : HermitianMat d ℂ) : 0 ≤ ρ.variance A := by
+  set μ := ρ.exp_val A
+  have hsq : (A - μ • (1 : HermitianMat d ℂ)) ^ 2 =
+      A ^ 2 - (2 * μ) • A + μ ^ 2 • (1 : HermitianMat d ℂ) := by
+    ext1
+    simp only [HermitianMat.mat_pow, HermitianMat.mat_sub, HermitianMat.mat_smul,
+      HermitianMat.mat_add, HermitianMat.mat_one, pow_two]
+    rw [sub_mul, mul_sub, mul_sub]
+    simp only [mul_smul_comm, smul_mul_assoc, mul_one, one_mul, smul_smul]
+    module
+  have h := ρ.exp_val_nonneg (T := (A - μ • 1) ^ 2) HermitianMat.sq_nonneg
+  rw [hsq, exp_val_add, exp_val_sub, exp_val_smul, exp_val_smul, exp_val_one] at h
+  unfold variance; linarith
+
 end exp_val
 
 section pure