phases_require_complex_k2

formal source

 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]
 135  simp only [Complex.add_im, Complex.mul_I_im, Complex.ofReal_im, Complex.ofReal_re, zero_add]
 136  -- sin(k * π / 4) ≠ 0 when k ∉ {0, 4}
 137  intro h_sin
 138  rw [Real.sin_eq_zero_iff] at h_sin
 139  rcases h_sin with ⟨n, hn⟩
 140  -- k * π / 4 = n * π implies k = 4n
 141  have h_eq : (k.val : ℤ) = 4 * n := by
 142    have : (k.val : ℝ) * π / 4 = n * π := hn.symm
 143    field_simp [Real.pi_ne_zero] at this
 144    exact_mod_cast this
 145  -- k ∈ {0,...,7} and k = 4n implies n ∈ {0, 1}, hence k ∈ {0, 4}
 146  have h_n_range : n = 0 ∨ n = 1 := by
 147    have h1 : 0 ≤ (k.val : ℤ) := Int.natCast_nonneg _