Lean, informalized

Nielsen & Chuang · Chapter 4, Quantum circuits · p. 198

Exercise 4.42 - An angle whose cosine is three fifths is an irrational multiple of a full turn

Cosine three fifths gives an irrational fraction of a turn.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

A rotation Rnˆ(θ)R_{\hat n}(\theta) of the Bloch sphere about an axis nˆ\hat n, applied over and over, comes back to the identity after finitely many steps exactly when θ\theta is a rational multiple of 2π2\pi. The exercise takes an angle θ\theta with cos⁡θ=3/5\cos\theta = 3/5, for instance the angle of a right triangle with sides 33, 44 and 55 that lies opposite the side of length 44, and asks to show that it is not such a multiple: that θ/2π\theta/2\pi is irrational, not a quotient of two integers.✦

The Claim

Theorem 1. Let θ\theta be a real number with cos⁡θ=3/5\cos\theta = 3/5. Then θ2π∉ℚ.\frac{\theta}{2\pi} \notin \mathbb{Q}.(1)✦

What Is Checked

Its angle θ\theta is any real solution of cos⁡θ=3/5\cos\theta = 3/5, not only the acute one.