Clifford project

4. Pauli matrices🔗

This section defines the generalized Pauli X and Z matrices on ℂ^d and proves some basic fats about them. Throughout this section we assume that d ≥ 1.

Lean codevariable (d : ℕ) [hd : NeZero d]

The generalized Pauli X matrix corresponds to adding one modulo d. This transformation is defined as the permutation matrix associated to a cyclic permutation of the basis.

Lean codeomit [NeZero d] in def ZmodShift (i : ZMod d) : (ZMod d) ≃ (ZMod d) := .mk (fun x => x - i) (fun x => x + i) (d:ℕhd:NeZero di:ZMod d⊢ Function.LeftInverse (fun x => x + i) fun x => x - i d:ℕhd:NeZero di:ZMod d⊢ ∀ (x : ZMod d), (fun x => x + i) ((fun x => x - i) x) = x; d:ℕhd:NeZero di:ZMod dx:ZMod d⊢ (fun x => x + i) ((fun x => x - i) x) = x; All goals completed! 🐙) (d:ℕhd:NeZero di:ZMod d⊢ Function.RightInverse (fun x => x + i) fun x => x - i d:ℕhd:NeZero di:ZMod d⊢ Function.LeftInverse (fun x => x - i) fun x => x + i; d:ℕhd:NeZero di:ZMod d⊢ ∀ (x : ZMod d), (fun x => x - i) ((fun x => x + i) x) = x; d:ℕhd:NeZero di:ZMod dx:ZMod d⊢ (fun x => x - i) ((fun x => x + i) x) = x; All goals completed! 🐙) omit [NeZero d] in lemma ZmodShiftOne (hd : d = 1) : (ZmodShift d 1) = Equiv.refl (ZMod d) := d:ℕhd:d = 1⊢ ZmodShift d 1 = Equiv.refl (ZMod d) d:ℕhd:d = 1⊢ { toFun := fun x => x - 1, invFun := fun x => x + 1, left_inv := ⋯, right_inv := ⋯ } = Equiv.refl (ZMod d); d:ℕhd:d = 1⊢ { toFun := fun x => x - 1, invFun := fun x => x + 1, left_inv := ⋯, right_inv := ⋯ } = Equiv.refl (ZMod 1); d:ℕhd:d = 1x:ZMod 1⊢ { toFun := fun x => x - 1, invFun := fun x => x + 1, left_inv := ⋯, right_inv := ⋯ } x = (Equiv.refl (ZMod 1)) x; d:ℕhd:d = 1x:ZMod 1⊢ 1 = 0; All goals completed! 🐙 omit [NeZero d] in lemma ZmodShiftMul (i j : ZMod d) : (ZmodShift d i) * (ZmodShift d j) = (ZmodShift d (i + j)) := d:ℕi:ZMod dj:ZMod d⊢ ZmodShift d i * ZmodShift d j = ZmodShift d (i + j) d:ℕi:ZMod dj:ZMod dx:ZMod d⊢ (ZmodShift d i * ZmodShift d j) x = (ZmodShift d (i + j)) x; d:ℕi:ZMod dj:ZMod dx:ZMod d⊢ (ZmodShift d i) ((ZmodShift d j) x) = (ZmodShift d (i + j)) x; d:ℕi:ZMod dj:ZMod dx:ZMod d⊢ { toFun := fun x => x - i, invFun := fun x => x + i, left_inv := ⋯, right_inv := ⋯ } ({ toFun := fun x => x - j, invFun := fun x => x + j, left_inv := ⋯, right_inv := ⋯ } x) = { toFun := fun x => x - (i + j), invFun := fun x => x + (i + j), left_inv := ⋯, right_inv := ⋯ } x; d:ℕi:ZMod dj:ZMod dx:ZMod d⊢ x - j - i = x - (i + j); All goals completed! 🐙 omit [NeZero d] in lemma ZmodShiftInv (i : ZMod d) : (ZmodShift d i)⁻¹ = (ZmodShift d (- i)) := d:ℕi:ZMod d⊢ (ZmodShift d i)⁻¹ = ZmodShift d (-i) d:ℕi:ZMod dx:ZMod d⊢ (ZmodShift d i)⁻¹ x = (ZmodShift d (-i)) x; d:ℕi:ZMod dx:ZMod d⊢ (ZmodShift d i).symm x = (ZmodShift d (-i)) x; d:ℕi:ZMod dx:ZMod d⊢ { toFun := fun x => x - i, invFun := fun x => x + i, left_inv := ⋯, right_inv := ⋯ }.symm x = { toFun := fun x => x - -i, invFun := fun x => x + -i, left_inv := ⋯, right_inv := ⋯ } x; All goals completed! 🐙; omit [NeZero d] in lemma ZmodShiftInv' (i : ZMod d) : (ZmodShift d i).symm = (ZmodShift d (- i)) := d:ℕi:ZMod d⊢ (ZmodShift d i).symm = ZmodShift d (-i) d:ℕi:ZMod dx:ZMod d⊢ (ZmodShift d i).symm x = (ZmodShift d (-i)) x; d:ℕi:ZMod dx:ZMod d⊢ { toFun := fun x => x - i, invFun := fun x => x + i, left_inv := ⋯, right_inv := ⋯ }.symm x = { toFun := fun x => x - -i, invFun := fun x => x + -i, left_inv := ⋯, right_inv := ⋯ } x; All goals completed! 🐙;
Definition4.1
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Lemma 4.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 5.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
OwnerMaris Ozols

The d-dimensional Pauli X matrix acts as follows: X \ket{k} = \ket{k+1} where k ∈ ℤ_d and addition is modulo d.

Lean code for Definition4.1-- NOTE : Permutation matrices are reverted, have to transpose to get the expected result! -- Hence the definition of ZmodShift that ends up reversed from the expected matrix action def X : Matrix (ZMod d) (ZMod d) ℂ := (Equiv.Perm.permMatrix ℂ (ZmodShift d 1))

Basic properties of X

Lemma4.2
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerWilliam HasleyEffortsmall

When d = 1, X is the Identity matrix

Lean code for Lemma4.2lemma X_one (hd : d = 1) (n : ℕ) : (X d) ^ n = 1 := d:ℕhd✝:NeZero dhd:d = 1n:ℕ⊢ X d ^ n = 1 d:ℕhd✝:NeZero dhd:d = 1n:ℕ⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d 1) ^ n = 1; d:ℕhd✝:NeZero dhd:d = 1n:ℕ⊢ Equiv.Perm.permMatrix ℂ (Equiv.refl (ZMod d)) ^ n = 1d:ℕhd✝:NeZero dhd:d = 1n:ℕ⊢ d = 1; d:ℕhd✝:NeZero dhd:d = 1n:ℕ⊢ d = 1; All goals completed! 🐙
Lemma4.3
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerWilliam HasleyEffortsmall

Let M^{\dagger} denote the usual conjugate transpose of M. Then X^{\dagger} = X^{-1}

Lean code for Lemma4.3@[simp] lemma X_inv : (X d)† = (X d)⁻¹ := d:ℕhd:NeZero d⊢ (X d)† = (X d)⁻¹ d:ℕhd:NeZero d⊢ (Equiv.Perm.permMatrix ℂ (ZmodShift d 1))† = (Equiv.Perm.permMatrix ℂ (ZmodShift d 1))⁻¹; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d 1)⁻¹ = (Equiv.Perm.permMatrix ℂ (ZmodShift d 1))⁻¹; d:ℕhd:NeZero d⊢ (Equiv.Perm.permMatrix ℂ (ZmodShift d 1))⁻¹ = Equiv.Perm.permMatrix ℂ (ZmodShift d 1)⁻¹; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d 1)⁻¹ * Equiv.Perm.permMatrix ℂ (ZmodShift d 1) = 1; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d 1 * (ZmodShift d 1)⁻¹) = 1; All goals completed! 🐙

Powers of the Pauli X matrix.

Lean codelemma X_pow_pos_n (n : ℕ) : X d ^ n = Equiv.Perm.permMatrix ℂ ((ZmodShift d n)) := d:ℕhd:NeZero dn:ℕ⊢ X d ^ n = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n) induction n with d:ℕhd:NeZero d⊢ X d ^ 0 = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑0) d:ℕhd:NeZero d⊢ 1 = Equiv.Perm.permMatrix ℂ (ZmodShift d 0); d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ 1 i j = Equiv.Perm.permMatrix ℂ (ZmodShift d 0) i j; d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ 1 i j = Equiv.Perm.permMatrix ℂ { toFun := fun x => x - 0, invFun := fun x => x + 0, left_inv := ⋯, right_inv := ⋯ } i j; d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ 1 i j = if i = j then 1 else 0; All goals completed! 🐙 d:ℕhd:NeZero dn:ℕhind:X d ^ n = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n)⊢ X d ^ (n + 1) = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑(n + 1)) d:ℕhd:NeZero dn:ℕhind:X d ^ n = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n)⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n) * X d = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑(n + 1)); d:ℕhd:NeZero dn:ℕhind:X d ^ n = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n)⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n) * Equiv.Perm.permMatrix ℂ (ZmodShift d 1) = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑(n + 1)); d:ℕhd:NeZero dn:ℕhind:X d ^ n = Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n)⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d ↑n) * Equiv.Perm.permMatrix ℂ (ZmodShift d 1) = Equiv.Perm.permMatrix ℂ (ZmodShift d (↑n + 1)); All goals completed! 🐙;

The Pauli X matrix has order d.

Lemma4.4
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerGina Muuss

The d-th power of the d-dimensional Pauli X matrix is the identity matrix: X^d = I.

Lean code for Lemma4.4@[simp] lemma X_pow_d_eq_one : X d ^ d = 1 := d:ℕhd:NeZero d⊢ X d ^ d = 1 d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d ↑d) = 1; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ (ZmodShift d 0) = 1; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ { toFun := fun x => x - 0, invFun := fun x => x + 0, left_inv := ⋯, right_inv := ⋯ } = 1; d:ℕhd:NeZero d⊢ Equiv.Perm.permMatrix ℂ { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ } = 1; d:ℕhd:NeZero dx:ZMod dj✝:ZMod d⊢ Equiv.Perm.permMatrix ℂ { toFun := fun x => x, invFun := fun x => x, left_inv := ⋯, right_inv := ⋯ } x j✝ = 1 x j✝; d:ℕhd:NeZero dx:ZMod dj✝:ZMod d⊢ (if x = j✝ then 1 else 0) = 1 x j✝; All goals completed! 🐙
Lean codelemma isUnit_X_det : IsUnit (X d).det := d:ℕhd:NeZero d⊢ IsUnit (X d).det d:ℕhd:NeZero d⊢ IsUnit (Equiv.Perm.permMatrix ℂ (ZmodShift d 1)).det; d:ℕhd:NeZero d⊢ IsUnit ↑↑(Equiv.Perm.sign (ZmodShift d 1)); All goals completed! 🐙

The generalized Pauli Z matrix is diagonal and introduces a phase ω to each standard basis vector \ket{k}. This transformation is defined as the Diagonal matrix where the i-th entry is \omega^i

Lean codeomit [NeZero d] in @[reducible] noncomputable def diag_omega_pow : (ZMod d → ℂ)ˣ := .mk (fun i => (ω d) ^ i.val) (fun i => (ω d) ^ (-i).val) (d:ℕhd:NeZero d⊢ ((fun i => ↑(ω d) ^ i.val) * fun i => ↑(ω d) ^ (-i).val) = 1 d:ℕhd:NeZero di:ZMod d⊢ ((fun i => ↑(ω d) ^ i.val) * fun i => ↑(ω d) ^ (-i).val) i = 1 i; d:ℕhd:NeZero di:ZMod d⊢ ↑(ω d) ^ i.val * ↑(ω d) ^ (-i).val = 1; d:ℕhd:NeZero di:ZMod d⊢ ↑(ω d) ^ (i + -i).val = 1; All goals completed! 🐙) (d:ℕhd:NeZero d⊢ ((fun i => ↑(ω d) ^ (-i).val) * fun i => ↑(ω d) ^ i.val) = 1 d:ℕhd:NeZero di:ZMod d⊢ ((fun i => ↑(ω d) ^ (-i).val) * fun i => ↑(ω d) ^ i.val) i = 1 i; d:ℕhd:NeZero di:ZMod d⊢ ↑(ω d) ^ (-i).val * ↑(ω d) ^ i.val = 1; d:ℕhd:NeZero di:ZMod d⊢ ↑(ω d) ^ (-i + i).val = 1; All goals completed! 🐙) @[simp] lemma diag_omega_pow_inv : Ring.inverse (diag_omega_pow d).val = fun i => (ω d).val ^ (-i).val := d:ℕhd:NeZero d⊢ Ring.inverse ↑(diag_omega_pow d) = fun i => ↑(ω d) ^ (-i).val d:ℕhd:NeZero d⊢ ↑(diag_omega_pow d)⁻¹ = fun i => ↑(ω d) ^ (-i).val; All goals completed! 🐙
Definition4.5
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Definition 5.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
OwnerMaris Ozols

The d-dimensional Pauli Z matrix acts as follows: Z \ket{k} = ω^k \ket{k} where k ∈ ℤ_d and ω is the primitive d-th root of unity from Definition 2.2.

Lean code for Definition4.5omit [NeZero d] in noncomputable def Z : Matrix (ZMod d) (ZMod d) ℂ := Matrix.diagonal (diag_omega_pow d)

Basic properties of Z

Lemma4.6
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerWilliam HasleyEffortsmall

When d = 1, Z is the Identity matrix

Lean code for Lemma4.6@[simp] lemma Z_one (hd : d = 1) : (Z d) = 1 := d:ℕhd✝:NeZero dhd:d = 1⊢ Z d = 1 d:ℕhd✝:NeZero dhd:d = 1⊢ Matrix.diagonal ↑(diag_omega_pow d) = 1; d:ℕhd✝:NeZero dhd:d = 1⊢ (fun i => ↑(ω d) ^ i.val) = 1; d:ℕhd✝:NeZero dhd:d = 1x:ZMod d⊢ ↑(ω d) ^ x.val = 1 x; d:ℕhd✝:NeZero dhd:d = 1x:ZMod d⊢ ↑1 ^ x.val = 1 xd:ℕhd✝:NeZero dhd:d = 1x:ZMod d⊢ d = 1; d:ℕhd✝:NeZero dhd:d = 1x:ZMod d⊢ d = 1; All goals completed! 🐙
Lemma4.7
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerWilliam HasleyEffortsmall

Much like X, Z is a unitary transformation. That is, Z^{\dagger} = Z^{-1}

Lean code for Lemma4.7@[simp] lemma Z_inv : (Z d)† = (Z d)⁻¹ := d:ℕhd:NeZero d⊢ (Z d)† = (Z d)⁻¹ d:ℕhd:NeZero d⊢ (Matrix.diagonal ↑(diag_omega_pow d))† = (Matrix.diagonal ↑(diag_omega_pow d))⁻¹; d:ℕhd:NeZero d⊢ Matrix.diagonal (star fun i => ↑(ω d) ^ i.val) = (Matrix.diagonal fun i => ↑(ω d) ^ i.val)⁻¹; d:ℕhd:NeZero d⊢ Matrix.diagonal (star fun i => ↑(ω d) ^ i.val) = Matrix.diagonal (Ring.inverse fun i => ↑(ω d) ^ i.val); d:ℕhd:NeZero d⊢ ∀ (i : ZMod d), (↑(ω d) ^ i.val)⁻¹ = Ring.inverse (fun i => ↑(ω d) ^ i.val) i; d:ℕhd:NeZero di:ZMod d⊢ (↑(ω d) ^ i.val)⁻¹ = Ring.inverse (fun i => ↑(ω d) ^ i.val) i; All goals completed! 🐙;

The Pauli Z matrix also has order d.

Lean codelemma Z_pow_n (n : ℕ) : Z d ^ n = Matrix.diagonal (fun i => (((ω d) ^ (n * i.val)) : ℂ)) := d:ℕhd:NeZero dn:ℕ⊢ Z d ^ n = Matrix.diagonal fun i => ↑(ω d) ^ (n * i.val) induction n with d:ℕhd:NeZero d⊢ Z d ^ 0 = Matrix.diagonal fun i => ↑(ω d) ^ (0 * i.val) All goals completed! 🐙; d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)⊢ Z d ^ (k + 1) = Matrix.diagonal fun i => ↑(ω d) ^ ((k + 1) * i.val) d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)⊢ (Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)) * Z d = Matrix.diagonal fun i => ↑(ω d) ^ ((k + 1) * i.val); d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)⊢ (Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)) * Matrix.diagonal ↑(diag_omega_pow d) = Matrix.diagonal fun i => ↑(ω d) ^ ((k + 1) * i.val); d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)⊢ (Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val) * ↑(diag_omega_pow d) i) = Matrix.diagonal fun i => ↑(ω d) ^ ((k + 1) * i.val); d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)⊢ ∀ (i : ZMod d), ↑(ω d) ^ (k * i.val) * ↑(ω d) ^ i.val = ↑(ω d) ^ ((k + 1) * i.val); d:ℕhd:NeZero dk:ℕih:Z d ^ k = Matrix.diagonal fun i => ↑(ω d) ^ (k * i.val)i:ZMod d⊢ ↑(ω d) ^ (k * i.val) * ↑(ω d) ^ i.val = ↑(ω d) ^ ((k + 1) * i.val); All goals completed! 🐙
Lemma4.8
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerCarli Bruinsma

The d-th power of the d-dimensional Pauli Z matrix is the identity matrix: Z^d = I.

Lean code for Lemma4.8@[simp] lemma Z_pow_d_eq_one : (Z d) ^ d = 1 := d:ℕhd:NeZero d⊢ Z d ^ d = 1 d:ℕhd:NeZero d⊢ (Matrix.diagonal fun i => ↑(ω d) ^ (d * i.val)) = 1; d:ℕhd:NeZero d⊢ (fun i => ↑(ω d) ^ (d * i.val)) = 1; d:ℕhd:NeZero di:ZMod d⊢ ↑(ω d) ^ (d * i.val) = 1 i d:ℕhd:NeZero di:ZMod d⊢ 1 = 1 i All goals completed! 🐙
Lean codelemma isUnit_Z_det : IsUnit (Z d).det := d:ℕhd:NeZero d⊢ IsUnit (Z d).det d:ℕhd:NeZero d⊢ IsUnit (Matrix.diagonal ↑(diag_omega_pow d)).det; d:ℕhd:NeZero d⊢ IsUnit (∏ i, ↑(diag_omega_pow d) i); d:ℕhd:NeZero d⊢ ∀ a ∈ Finset.univ, IsUnit (↑(diag_omega_pow d) a); d:ℕhd:NeZero da:ZMod d⊢ a ∈ Finset.univ → IsUnit (↑(diag_omega_pow d) a); All goals completed! 🐙

Pauli X and Z commute up to a phase.

Lemma4.9
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerGina Muuss

Pauli X and Z matrices satisfy the following commutation relation: Z X = ω X Z.

Lean code for Lemma4.9lemma ZX_eq_omega_mul_XZ : Z d * X d = (ω d).val • (X d * Z d) := d:ℕhd:NeZero d⊢ Z d * X d = ↑(ω d) • (X d * Z d) d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ (Z d * X d) i j = (↑(ω d) • (X d * Z d)) i j; d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ (Matrix.diagonal ↑(diag_omega_pow d) * X d) i j = (↑(ω d) • (X d * Matrix.diagonal ↑(diag_omega_pow d))) i j; d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ↑(diag_omega_pow d) i * X d i j = (↑(ω d) • (X d * Matrix.diagonal ↑(diag_omega_pow d))) i j; d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ↑(ω d) ^ i.val * X d i j = ↑(ω d) * (X d i j * ↑(ω d) ^ j.val); d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ↑(ω d) ^ i.val * Equiv.Perm.permMatrix ℂ { toFun := fun x => x - 1, invFun := fun x => x + 1, left_inv := ⋯, right_inv := ⋯ } i j = ↑(ω d) * (Equiv.Perm.permMatrix ℂ { toFun := fun x => x - 1, invFun := fun x => x + 1, left_inv := ⋯, right_inv := ⋯ } i j * ↑(ω d) ^ j.val); d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ (if i - 1 = j then ↑(ω d) ^ i.val else 0) = if i - 1 = j then ↑(ω d) * ↑(ω d) ^ j.val else 0 d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ (i - 1 = j → ↑(ω d) ^ i.val = if i - 1 = j then ↑(ω d) ^ (j.val + 1) else 0) ∧ (¬i - 1 = j → 0 = if i - 1 = j then ↑(ω d) ^ (j.val + 1) else 0); d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ (i - 1 = j → ↑(ω d) ^ i.val = if i - 1 = j then ↑(ω d) ^ (j.val + 1) else 0) ∧ (¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1)); d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ i - 1 = j → ↑(ω d) ^ i.val = if i - 1 = j then ↑(ω d) ^ (j.val + 1) else 0d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = j⊢ ↑(ω d) ^ i.val = if i - 1 = j then ↑(ω d) ^ (j.val + 1) else 0d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = j⊢ ↑(ω d) ^ i.val = if j = j then ↑(ω d) ^ (j.val + 1) else 0d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = j⊢ ↑(ω d) ^ i.val = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1⊢ ↑(ω d) ^ i.val = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1) d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1⊢ ↑(ω d) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ ↑(ω d) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':¬d = 1⊢ ↑(ω d) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod d⊢ ¬i - 1 = j → i - 1 = j → 0 = ↑(ω d) ^ (j.val + 1) d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ ↑(ω d) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1) nth_rw 1 [d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ ↑(ω 1) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ ↑(ω 1) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1); d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ 1 = ↑(ω d) ^ (j.val + 1); nth_rw 1 [d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ 1 = ↑(ω 1) ^ (j.val + 1)d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':d = 1⊢ 1 = ↑(ω 1) ^ (j.val + 1); All goals completed! 🐙 d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':¬d = 1⊢ ↑(ω d) ^ (j.val + ZMod.val 1) = ↑(ω d) ^ (j.val + 1) d:ℕhd:NeZero di:ZMod dj:ZMod dh:i - 1 = jh':i = j + 1hd':¬d = 1⊢ d ≠ 1; All goals completed! 🐙; d:ℕhd:NeZero di:ZMod dj:ZMod dh:¬i - 1 = jh':i - 1 = j⊢ 0 = ↑(ω d) ^ (j.val + 1); All goals completed! 🐙

And so do their powers.

Lemma4.10
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerDaan Planken

Pauli X and Z matrices satisfy the following commutation relation: Z^k X^ℓ = ω^{k·ℓ} X^ℓ Z^k.

Lean code for Lemma4.10lemma ZX_pow_eq_omega_mul_XZ (ℓ : ℕ) : Z d * (X d) ^ ℓ = ((ω d).val)^ℓ • ((X d)^ℓ * Z d) := d:ℕhd:NeZero dℓ:ℕ⊢ Z d * X d ^ ℓ = ↑(ω d) ^ ℓ • (X d ^ ℓ * Z d) induction ℓ with d:ℕhd:NeZero d⊢ Z d * X d ^ 0 = ↑(ω d) ^ 0 • (X d ^ 0 * Z d) All goals completed! 🐙 d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ Z d * X d ^ (n + 1) = ↑(ω d) ^ (n + 1) • (X d ^ (n + 1) * Z d) d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ ↑(ω d) ^ n • (X d ^ n * Z d) * X d = ↑(ω d) ^ (n + 1) • (X d ^ n * X d * Z d); d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ ↑(ω d) ^ n • (X d ^ n * (Z d * X d)) = ↑(ω d) ^ (n + 1) • (X d ^ n * X d * Z d); d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ ↑(ω d) ^ n • (X d ^ n * ↑(ω d) • (X d * Z d)) = ↑(ω d) ^ (n + 1) • (X d ^ n * X d * Z d); d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ ↑(ω d) ^ n • ↑(ω d) • (X d ^ n * (X d * Z d)) = ↑(ω d) ^ (n + 1) • (X d ^ n * X d * Z d); d:ℕhd:NeZero dn:ℕih:Z d * X d ^ n = ↑(ω d) ^ n • (X d ^ n * Z d)⊢ (↑(ω d) ^ n * ↑(ω d)) • (X d ^ n * (X d * Z d)) = ↑(ω d) ^ (n + 1) • (X d ^ n * (X d * Z d)); All goals completed! 🐙; lemma Z_pow_X_pow_eq_omega_mul_X_pow_Z_pow (k : ℕ) (ℓ : ℕ) : (Z d) ^ k * (X d) ^ ℓ = (ω d).val ^ (k * ℓ) • ((X d) ^ ℓ * (Z d) ^ k) := d:ℕhd:NeZero dk:ℕℓ:ℕ⊢ Z d ^ k * X d ^ ℓ = ↑(ω d) ^ (k * ℓ) • (X d ^ ℓ * Z d ^ k) induction k with d:ℕhd:NeZero dℓ:ℕ⊢ Z d ^ 0 * X d ^ ℓ = ↑(ω d) ^ (0 * ℓ) • (X d ^ ℓ * Z d ^ 0) All goals completed! 🐙 d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ Z d ^ (n + 1) * X d ^ ℓ = ↑(ω d) ^ ((n + 1) * ℓ) • (X d ^ ℓ * Z d ^ (n + 1)) d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ Z d * ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n) = ↑(ω d) ^ ((n + 1) * ℓ) • (X d ^ ℓ * (Z d * Z d ^ n)); d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ ↑(ω d) ^ (n * ℓ) • (Z d * (X d ^ ℓ * Z d ^ n)) = ↑(ω d) ^ ((n + 1) * ℓ) • (X d ^ ℓ * (Z d * Z d ^ n)); d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ ↑(ω d) ^ (n * ℓ) • (↑(ω d) ^ ℓ • (X d ^ ℓ * Z d) * Z d ^ n) = ↑(ω d) ^ ((n + 1) * ℓ) • (X d ^ ℓ * (Z d * Z d ^ n)); d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ ↑(ω d) ^ (n * ℓ) • ↑(ω d) ^ ℓ • (X d ^ ℓ * Z d * Z d ^ n) = ↑(ω d) ^ ((n + 1) * ℓ) • (X d ^ ℓ * (Z d * Z d ^ n)); d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ ↑(ω d) ^ (n * ℓ + ℓ) • (X d ^ ℓ * Z d * Z d ^ n) = ↑(ω d) ^ (n * ℓ + 1 * ℓ) • (X d ^ ℓ * (Z d * Z d ^ n)); d:ℕhd:NeZero dℓ:ℕn:ℕih:Z d ^ n * X d ^ ℓ = ↑(ω d) ^ (n * ℓ) • (X d ^ ℓ * Z d ^ n)⊢ X d ^ ℓ * Z d * Z d ^ n = X d ^ ℓ * (Z d * Z d ^ n); All goals completed! 🐙

And also backwards

Lean codelemma declaration uses `sorry`X_pow_Z_pow_eq_omega_mul_Z_pow_X_pow (k : ZMod d) (l : ZMod d) : (X d) ^ k.val * (Z d) ^ l.val = (ω d) ^ (-(k * l)).val • ((Z d) ^ l.val * (X d) ^ k.val) := d:ℕhd:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ (-(k * l)).val • (Z d ^ l.val * X d ^ k.val) d:ℕhd:NeZero dk:ZMod dl:ZMod d⊢ X d ^ k.val * Z d ^ l.val = ω d ^ (-(k * l)).val • ↑(ω d) ^ (l.val * k.val) • (X d ^ k.val * Z d ^ l.val); All goals completed! 🐙 -- simp [smul_smul] -- nth_rw 2 [omega_pow_n_mod_d] -- rw [← ZMod.val_mul, ← pow_add] -- rw [omega_pow_n_mod_d, ← ZMod.val_add] -- rw [mul_comm, neg_add_cancel, ZMod.val_zero] -- rw [pow_zero, one_smul]
Lemma4.11
Group: Core properties of the single-qudit Pauli matrices. (10)
Group member previews
Preview
Definition 4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
OwnerCarli Bruinsma

Powers of Pauli X and Z satisfy X^n = X^{n \mod d} Z^n = Z^{n \mod d}

Lean code for Lemma4.11theorem X_pow_n_mod_d (n : ℕ): X d ^ n = X d ^ (n % d) := pow_eq_pow_mod n (X_pow_d_eq_one d) theorem Z_pow_n_mod_d (n : ℕ): Z d ^ n = Z d ^ (n % d) := pow_eq_pow_mod n (Z_pow_d_eq_one d)
Lean codelemma X_pow_eq_mod_d (x y : ℕ) : (x % d = y % d → X d ^ x = X d ^ y ) := d:ℕhd:NeZero dx:ℕy:ℕ⊢ x % d = y % d → X d ^ x = X d ^ y d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ x = X d ^ y d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (d * (x / d) + x % d) = X d ^ y d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (d * (x / d) + x % d) = X d ^ (d * (y / d) + y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ (X d ^ d) ^ (x / d) * X d ^ (x % d) = (X d ^ d) ^ (y / d) * X d ^ (y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ 1 ^ (x / d) * X d ^ (x % d) = 1 ^ (y / d) * X d ^ (y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ X d ^ (x % d) = X d ^ (y % d) All goals completed! 🐙
Lean codelemma X_inv_pow (x : ℤ) : (X d)⁻¹ ^ x = (X d) ^ (-x) := d:ℕhd:NeZero dx:ℤ⊢ (X d)⁻¹ ^ x = X d ^ (-x) d:ℕhd:NeZero dx:ℤ⊢ IsUnit (X d).det; All goals completed! 🐙 lemma declaration uses `sorry`X_inv_pow' (x : ZMod d) : ((X d)^(x.val)).conjTranspose = (X d)^((-x).val):= d:ℕhd:NeZero dx:ZMod d⊢ (X d ^ x.val)† = X d ^ (-x).val d:ℕhd:NeZero dx:ZMod d⊢ (X d ^ x.val)⁻¹ = X d ^ (-x).val; d:ℕhd:NeZero dx:ZMod d⊢ (X d ^ x.val)⁻¹ = X d ^ if x = 0 then 0 else d - x.val; d:ℕhd:NeZero dx:ZMod dhx:x = 0⊢ (X d ^ x.val)⁻¹ = X d ^ if x = 0 then 0 else d - x.vald:ℕhd:NeZero dx:ZMod dhx:¬x = 0⊢ (X d ^ x.val)⁻¹ = X d ^ if x = 0 then 0 else d - x.val d:ℕhd:NeZero dx:ZMod dhx:x = 0⊢ (X d ^ x.val)⁻¹ = X d ^ if x = 0 then 0 else d - x.val d:ℕhd:NeZero dx:ZMod dhx:x = 0⊢ (X d ^ ZMod.val 0)⁻¹ = X d ^ if 0 = 0 then 0 else d - ZMod.val 0; All goals completed! 🐙 d:ℕhd:NeZero dx:ZMod dhx:¬x = 0⊢ (X d ^ x.val)⁻¹ = X d ^ if x = 0 then 0 else d - x.val All goals completed! 🐙 -- Matrix.zpow_neg_natCast,
Lean codelemma Z_pow_eq_mod_d : (x: ℕ) → (y: ℕ) → (x % d = y % d → Z d ^ x = Z d ^ y ) := d:ℕhd:NeZero d⊢ ∀ (x y : ℕ), x % d = y % d → Z d ^ x = Z d ^ y -- This is exactly the same proof as for X, -- maybe we can consolidate d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ x = Z d ^ y d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (d * (x / d) + x % d) = Z d ^ y d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (d * (x / d) + x % d) = Z d ^ (d * (y / d) + y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ (Z d ^ d) ^ (x / d) * Z d ^ (x % d) = (Z d ^ d) ^ (y / d) * Z d ^ (y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ 1 ^ (x / d) * Z d ^ (x % d) = 1 ^ (y / d) * Z d ^ (y % d) d:ℕhd:NeZero dx:ℕy:ℕh:x % d = y % d⊢ Z d ^ (x % d) = Z d ^ (y % d) All goals completed! 🐙
Lean codelemma Z_inv_pow (x : ℤ) : (Z d)⁻¹ ^ x = (Z d) ^ (-x) := d:ℕhd:NeZero dx:ℤ⊢ (Z d)⁻¹ ^ x = Z d ^ (-x) d:ℕhd:NeZero dx:ℤ⊢ IsUnit (Z d).det; All goals completed! 🐙 lemma declaration uses `sorry`Z_inv_pow' : (x: ZMod d) → ((Z d)^(x.val)).conjTranspose = (Z d)^((-x).val):= d:ℕhd:NeZero d⊢ ∀ (x : ZMod d), (Z d ^ x.val)† = Z d ^ (-x).val -- This is exactly the same proof as for X, -- maybe we can consolidate d:ℕhd:NeZero dx:ZMod d⊢ (Z d ^ x.val)† = Z d ^ (-x).val; d:ℕhd:NeZero dx:ZMod d⊢ (Z d ^ x.val)⁻¹ = Z d ^ (-x).val; All goals completed! 🐙 --rw [(Nat.mod_eq_of_lt (ZMod.val_lt (-x)))]