A computer-assisted proof of chaos in Josephson junctions

This paper presents a rigorous verification of chaos in the RCLSJ model for studying dynamics of the Josephson junction. By carefully picking a suitable cross-section with respect to the attractor, it is shown that for the corresponding Poincaré map P obtained in terms of second return time, there exists a closed invariant set Λ in this cross-section such that P Λ is semi-conjugate to a 2-shift map, thus showing existence of chaos in the RCLSJ model.