phases_require_complex_k1

formal source

 101
 102/-- **THEOREM**: 8-tick phases require rotation, which requires ℂ.
 103    The first non-trivial phase (k=1) has nonzero imaginary part. -/
 104theorem phases_require_complex_k1 : (tickPhase ⟨1, by omega⟩).im ≠ 0 := by
 105  unfold tickPhase
 106  -- exp(I * π / 4) = cos(π/4) + I * sin(π/4)
 107  have h : I * ↑π * ↑(1 : ℕ) / 4 = ↑(π / 4 : ℝ) * I := by push_cast; ring
 108  simp only [show (⟨1, by omega⟩ : Fin 8).val = 1 from rfl] at *
 109  rw [h, Complex.exp_mul_I]
 110  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
 111  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
 112  -- sin(π/4) = √2/2 ≠ 0
 113  rw [Real.sin_pi_div_four]
 114  exact ne_of_gt (by positivity)
 115
 116/-- The phase at k=2 (which is π/2) also has nonzero imaginary part. -/
 117theorem phases_require_complex_k2 : (tickPhase ⟨2, by omega⟩).im ≠ 0 := by
 118  unfold tickPhase
 119  have h : I * ↑π * ↑(2 : ℕ) / 4 = ↑(π / 2 : ℝ) * I := by push_cast; ring
 120  simp only [show (⟨2, by omega⟩ : Fin 8).val = 2 from rfl] at *
 121  rw [h, Complex.exp_mul_I]
 122  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]
 123  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
 124  rw [Real.sin_pi_div_two]
 125  norm_num
 126
 127/-- General statement: for k ∈ {1,2,3,5,6,7}, the tick phase has nonzero imaginary part. -/
 128theorem phases_require_complex (k : Fin 8) (hk : k.val ≠ 0 ∧ k.val ≠ 4) :
 129    (tickPhase k).im ≠ 0 := by
 130  -- For phases 1,2,3,5,6,7, sin(k*π/4) ≠ 0
 131  unfold tickPhase
 132  have h_exp : I * π * k / 4 = ↑((k.val : ℝ) * π / 4 : ℝ) * I := by push_cast; ring
 133  rw [h_exp, Complex.exp_mul_I]
 134  rw [← Complex.ofReal_cos, ← Complex.ofReal_sin]