phases_require_complex

formal source

 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 _
 148    have h2 : (k.val : ℤ) < 8 := by omega
 149    omega
 150  cases h_n_range with
 151  | inl h0 =>
 152    simp only [h0, mul_zero, Int.cast_zero] at h_eq
 153    have : k.val = 0 := by omega
 154    exact hk.left this
 155  | inr h1 =>
 156    simp only [h1, mul_one, Int.cast_one] at h_eq
 157    have : k.val = 4 := by omega
 158    exact hk.right this