Computer-assisted proof of a periodic solution in a nonlinear feedback DDE

Abstract

In this paper, we rigorously prove the existence
of a non-trivial periodic orbit for the nonlinear DDE:
$x'(t) = - K \sin(x(t-1))$ for $K=1.6$. We show that the equations for
the Fourier coefficients have a solution by computing the local Brouwer
degree. This degree can be
computed by using a homotopy, and its validity can be proved by checking
a finite number of inequalities. Checking these inequalities is done by
a computer program.