Rigorous verification of formal chaos produced by one-dimensional discrete dynamical system with use of interval arithmetic

Definitions of chaos and its observability for 1D mapping systems are briefly reviewed. This paper provides a theorem guaranteeing that formal chaos exists in 1D mapping system based on one dimensional horseshoe map geometrical structure, and also provides algorithms verifying the conditions in the theorem with the use of interval arithmetic. Further this paper discusses the effectiveness of the approach through an example of a transmission line circuit with nonlinear boundary conditions.