{'fraction_non_alphanumeric': 0.038815937329437826, 'fraction_numerical': 0.010530709217581147, 'mean_word_length': 3.8767809613276967, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Uniformly hyperbolic attractor of the Smale-Williams type for a Poincar\'e map in the Kuznetsov system

We propose a general algorithm for computer assisted verification of uniform hyperbolicity for maps which exhibit a robust attractor. The method has been successfully applied to a Poincare map for a system of coupled non-autonomous van der Pol oscillators. The model equation has been proposed by Kuznetsov and the attractor seems to be of the Smale-Williams type.


Introduction.
Hyperbolic systems of dissipative type, contracting the phase space volume, manifest robust attractors. That means that the dynamics does not change qualitatively when the parameters of the system vary in some range.
There are several models of maps which produce hyperbolic nontrivial attractor -like the Plykin attractor [P] or the Smale solenoid [KH]. But for long time there were no examples of continuous systems that apparently have hyperbolic strange attractors.
Recently, Kuznetsov [K] proposed a continuous model that exhibits an uniformly hyperbolic attractor of the Smale-Williams type in the Poincaré map. This is a nonautonomous system in R 4 and it is constructed on a basis of two coupled van der Pol oscillators: (1) Let P denote the Poincaré map of the above system defined naturally as the shift along the trajectories over the period of the vector field (2) P (x, u, y, v) = (x (T ), u(T ), y (T ), v(T )) .
Kuznetsov and Sataev [KS] gave a deep numerical study of this system and observed that for some range of parameter values there is an absorbing domain for P of the toroidal shape as presented in Figure 1, left panel. This domain is a product of a 3D ball and a circle. The observed attractor is of the Smale-Williams type. Numerical studies [K, KS, KSe] gave a strong numerical evidence of the existence of uniformly hyperbolic attractor for some range of parameter values around (3) ω 0 = 2π, A = 5, T = 6, ε = 0.5 -see Figure 1 right panel, where the unstable and stable foliations are presented. In this paper we propose a method for computer assisted verification that a map possesses an uniformly hyperbolic attractor. As a test case we apply the method to the model map proposed by Smale [KH]. This is a map defined on the twodimensional solid torus and it is analytically proved to be uniformly hyperbolic.
Although the method is general, the main motivation for us to undertake this study was to prove Kuznetsov's conjecture about the hyperbolicity of the system (1). The following theorem is the main result of this paper.
Theorem 1. Consider the system (1) with the parameter values (3). Let P denote the Poincaré map for this system as defined in (2). There exists a compact, connected and explicitly given set B such that (1) B is positive invariant with respect to P , i.e. P (B) ⊂ B, (2) P is uniformly hyperbolic on the maximal invariant set A = i>0 P i (B) with one positive and three negative Lyapunov exponents.
After a linear change of coordinates the set B is a union of 7 970 392 fourdimensional explicitly given cubes. The set B is a very narrow enclosure of A as presented in Figure 3. Note, the coordinates (x 0 , x 1 , x 2 , x 3 ) are related to (x, u, y, v) by a linear change of coordinates.
The above theorem implies that the set A = i>0 P i (B) is compact and connected. The following theorem implies that it is a non-trivial continuum.
Theorem 2. The set A contains at least one fixed point and one period-two orbit for P .
In the literature there are already algorithms for computer assisted verification of uniform hyperbolicity and enclosure of attractors. The very pioneer and famous work has been done by Warwick Tucker [T]. He proved that the Lorenz system for classical parameter values satisfies the geometric model by Guckenheimer and Holmes [GH]. Moreover, he gave the proof of the existence of the SRB measure supported on the attractor.
Recently, Hruska [Hr1,Hr2] proposed a method for computer assisted verification of uniform hyperbolicity. She successfully applied the method to the complex Hénon map. The method proposed by Hruska uses the notion of box-hyperbolicity. This method reduces the verification of the hyperbolicity of an invariant set to the verification if some quadratic forms are positive definite. The box-hyperbolicity requires some conditions for the derivative of a map under consideration and its inverse. This is not a limitation in the case of the Hénon map but makes the algorithm difficult to apply for ODE's. To compute the derivative of the inverse of a Poincaré map we can either invert an interval matrix that is an enclosure of the derivatives of the Poincaré map or integrate the ODE backwards together with the variational equations. In the first case the derivatives of Poincaré maps are often non-invertible as interval matrices because of unavoidable over-estimations when integrating the variational equations. Backward integration does not help in many cases. After changing the time t → −t in the equation the system often becomes stiff and again computationally difficult. In particular, this happens when the invariant set is an attractor with strong dissipation.
Later, Arai [A] proposed a method for verification that a chain recurrent set for a map is uniformly hyperbolic. He applied the method to the Hénon map [H] and verified that it is hyperbolic on the non-wandering set for a wide range of parameter values. This method, however, requires huge memory to work and it is computationally expensive by its very construction. Therefore, there is a little hope to apply it successfully in the high dimensional space and for nontrivial ODE's. Similar results were obtained by Mazur, Tabor and Kościelniak [MTK] and by Mazur and Tabor [MT]. The authors introduced a notion of semi-hyperbolicity and applied the method to the real Hénon map.
Our method is similar in the spirit to that proposed by Hruska. We use a notion of strong hyperbolicity proposed in [KWZ, Z] as a theoretical tool for verifying uniform hyperbolicity. The main difference of the method proposed here is that it does not involve conditions for the inverse of the map under consideration.
We believe that a successful application of our algorithms to a four dimensional Poincaré map is a serious test for the method as well as the implementation and it proves their applicability. We would like to mention here that verification of uniform hyperbolicity for explicit given maps is significantly easier than for the continuous systems. It is clear that in a numerical approach to hyperbolic dynamics one needs to enclose both values and derivatives of the map under consideration. This is an easy task when the map is given explicitly, while for Poincaré maps one needs to integrate the system with its variational equations.
For rigorous integration of the system and its partial derivatives we used C 0 and C 1 solvers from the CAPD library [CAPD] that the author is one of the main developers.
The paper is organized as follows. In Section 2 we give the notion of strong hyperbolicity and the theoretical background on how to verify uniform hyperbolicity using this tool. In Section 3 we present algorithms used to define stable and unstable cones over the attractor. In Section 4 we give an application of the proposed method to the Smale map. We also present proofs of Theorem 1 and Theorem 2.
Let f : R n → R n be a diffeomorphism and let M ⊂ R n be a compact invariant set for f . We denote by T M the restriction of the tangent bundle T R n to M .
Definition 1. f is uniformly hyperbolic on M if T M splits into a direct sum T M = E u ⊕ E s of two T f -invariant sub-bundles and there are constants c > 0 and 0 < λ < 1 such that We will recall and reformulate the definition of strong hyperbolicity introduced in [KWZ] and later extended in [Z].
are compact sets having pairwise disjoint interiors. In our algorithms these sets will be boxes in some coordinate systems. Let us fix nonegative integers u, s such that u + s = n. Assume that at each set M i we have fixed a linear coordinate system C i . We define a quadratic form For i = 1, . . . , N we define positive and negative cones by and call cubical set with cones.
By Inv(f, M ) we will denote the maximal invariant set for f in M , i.e.
The proof of the above theorem consists of several lemmas.
Proof. We will prove the first assertion. Since u ∈ Q + i we have Q(C i u) > 0. Fix j such that f (M i ) ∩ M j = ∅. Putū = C i u andz = C i z. Since C i and C j are linear and f is strongly hyperbolic on M we have Thus, by definition Df (z)u ∈ Q + j . We will now prove the second assertion.
Reasoning as in the proof of the first assertion we conclude that Hence, s = Df (z)s ∈ Q + j which contradicts the choice of s.
Then the assertion follows from the compactness of M .
Before we state the next lemmas let us define some constants. Put There is a constant R > 0 such that for u ∈ R n and i = 1, . . . , N we have u 2 ≥ R|Q(C i u)|.
Proof. We have Similarly Hence, the assertion follows with (8) for u = 0 and k > 1 we have From Lemma 6 we get that there is a constant R > 0 depending on M only, such that for u ∈ R n holds where D 2 (M) was defined in (7). Combining (10-12) we obtain that for u ∈ Q + i0 and k > 1 holds Clearly, adjusting the constant c we can obtain required inequality for k > 0.
There remains for us to show backward expansion in the negative cones.
Proof. From Lemma 5 there isλ ∈ (0, 1) such that the matrices (13) for k > 0 and s = 0 we obtain that after substituting s k and z k becomes From (13-14) we have Combining (15-17) we obtain that for k > 1 and s ∈ Q − i0 holds Adjusting the constant c if necessary we can obtain the same inequality for k > 0.
Proof of Theorem 3. Let us associate to each z ∈ Inv(f, M ) an index i z such that z ∈ M iz . This index might be not unique but for each z we can fix one of them. For simplicity we will write M z , C z , Q ± z instead of M iz , C iz , Q ± iz . From Lemma 4, Lemma 7 and Lemma 8 there are constants c > 0 and λ > 1 such that for z ∈ Inv(f, M ) we have z . Note, the cones Q + z and Q − z are disjoint and the sum of them spans R n . Hence, the assertion follows from [KH, Corollary 6.4.8].

Algorithms.
3.1. Graph representations of maps. Let X be a topological space and let N ⊂ X. For a family of subsets U ∈ 2 X by supp (U) we will denote its geometrical representation supp (U) = U ∈U U .
Definition 3. We will say that U ∈ 2 X is a cover of N if U is a finite set and N ⊂ supp (U).
Definition 4. Let U, V be a finite sets. A multivalued function f : U V is called a combinatorial map.
Covers of compact sets as well as combinatorial maps appear naturally in the computer assisted proofs in dynamical systems. We usually cannot compute the range of a map f : X → Y over a domain U ⊂ X. Instead, one can fix covers X , Y of X and Y , respectively, and then compute combinatorial representation of the map in the covers X , Y. This is usually realized in the following steps.
• For U ⊂ X compute a minimal cover This step is often realized by means of the interval arithmetic [M]. In most cases it is very difficult to compute V i as a minimal cover of f (V i ). • Define a cover of f (U ) by V i .
The above considerations lead to a very natural definition of the combinatorial representation of a map.
Definition 5. Let f : X → Y be a map and let us fix covers X , Y of X and Y , respectively.
We will say that a combinatorial map F : X Y is a combinatorial representation of f if for x ∈ X and for all U ∈ X such that x ∈ U holds f (x) ∈ supp (F(U )).
For a map f : X → X and a cover X of X it is natural to encode a combinatorial representation of f as a directed graph. A finite directed graph is a pair G = (V, E), where V is a finite set whose elements are called vertexes, and E ⊂ V × V is a set of selected (ordered) pairs of vertexes. The elements of E are called edges.
We will need a notion of the transposed graph and outgoing edges. For a graph 3.2. Enclosure of an attractor. In this section we will describe an algorithm that we used to enclose an attractor. There are already existing packages for rigorous enclosures of invariant objects, see for example [GAIO]. We used, however, our own implementation dedicated for this purpose which seems to be easier and makes the software independent on the other libraries. We will use the fact that what we want to enclose is an attractor. The idea is very simple. First, we fix a cover X of the observed attracting domain. Then we choose a box V from observed attracting region, and we enclose its forward trajectory using the sets from the cover X as long as the trajectory does not leave supp (X ). Since the cover X is finite by its definition, after a finite number of steps there are no new sets in the cover of the trajectory of V and we can stop the procedure. This approach generates an enclosure of some invariant set, that is expected to be an attractor.
The Algorithm 1 summarizes the above considerations.
Lemma 9. Fix a cover X of X. Assume Algorithm 1 is called with its arguments V , G = (V, E) and f . If the algorithms stops without the Failure result then Proof. First observe that the algorithm always stops. By contradiction, assume it does not stop. This means that in each iteration of the main repeat-until loop (lines 4-15) the set U is not empty. This implies, that the number of elements in the set V, which is updated in line 14, is strictly increasing. But this is a contradiction with V ⊂ X , which is a finite set by the definition of cover.
Let G be the result returned by the algorithm and let F : V V be the combinatorial map represented by the graph G.
We are proving the assertion (i). Let x ∈ supp (V) and let V ∈ V be such that x ∈ V . Observe, that if F(V ) is not empty then f (V ) ⊂ supp (F(V )) -as guaranteed in lines 9, 11, 12 and 14 of the algorithm. Hence, in this case the assertion follows. To finish this step we observe, that the main repeat-until loop stops when the set U is empty. But this set contains of exactly these sets U ∈ V (lines 10 and 13) for which the value F(U ) is not computed yet. Hence, after the algorithm stops, for each V ∈ V, supp (out(V, G)) contains a computed enclosure of f (V ).
Assertions (ii) follows from (i) and the definition of combinatorial representation.
To prove (iii) it is enough to observe that V ⊂ supp (V) as guaranteed in line 3, 10 and 14 of the algorithm. Then the assertion follows from (ii).
Using Algorithm 1 one can compute combinatorial representation of a map restricted to some positive invariant set, which is expected to be an attractor. For further applications this graph should be as small as possible and it should still contain enclosure of the invariant set of f restricted to supp (V). Therefore it is important to choose the starting box V such that it contains points from the attractor. An easy way to do that is to take a point from the observed basin of attraction and compute non-rigorously its forward trajectory for some long time. Then we can choose a set V from the cover that contains the last computed point.

3.3.
Computing of coordinate systems. In this section we assume that the graph G = (V, E) is a combinatorial representation of f resulting from Algorithm 1. We present a heuristic method for computing of coordinate systems C V at the vertex V , for V ∈ V. We assume that at the beginning the coordinate systems are not set, which we will denote by C V =NULL.
The method consists of the following steps.
Step 1. Finding cycles in the graph. First we try to find (non-rigorously) as much as possible of periodic points of f in supp (V). This is important, because given a period p point, say x, a very natural choice of a coordinate system in a vertex containing this point is the Jordan basis of Df p (x). Of course it may happen that several periodic points belong to the same vertex. In this case we are choosing one from these points of the lowest principal period. More formally; let us fix a positive integer N . This is an upper bound for the highest period of orbits we will search for. Since G is a combinatorial representation of f , all periodic points of f must belong to some cycles in the graph G. Let P i , i = 1, . . . N be a set of vertexes V such that there exists an i-periodic cycle in the graph G through V and no lower period cycle containing V exists. The sets P i can be computed by means of standard graph algorithms and we omit details here.
Step 2. Refining cycles to periodic points. In this step we compute the sets of points P i , i = 1, . . . , N that are good approximations of periodic points. For V ∈ P i we proceed as follows. Let x be an approximate center of V . The point x is a seed point for the standard Newton method for zero finding problem applied to the map g(x) = f i (x) − x. If the Newton method converges to a point y ∈ supp (V) which is of principal period i then we insert the point y to the set P i .
We would like to comment here, that we do not try to find all periodic orbits of low periods for the map f . Using our approach one can detect most of them if the set V consists of small enough sets. Clearly, a larger number of detected periodic points is better for setting the coordinate systems but the task of finding all low period orbits is not a goal for us.
Step 3. Setting coordinate systems in a neighborhood of periodic points. The goal of this step is to assign a coordinate system to vertexes that contain computed approximate periodic point. For y ∈ P i we proceed as follows. Let V ∈ V be a vertex such that y ∈ V . Such a vertex exists since we know that y ∈ supp (V) -as guaranteed by the previous step.
• If the vertex V has already assigned a coordinate system then we proceed with the next point from P i . • We compute an approximate derivative Df i (y) and an approximate matrix M y of normalized eigenvectors. The columns of M y are sorted by decreasing absolute value of the associated eigenvalue. • We assign to the vertex V a coordinate system V C = M y .
We would like to comment here that the sets P i are proceeded by increasing index i. This guarantees that a vertex V will have assigned coordinate system from some periodic point of the lowest principal period. Note, the resulting coordinates depend on the order chosen in the set P i .
Step 4. Spreading coordinates from periodic points. The main idea is to propagate the coordinate systems from periodic points by the action of the derivative. It is well known that the direct propagation of coordinates by Df in floating point arithmetic usually results in collapsing of these coordinates to a singular matrix. Therefore we will involve some orthonormalization process.
The Algorithm 2 describes the procedure. Proof. We will prove that the algorithm always stops. Assume it is not the case. Then in each iteration of the main loop the set P is non-empty. But this set contains (lines 3 and 19-22) exactly these vertexes for which the coordinate system is assigned in the current iteration of the loop. Hence, the set of vertexes at which we have assigned the coordinate system will increase in each iteration. This contradicts the fact, that V is a finite set. We will prove that the algorithm sets coordinates in each vertex. Assume it is not the case. Take G T = (V , E ). Let V be a vertex such that C V =NULL. Then for U ∈ out(V, V ) holds C U = N U LL. Otherwise, U will belong to the set S in some iteration and then the coordinates will be set in V . Denote V 1 = out(V, G T ).
In a recurrent way we can define The same reasoning proves that C U =NULL for U ∈ V k . Since G consists of only one strongly connected component, G T does too. Hence, for some K > 0 we have V K = V which contradicts the assumption that C U =NULL for U ∈ S and S = ∅.
The input argument S is the set of vertexes that contain periodic points and for which the coordinate systems were already computed in Step 3. As we have seen, lines 5-18 are not important for the correctness of the Algorithm 2. In these lines a heuristic method for computing of coordinate systems is proposed. We propagate the actual coordinate system C V by the derivative along a short part (k iterations) of the trajectory of the center of V . Then we perform orthonormalization of columns and propagate the obtained matrix backwards k − 1 times. This heuristic can work because for the inverse map the stable directions are attracting for T f and after few steps we get some approximation of stable directions at f (centre(V )).
In this step we also assumed that the graph G consists of only one strongly connected component. It is not a restriction, since the method is dedicated for attractors. In practice, Algorithm 1 always returns such a graph if the initial set V is chosen carefully. Formally, it is easy to verify that a graph consists of one strongly connected component using for example Tarjan's algorithm [Ta].
Remark 11. The result of the algorithms described in steps 2,3,4 depend on the order chosen to index the sets of vertexes and points (P i , P i and S). Moreover, these algorithms are not deterministic, when implemented in parallel mode. The coordinate system at each vertex is computed by the first thread that reaches this vertex.
Anyway, the conclusion of Lemma 10 holds; we have computed some coordinate system at each vertex and we can start verification of the cone conditions.
3.4. Verification of the cone conditions. This step is quite straightforward. Let G = (V, E) be a graph which encodes a combinatorial representation of a map f . Assume we have computed some coordinate systems {C V } V ∈V . The goal is to check whether the assumptions of Theorem 3 hold true for f . This can be done by simply verifying the positive definiteness of some interval matrices corresponding to every edge in E. We have the following obvious lemma.
Lemma 12. Assume the Algorithm 3 is called with its arguments G = (V, E), Q and f . Assume that all the matrices {C V } V ∈V are invertible. The algorithm always stops and returns a set U such that for V ∈ V \ U and W ∈ out(V, G) the interval matrix A direct consequence of the above Lemma and Theorem 3 is the following Corollary 13. The same assumption as in Lemma 12. Assume G encodes a combinatorial representation of the map f and let Q be quadratic form as in (4). If the Algorithm 3 called with its arguments G = (V, E), Q and f returns an empty set U then f is uniformly hyperbolic on Inv(f, supp (V)).

Applications.
In this section we will show how the method introduced in the last section works in a very easy example. Then we will give a proof of Theorem 1.

Toy example -Smale map.
A natural choice to test the algorithms and implementation is a very simple example. Here we have chosen the well known Smale map s : s(x, y, t) = (0.1x + 0.5 cos(2πt), 0.1y + 0.5 sin(2πt), 2t mod 1).
The map is proved to be uniformly hyperbolic just by simple hand-made calculations. It is easy to see that the set [−1, 1] × [−1, 1] × [0, 1] is positive invariant for s. Define a cover of this attracting domain of the form We will call the number k in X k the resolution. After application of Algorithm 1 we got an enclosure of the attractor consisting of 567 boxes for k = 4 and 3333 boxes for k = 6. These enclosures are shown in Fig. 2.  Figure 2. Enclosure of the Smale attractor for the resolutions k = 4 and k = 6. Note, the planes t = 0 and t = 1 should be identified.
We completed the proof of uniform hyperbolicity for the resolution k = 4. We run the algorithm for finding cycles in the graph and refining them to periodic points with the maximum period set to N = 3. They returned 1 candidate for fixed point, a period 2 orbit and two period 3 orbits.
Then we applied the algorithm for spreading coordinate systems with k = 2 (this is the number of forward iterates when propagate the coordinate systems) and verification of the cone conditions. We run Algorithm 3 with the quadratic form and it returned an empty set U of unverified vertexes. The program executes within less than 1 second on a laptop-type computer.
4.2. Application to the system of coupled van der Pol oscillators -proof of Theorem 1. Consider the system (1) with the parameter values (3). Let P be the Poincaré map as defined in (2). Let us perform a linear change of coordinates  As it is observed in [KSe], in these coordinates the attractor is more aligned to the coordinate axes. In the sequel we will consider the Poincaré mapP = L −1 P L, where L is the matrix of coordinate change. After few attempts we found that the resolution k = 14 is enough for verification of the hyperbolicity of the observed attractor forP . This means that we have used a uniform grid in some bounded domain of the form In Table 1 we give the results of applying of the algorithms for generating enclosure, setting of coordinate systems and verification of strong hyperbolicity. We run Algorithm 3 with the quadratic form and it returned an empty set of unverified vertexes. Hence, the uniform hyperbolicity of the set Inv (P , supp (V)) is verified. To complete the proof of Theorem 1 we used the CHOMP library [CHOMP] in order to compute homology groups of the cubical set represented by V. The program verified that H 0 (V) = Z, hence the set supp (V) is connected. The group H 1 (V) also was nonzero, hence the set is non-contractible. This finishes the proof of Theorem 1.

4.3.
The existence of a fixed point and a period two orbit -proof of Theorem 2. As a byproduct of the proof of Theorem 1 we got a good numerical approximations of over one hundred periodic points. To prove that the set Inv (P , supp (V)) is nontrivial we used the interval Newton operator [M] as a tool for verification of the existence and local uniqueness of zeros of maps. We have the following lemma.
Lemma 14. Assume f is a smooth map in a neighborhood of an interval set X ⊂ R n and fixx ∈ intX. If the interval Newton operator then the map f has unique zero in the set X. Moreover, if x * ∈ X is the unique zero of f in X then x * ∈ N (x, X, f ).
Proof of Theorem 2. A good numerical approximation of a fixed point forP is -this is a point returned from the step of finding periodic points in supp (V). Let X be a ball of radius 10 −10 in the maximum norm centered atx. We computed the interval Newton operator N (x, X,P − Id) and we got that Hence, N (x, X,P − Id) ⊂ int(X) and the mapP − Id has a unique zero in X. Clearly this is a fixed point forP . We also verified that N (x, X,P − Id) ⊂ supp (V) and this finishes the proof thatP has a fixed point supp (V).
In a similar way we verified that the attractor contains a period two orbit. It is enough to show that the map F (x, y) = (P (x) − y, P (y) − x) has a zero for some (x * , y * ) and x * = y * . We have a good candidate for periodic points Let Z ⊂ R 8 be a ball of radius 10 −10 in the maximum norm centered atz = (x,ȳ). We verified that This proves that F has a unique zero (x * , y * ) ∈ Z. Since x −ȳ 0 ≥ 2 · 10 −10 we have x * = y * and both x * , y * are period two points forP . We also verified that (x * , y * ) ∈ N (z, Z, F ) ⊂ supp (V) × supp (V) and this completes the proof of Theorem 2.

Conclusions.
In this paper we proposed a method for rigorous verification of uniform hyperbolicity for maps. The method has been successfully applied to a Poincaré map of a non-autonomous ODE in four dimensions. We believe the method can be applied to other systems.
Kuznetsov [K2] did a numerical study of this system and observed that for a wide range of parameter values around K = 1.9 and ε = 0.72 the Poincaré map has a hyperbolic attractor. A rigorous enclosure of the attractor for K = 1.9, ε = 0.72 resulting from Algorithm 1 with the resolution k = 9 is shown in Fig. 4. The resolution k = 9 was not enough to perform the step of verification of uniform hyperbolicity of this map. We also enclosed this attractor with resolution k = 12 but again this was not enough to verify the hyperbolicity. Further subdivision was not possible due to memory limitations in the computer that we used. Computations for the system (19) are much harder than for (1). First -the vector field is a quite large expression and even if the system is lower dimensional, it is more complicated for rigorous integration. Second, and most important; as easily seen in Fig. 4, the attractor is very thick and harder to cover than the almost one dimensional Smale solenoid. An approximate Hausdorff dimension reported in [K2] is ca 1.7. We reached the limit of available memory on our computer when enclosing the attractor with a thinner cover. We believe, however, that some further optimizations in data structures will help to prove hyperbolicity of this system. A straightforward idea is to use non-uniform covers.  (19) with parameter values K = 1.9, ε = 0.72 and with the resolution k = 9.
5.1. General invariant sets. In this paper we verified hyperbolicity of attractors. But the method can be easily extended to invariant sets. The only part which requires some modification is the method for generating an enclosure of an invariant set. If the invariant set is an attractor, the strategy of "inner" enclosure is better -Algorithm 1. For a general invariant set an "outer" approximation is necessary. We also implemented "outer" approximation for enclosing of general invariant sets but we do not report details here, since it is rather standard procedure. As a test case we proved that the well known Hénon map [H] H a,b (x, y) = (1 + y − ax 2 , bx) is uniformly hyperbolic on the invariant set for the parameter values a = 5.4 and b = −1.
As mentioned above, we used an "outer" strategy to enclose the invariant set -the result is shown in Fig. 5 and it consists of 8832 boxes. Then we applied algorithms for finding cycles and periodic points, computing of coordinate systems and verification of the cone condition with the quadratic form Q = 1 0 0 −1 .
The program executes within less than 1 second on a laptop-type computer with the Intel Core 2 Duo 2GHz processor. A computer assisted proof for the same parameter values is presented in [A, MT]. In [MT] the authors report the time of computations less than 10 seconds on a comparable CPU. 5.2. Implementation. The C++ program for verifying the hyperbolicity has been implemented by the author and the source code is available at [W]. The code is highly parallelized using the Open MP library supported by the compilers gcc-4.2 or newer. The code is written in a very generic way; it heavily uses template techniques. In fact, an input to the algorithms is an abstract map (template parameter) for which we assume that we know how to compute values and derivatives. In the case of Poincaré maps we used for this purpose the C 0 and C 1 solvers from the [CAPD] library -see also [Z1] for an efficient algorithm for integration of first order variational equations. All computations regarding Theorem 1 and Theorem 2 were performed on a cluster with 7 computers, each having 8 Quad-Core AMD Opteron(tm) 8354, 2.2GHz processors with 64GB of RAM. During the computations the maximal usage of the memory was 32%.