This chapter proves Aubry-Mather type for the double resonance regime. It begins by considering the “non-critical energy case” and showing that the cohomologies as chosen are of Aubry-Mather type. The proof consists of two cases. In the first case, the chapter uses the almost verticality of the cylinder, and the idea is similar to the proof of Theorem 9.3. It applies the a priori Lipschitz estimates for the Aubry sets. In the second case, the chapter uses the strong Lipschitz estimate for the energy, and the idea is similar to the proof of Theorem 11.1. It then looks at the construction of the local coordinates. This is done separately near the hyperbolic fixed point (local) and away from it (global).