A Computer-Assisted Proof of Σ3-Chaos in the Forced Damped Pendulum Equation

The present paper is devoted to studying Hubbard's pendulum equation x + 10(-1)x + sin(x) = cos(t). Using rigorous/interval methods of computation, the main assertion of Hubbard on chaos properties of the induced dynamics is raised from the level of experimentally observed facts to the level of a theorem completely proved. A special family of solutions is shown to be chaotic in the sense that, on consecutive time intervals (2k pi, 2(k + 1)pi) (k is an element of Z), individual members of the family can freely "choose" between the following possibilities: the pendulum crosses the bottom position exactly once clockwise or does not cross the bottom position at all or crosses the bottom position exactly once counterclockwise. The proof follows the topological index/degree approach by Mischaikow, Mrozek, and Zgliczynski. The new feature of this paper is a definition of the transition graph for which the periodic orbit lemma-the key technical result of the approach mentioned above-turns out to be a consequence of Brouwer's fixed point theorem. The role of wholly automatic versus "trial-and-error with human overheads" computer procedures in detecting chaos is also discussed.