5. Displacement operators
This section uses the generalized Pauli X and Z matrices to define the displacement operators D_{x,z}.
These operators effectively constitute the generalized Pauli or Weyl–Heisenberg group on a single quantum system of dimension d.
Unless stated otherwise, we assume that d ≥ 1.
Lean code
variable (d : ℕ) [NeZero d]
We use the generalized Pauli X and Z to define the displacement operators, see Eq. (8) in Appleby (2005).
Definition5.46
The displacement operator corresponding to x,z ∈ ℤ is defined as
D_{x,z} = τ^{xz} X^x Z^z
where τ comes from Definition 2.10, X comes from Definition 4.29, and Z comes from Definition 4.32.
Displacement operators behave nicely under complex conjugation, see Eq. (9) in Appleby (2005).
Lemma5.47
Group: Core properties of the single-qudit Pauli group. (7)
Preview
Definition 5.46
Associated Lean declarations
-
conjTranspose_D[sorry in proof]
For all x,z ∈ ℤ,
D_{x,z}^† = D_{-x,-z}
where \dagger denotes the conjugate transpose.
Lean code for Lemma5.47
Associated Lean declarations
-
conjTranspose_D[sorry in proof]
Associated Lean declarations
-
conjTranspose_D[sorry in proof]
lemma conjTranspose_D (x z : ℤ) :
(D d x z).conjTranspose = D d (-x) (-z) := d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (D d ↑x ↑z).conjTranspose = D d (-↑x) (-↑z)
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (τ d ^ ((↑x).val * (↑z).val) • X d ^ (↑x).val * Z d ^ (↑z).val).conjTranspose =
τ d ^ ((-↑x).val * (-↑z).val) • X d ^ (-↑x).val * Z d ^ (-↑z).val
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (τ d ^ ((↑x).val * (↑z).val) • (X d ^ (↑x).val * Z d ^ (↑z).val)).conjTranspose =
τ d ^ ((-↑x).val * (-↑z).val) • X d ^ (-↑x).val * Z d ^ (-↑z).val
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (τ d ^ ((↑x).val * (↑z).val) • ω d ^ (-(↑x * ↑z)).val • (Z d ^ (↑z).val * X d ^ (↑x).val)).conjTranspose =
τ d ^ ((-↑x).val * (-↑z).val) • X d ^ (-↑x).val * Z d ^ (-↑z).val
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) •
star (ω d ^ (-(↑x * ↑z)).val) • ((X d ^ (↑x).val).conjTranspose * (Z d ^ (↑z).val).conjTranspose) =
τ d ^ ((-↑x).val * (-↑z).val) • X d ^ (-↑x).val * Z d ^ (-↑z).val
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (ω d ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • X d ^ (-↑x).val * Z d ^ (-↑z).val
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (ω d ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (ω d ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (ω d ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star ((τ d ^ 2) ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
nth_rw 2 [star_powd:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (τ d ^ 2) ^ (-(↑x * ↑z)).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
nth_rw 2 [pow_muld:ℕinst✝:NeZero dx:ℤz:ℤ⊢ star (τ d ^ ((↑x).val * (↑z).val)) • star (τ d ^ 2) ^ (-(↑x * ↑z)).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
(τ d ^ (-↑x).val) ^ (-↑z).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
have tau_star_nat
(d : ℕ) (n : ℕ) [NeZero d] :
star (τ d ^ n) = τ d^(-(n: ℤ)) := d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (D d ↑x ↑z).conjTranspose = D d (-↑x) (-↑z)
d✝:ℕinst✝¹:NeZero dx:ℤz:ℤd:ℕn:ℕinst✝:NeZero dh:star (τ d ^ ↑n) = τ d ^ (-↑n)⊢ star (τ d ^ n) = τ d ^ (-↑n)
d✝:ℕinst✝¹:NeZero dx:ℤz:ℤd:ℕn:ℕinst✝:NeZero dh:star (τ d ^ n) = τ d ^ (-↑n)⊢ star (τ d ^ n) = τ d ^ (-↑n)
All goals completed! 🐙
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)⊢ τ d ^ (-↑((↑x).val * (↑z).val)) • (τ d ^ (-↑2)) ^ (-(↑x * ↑z)).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
(τ d ^ (-↑x).val) ^ (-↑z).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)⊢ (τ d ^ (-↑((↑x).val * (↑z).val)) • (τ d ^ (-↑2)) ^ (-(↑x * ↑z)).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
(τ d ^ (-↑x).val) ^ (-↑z).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
-- This is a insane bodge, but this way lean can do the casts...
have hh (z : ℂ ) (a: ℤ ) (b: ℕ ): z ^(a*b) = (z^a)^b :=d:ℕinst✝:NeZero dx:ℤz:ℤ⊢ (D d ↑x ↑z).conjTranspose = D d (-↑x) (-↑z)
All goals completed! 🐙
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ (τ d ^ (-↑((↑x).val * (↑z).val)) • τ d ^ (-↑2 * ↑(-(↑x * ↑z)).val)) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
(τ d ^ (-↑x).val) ^ (-↑z).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ (τ d ^ (-↑((↑x).val * (↑z).val)) * τ d ^ (-↑2 * ↑(-(↑x * ↑z)).val)) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
(τ d ^ (-↑x).val) ^ (-↑z).val • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ (τ d ^ (-↑((↑x).val * (↑z).val)) * τ d ^ (-↑2 * ↑(-(↑x * ↑z)).val)) • (X d ^ (-↑x).val * Z d ^ (-↑z).val) =
τ d ^ ((-↑x).val * (-↑z).val) • (X d ^ (-↑x).val * Z d ^ (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ τ d ^ (-↑((↑x).val * (↑z).val)) * τ d ^ (-↑2 * ↑(-(↑x * ↑z)).val) = τ d ^ ((-↑x).val * (-↑z).val)
nth_rw 3 [mul_commd:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ τ d ^ (-↑((↑x).val * (↑z).val)) * τ d ^ (↑(-(↑x * ↑z)).val * -↑2) = τ d ^ ((-↑x).val * (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ τ d ^ (-↑((↑x).val * (↑z).val)) * τ d ^ (-↑((-(↑x * ↑z)).val * 2)) = τ d ^ ((-↑x).val * (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ τ d ^ (-↑((↑x).val * (↑z).val) + -↑((-(↑x * ↑z)).val * 2)) = τ d ^ ((-↑x).val * (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ τ d ^ (-↑((↑x).val * (↑z).val) + -↑((-(↑x * ↑z)).val * 2)) = τ d ^ ((-↑x).val * (-↑z).val)
d:ℕinst✝:NeZero dx:ℤz:ℤtau_star_nat:∀ (d n : ℕ) [NeZero d], star (τ d ^ n) = τ d ^ (-↑n)hh:∀ (z : ℂ) (a : ℤ) (b : ℕ), z ^ (a * ↑b) = (z ^ a) ^ b⊢ (-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ (-↑((↑x).val * (↑z).val) + -↑((-(↑x * ↑z)).val * 2)) =
(-Complex.exp (↑Real.pi * Complex.I / ↑d)) ^ ((-↑x).val * (-↑z).val)
All goals completed! 🐙
/-
--rw [Matrix.conjTranspose_apply]
--unfold Matrix.conjTranspose_mul
--rw [Matrix.conjTranspose_mul]
simp only [star_pow, star_neg, RCLike.star_def]
--unfold τ
--rw [starRingEnd_apply]
#check starRingEnd
#check star_pow
#check star_neg
--rw[star_neg]
--simp only [RCLike.star_def]
--simp only [RCLike.star_def, even_two, Even.neg_pow]
rw[ ← Complex.exp_conj]
#check neg_pow
simp only [map_div₀, map_mul, Complex.conj_ofReal, Complex.conj_I, mul_neg, map_natCast]
rw [neg_pow]
rw [(neg_pow (Complex.exp (↑Real.pi * Complex.I / ↑d))
((-(x : ZMod d)).val * (-(z : ZMod d)).val))] -- Somehow here we have to specify....
rw [← Complex.exp_nat_mul]
rw [← Complex.exp_nat_mul]
rw [ZMod.val_mul]
#check neg_one_pow_congr
--rw [← Complex.exp_nsmul,← Complex.exp_int_mul, ← Complex.exp_neg]
#check neg_mul
-- rw [neg_smul, ← Complex.exp_int_mul, ← Complex.exp_add]
-/
Multiplication of displacement operators corresponds to adding their subscripts and introducing a phase given by the symplectic inner product, see Eq. (10) in Appleby (2005).
Lemma5.48
For all \p, \q ∈ ℤ^2,
D_\p D_\q = τ^{\braket{\p,\q}} D_{\p+\q}
where τ is the root of unity from Definition 2.10 and \braket{\cdot,\cdot} is the symplectic inner product from Definition 3.2.
Lean code for Lemma5.48
Associated Lean declarations
-
D_mul[sorry in proof]
Associated Lean declarations
-
D_mul[sorry in proof]
lemma D_mul (p q : ZMod d × ZMod d) :
(D d p.1 p.2) * (D d q.1 q.2) =
τ d ^ (symp p q).val •
D d (p.1 + q.1) (p.2 + q.2) := d:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod d⊢ D d p.1 p.2 * D d q.1 q.2 = τ d ^ (symp p q).val • D d (p.1 + q.1) (p.2 + q.2)
All goals completed! 🐙
The n-th power of a displacement operator is again a displacement operator.
Lemma5.49
Group: Core properties of the single-qudit Pauli group. (7)
Preview
Definition 5.46
Associated Lean declarations
-
D_pow_nsmul[complete]
Used by 3
Preview
Lemma 5.52
For all \p \in ℤ^2 and n \geq 0,
D_\p^n = D_{n\p}.
Proof
We proceed by induction on n. The base case n = 0 gives D_\p^0 = I = D_\mathbf{0}. For the inductive step, assuming D_\p^n = D_{n\p} we get
D_\p^{n+1} = D_\p^n · D_\p = D_{n\p} \cdot D_\p = \tau^{\langle n\p,\p\rangle} D_{(n+1)\p},
where the last step used Lemma 5.48.
The result follows since \langle n\p,\p\rangle = n \langle\p,\p\rangle = 0 thanks to Lemma 3.4.
Lean code for Lemma5.49
Associated Lean declarations
-
D_pow_nsmul[complete]
Associated Lean declarations
-
D_pow_nsmul[complete]
lemma D_pow_nsmul (p : ZMod d × ZMod d) (n : ℕ) :
D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2 := d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕ⊢ D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2
induction n with
d:ℕinst✝:NeZero dp:ZMod d × ZMod d⊢ D d p.1 p.2 ^ 0 = D d (0 • p).1 (0 • p).2
d:ℕinst✝:NeZero dp:ZMod d × ZMod d⊢ 1 = D d 0.1 0.2
d:ℕinst✝:NeZero dp:ZMod d × ZMod d⊢ 1 = τ d ^ (0.1.val * 0.2.val) • X d ^ 0.1.val * Z d ^ 0.2.val
All goals completed! 🐙
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2⊢ D d p.1 p.2 ^ (n + 1) = D d ((n + 1) • p).1 ((n + 1) • p).2
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2⊢ D d (n • p).1 (n • p).2 * D d p.1 p.2 = D d ((n + 1) • p).1 ((n + 1) • p).2
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2⊢ τ d ^ (symp (n • p) p).val • D d ((n • p).1 + p.1) ((n • p).2 + p.2) = D d ((n + 1) • p).1 ((n + 1) • p).2
have h : symp ( n • p) p = 0 := d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕ⊢ D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2⊢ (n • p).2 * p.1 - (n • p).1 * p.2 = 0; d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2⊢ ↑n * p.2 * p.1 - ↑n * p.1 * p.2 = 0; All goals completed! 🐙
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2h:symp (n • p) p = 0⊢ D d ((n • p).1 + p.1) ((n • p).2 + p.2) = D d ((n + 1) • p).1 ((n + 1) • p).2
d:ℕinst✝:NeZero dp:ZMod d × ZMod dn:ℕih:D d p.1 p.2 ^ n = D d (n • p).1 (n • p).2h:symp (n • p) p = 0⊢ D d (↑n * p.1 + p.1) (↑n * p.2 + p.2) = D d ((↑n + 1) * p.1) ((↑n + 1) * p.2); All goals completed! 🐙
If d is odd, adding a multiple of d to the index of a displacement operator does not change it, see Eq. (11) in Appleby (2005).
Lemma5.50
✓L∃∀N
Associated Lean declarations
-
D_add_nsmul[complete]
Used by 2
Preview
Lemma 5.51
If d is odd then D_{\p+d\q} = D_{\p} for all \p, \q ∈ ℤ^2.
Lean code for Lemma5.50
Associated Lean declarations
-
D_add_nsmul[complete]
Associated Lean declarations
-
D_add_nsmul[complete]
lemma D_add_nsmul (p q : ZMod d × ZMod d) (hodd : Odd d) :
D d (p.1 + d * q.1) (p.2 + d * q.2)
= D d p.1 p.2 := d:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ D d (p.1 + ↑d * q.1) (p.2 + ↑d * q.2) = D d p.1 p.2
d:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ τ d ^ ((p.1 + ↑d * q.1).val * (p.2 + ↑d * q.2).val) • X d ^ (p.1 + ↑d * q.1).val * Z d ^ (p.2 + ↑d * q.2).val =
τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val
d:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ Odd dd:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ Odd d
d:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ Odd dd:ℕinst✝:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dhodd:Odd d⊢ Odd d All goals completed! 🐙 -- for tau_pow_n_mod_d_of_d_odd
If d is odd, the index \p of a displacement operator D_\p can be treated modulo d.
In other words, it makes sense to write \p \in ℤ_d^2.
Lemma5.51
If d is odd, then for all \p \in ℤ^2,
D_\p = D_{\p \pmod d}.
Proof
This is a direct consequence of Lemma 5.50
Lean code for Lemma5.51
Associated Lean declarations
-
D_mod_d[sorry in proof]
Associated Lean declarations
-
D_mod_d[sorry in proof]
@[default_instance]
instance : EuclideanDomain ℤ := Int.euclideanDomain
lemma D_mod_d (p : ZMod d × ZMod d) (hodd : Odd d):
D d p.1 p.2 = D d p.1 p.2 :=
sorry
/-
by calc
D d p.1 p.2 =
D d (p.1 % d + d * (p.1 / d))
(p.2 % d + d * (p.2 / d))
:= by rw[EuclideanDomain.mod_add_div p.1];
rw[EuclideanDomain.mod_add_div p.2]
_ = D d (p.1 % d) (p.2 % d)
:= D_add_nsmul d (p.1 % d, p.2 % d)
(p.1 / d, p.2 / d) hodd
-/
The displacement operators have order d.
Lemma5.52
Group: Core properties of the single-qudit Pauli group. (7)
Preview
Definition 5.46
Associated Lean declarations
-
D_pow_d_eq_one[sorry in proof]
Used by 2
Preview
Theorem 7.1
If d is odd, then for all \p \in ℤ^2,
D_\p^d = I.
Proof
By Lemma 5.49, D_\p^d = D_{d\p} = D_\mathbf{0} = I, using d\p = \mathbf{0} in ℤ_d^2.
Lean code for Lemma5.52
Associated Lean declarations
-
D_pow_d_eq_one[sorry in proof]
Associated Lean declarations
-
D_pow_d_eq_one[sorry in proof]
lemma D_pow_d_eq_one (p : ZMod d × ZMod d) (hOdd : Odd d) :
D d p.1 p.2 ^ d = 1 :=
d:ℕinst✝:NeZero dp:ZMod d × ZMod dhOdd:Odd d⊢ D d p.1 p.2 ^ d = 1 All goals completed! 🐙
/-rw [D_pow_nsmul]; calc
D d (d • p).1 (d • p).2 =
D d ((d • p).1 % d) ((d • p).2 % d)
:= D_mod_d d (d • p) hOdd
_ = D d 0 ((d • p).2 % d)
:= by simp
_ = D d 0 0
:= by simp
_ = 1 := by unfold D; simp
-/
Displacement operators with different \p (modulo d) are indeed different.
Lemma5.53
Group: Core properties of the single-qudit Pauli group. (7)
Preview
Definition 5.46
Associated Lean declarations
-
D_p_neq_D_q[complete]
Let \p,\q \in ℤ^2 and assume α,β ∈ ℂ are both non-zero.
If
α D_\p = β D_\q
then \p \equiv \q \pmod{d}.
Proof
This theorem always holds when d = 1.
For d > 1, (to be continues... from the assumption, you work out the matrices, take the diagonal entries at 0 and 1, and find your proof)
Lean code for Lemma5.53
Associated Lean declarations
-
D_p_neq_D_q[complete]
Associated Lean declarations
-
D_p_neq_D_q[complete]
lemma D_p_neq_D_q
(p q : ZMod d × ZMod d)
(α β : ℂ) [NeZero α] [NeZero β] :
α • (D d p.1 p.2) = β • (D d q.1 q.2) →
p.1 = q.1 ∧ p.2 = q.2 := d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val) →
p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val)⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val)hd:d = 1⊢ p.1 = q.1 ∧ p.2 = q.2d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val)hd:¬d = 1⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val)hd:d = 1⊢ p.1 = q.1 ∧ p.2 = q.2 α:ℂβ:ℂinst✝²:NeZero αinst✝¹:NeZero βinst✝:NeZero 1p:ZMod 1 × ZMod 1q:ZMod 1 × ZMod 1h:α • (τ 1 ^ (p.1.val * p.2.val) • X 1 ^ p.1.val * Z 1 ^ p.2.val) =
β • (τ 1 ^ (q.1.val * q.2.val) • X 1 ^ q.1.val * Z 1 ^ q.2.val)⊢ p.1 = q.1 ∧ p.2 = q.2
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:α • (τ d ^ (p.1.val * p.2.val) • X d ^ p.1.val * Z d ^ p.2.val) =
β • (τ d ^ (q.1.val * q.2.val) • X d ^ q.1.val * Z d ^ q.2.val)hd:¬d = 1⊢ p.1 = q.1 ∧ p.2 = q.2 d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βh:(α * τ d ^ (p.1.val * p.2.val)) • X d ^ p.1.val * Z d ^ p.2.val =
(β * τ d ^ (q.1.val * q.2.val)) • X d ^ q.1.val * Z d ^ q.2.valhd:¬d = 1⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:(α * τ d ^ (p.1.val * p.2.val)) • X d ^ p.1.val * Z d ^ p.2.val * Z d ^ (-p.2).val =
(β * τ d ^ (q.1.val * q.2.val)) • X d ^ q.1.val * Z d ^ q.2.val * Z d ^ (-p.2).val⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:(α * τ d ^ (p.1.val * p.2.val)) • X d ^ p.1.val =
(β * τ d ^ (q.1.val * q.2.val)) • X d ^ q.1.val * Z d ^ (q.2 - p.2).val⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:X d ^ (-q.1).val * (α * τ d ^ (p.1.val * p.2.val)) • X d ^ p.1.val =
X d ^ (-q.1).val * ((β * τ d ^ (q.1.val * q.2.val)) • X d ^ q.1.val * Z d ^ (q.2 - p.2).val)⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:(α * τ d ^ (p.1.val * p.2.val)) • X d ^ (p.1 - q.1).val = (β * τ d ^ (q.1.val * q.2.val)) • Z d ^ (q.2 - p.2).val⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • X d ^ (p.1 - q.1).val) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Z d ^ (q.2 - p.2).val) i j⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i j⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) 0 0 =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) 0 0⊢ p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)⊢ p.1 = q.1 ∧ p.2 = q.2
have h1 : p.1 - q.1 = 0 := d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1':¬p.1 - q.1 = 0⊢ False
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:0 = β * τ d ^ (q.1.val * q.2.val)h1':¬p.1 - q.1 = 0⊢ False
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:0 = β * τ d ^ (q.1.val * q.2.val)h1':¬p.1 - q.1 = 0h_false:0 ≠ β * τ d ^ (q.1.val * q.2.val)⊢ False
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.1 = q.1d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.1 = q.1 d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ (fun x => x - q.1) p.1 = (fun x => x - q.1) q.1
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.1 - q.1 = q.1 - q.1
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.1 - q.1 = 0
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:(α * τ d ^ (p.1.val * p.2.val) * if p.1 - q.1 = 0 then 1 else 0) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.2 = q.2 d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1h:∀ (i j : ZMod d),
((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) i j =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) i jhphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:((α * τ d ^ (p.1.val * p.2.val)) • Matrix.of fun i j => if j + (p.1 - q.1).cast = i then 1 else 0) 1 1 =
((β * τ d ^ (q.1.val * q.2.val)) • Matrix.diagonal fun i => ω d ^ (i.val * (q.2 - p.2).val)) 1 1⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:α * τ d ^ (p.1.val * p.2.val) = α * τ d ^ (p.1.val * p.2.val) * ω d ^ (q.2 - p.2).val⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val)) =
(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val) * ω d ^ (q.2 - p.2).val)⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val)) =
(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val) * ω d ^ (q.2 - p.2).val)c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0⊢ p.2 = q.2
have c2 : 2 * ↑Real.pi * Complex.I ≠ (0 : ℂ)
:= d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2 All goals completed! 🐙
have c3 : 2 * ↑Real.pi * Complex.I / ↑d ≠ (0 : ℂ)
:= d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val)) =
(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val) * ω d ^ (q.2 - p.2).val)c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0⊢ 0 < Complex.normSq (2 * ↑Real.pi * Complex.I / ↑d)
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val)) =
(α * τ d ^ (p.1.val * p.2.val))⁻¹ * (α * τ d ^ (p.1.val * p.2.val) * ω d ^ (q.2 - p.2).val)c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0⊢ ¬d = 0
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:1 = ω d ^ (q.2 - p.2).valc1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:1 = Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ^ (q.2 - p.2).valc1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:Complex.exp (2 * ↑Real.pi * Complex.I / ↑d) ^ (q.2 - p.2).val = 1c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0h:Complex.exp (↑(q.2 - p.2).val * (2 * ↑Real.pi * Complex.I / ↑d)) = 1c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0h:∃ n, ↑(q.2 - p.2).val * (2 * ↑Real.pi * Complex.I / ↑d) = ↑n * (2 * ↑Real.pi * Complex.I)⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val * (2 * ↑Real.pi * Complex.I / ↑d) = ↑n * (2 * ↑Real.pi * Complex.I)⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val * (2 * ↑Real.pi * Complex.I / ↑d) * (2 * ↑Real.pi * Complex.I / ↑d)⁻¹ =
↑n * (2 * ↑Real.pi * Complex.I) * (2 * ↑Real.pi * Complex.I / ↑d)⁻¹⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑d⊢ p.2 = q.2
have hn_int : ((q.2 - p.2).val : ℤ) = n * d := d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑d⊢ p.2 = q.2
have h_ub : n ≤ 0 := d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2 -- n * ↑d < d := by
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑d⊢ n ≤ 1 - 1
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑d⊢ n < 1
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑d⊢ n * ↑d < ↑d
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑d⊢ ↑(q.2 - p.2).val < ↑d
All goals completed! 🐙
have h_lb : 0 ≤ n * ↑d := d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero β⊢ α • D d p.1 p.2 = β • D d q.1 q.2 → p.1 = q.1 ∧ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑dh_ub:n ≤ 0⊢ 0 ≤ ↑(q.2 - p.2).val
All goals completed! 🐙
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = n * ↑dhd:0 < ↑dh_ub:n ≤ 0h_lb✝:0 ≤ n * ↑dh_lb:0 ≤ n⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = 0hd:0 < ↑dh_ub:n ≤ 0h_lb✝:0 ≤ n * ↑dh_lb:0 ≤ n⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = 0hd:0 < ↑dh_ub:n ≤ 0h_lb✝:0 ≤ n * ↑dh_lb:0 ≤ nh2:q.2 - p.2 = 0⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = 0hd:0 < ↑dh_ub:n ≤ 0h_lb✝:0 ≤ n * ↑dh_lb:0 ≤ nh2:q.2 - p.2 + p.2 = 0 + p.2⊢ p.2 = q.2
d:ℕinst✝²:NeZero dp:ZMod d × ZMod dq:ZMod d × ZMod dα:ℂβ:ℂinst✝¹:NeZero αinst✝:NeZero βhd✝:¬d = 1hphase:α * τ d ^ (p.1.val * p.2.val) = β * τ d ^ (q.1.val * q.2.val)h1:p.1 - q.1 = 0c1:α * τ d ^ (p.1.val * p.2.val) ≠ 0c2:2 * ↑Real.pi * Complex.I ≠ 0c3:2 * ↑Real.pi * Complex.I / ↑d ≠ 0n:ℤhn:↑(q.2 - p.2).val = ↑n * ↑dhn_int:↑(q.2 - p.2).val = 0hd:0 < ↑dh_ub:n ≤ 0h_lb✝:0 ≤ n * ↑dh_lb:0 ≤ nh2:q.2 = p.2⊢ p.2 = q.2
All goals completed! 🐙
Displacement operators with phases that are arbitrary powers of τ form a group.
Definition5.54
Group: Core properties of the single-qudit Pauli group. (7)
Preview
Definition 5.46
Associated Lean declarations
-
pauliGroup[sorry in proof]
The generalized Pauli group or discrete Weyl–Heisenberg group consists of
\GP(d) = \{τ^a D_\p : a ∈ ℤ_d, \p ∈ ℤ_d^2\}
where τ is from Definition 2.10 and D_\p is from Definition 5.46.
Lean code for Definition5.54
Associated Lean declarations
-
pauliGroup[sorry in proof]
Associated Lean declarations
-
pauliGroup[sorry in proof]
def pauliGroup (d : ℕ) [NeZero d] :
Subgroup (Matrix.unitaryGroup (ZMod d) ℂ) where
carrier := {U | ∃ (a : ZMod d) (p : ZMod d × ZMod d),
(U : Matrix (ZMod d) (ZMod d) ℂ) =
(τ d) ^ a.val • D d (p.1.val : ℤ) (p.2.val : ℤ)}
one_mem' := d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 ∈ {U | ∃ a p, ↑U = τ d ^ a.val • D d ↑↑p.1.val ↑↑p.2.val} d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ ∃ p, ↑1 = τ d ^ ZMod.val 0 • D d ↑↑p.1.val ↑↑p.2.val; d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ ↑1 = τ d ^ ZMod.val 0 • D d ↑↑(0, 0).1.val ↑↑(0, 0).2.val; d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 = D d 0 0; d✝:ℕinst✝¹:NeZero d✝d:ℕinst✝:NeZero d⊢ 1 = τ d ^ (ZMod.val 0 * ZMod.val 0) • X d ^ ZMod.val 0 * Z d ^ ZMod.val 0; All goals completed! 🐙
mul_mem' := @fun A B A' B' => sorry -- Need 5.30
inv_mem' := sorry
We could have equivalently written
\GP(d) = \{τ^a X^x Z^z : a,x,z ∈ ℤ_d\}
where X and Z are the generalized Pauli matrices.
The generalized Pauli group \GP(d) modulo its center \{\tau^a I : a \in \Z_d\} is isomorphic to ℤ_d^2.