circle_map_check_paths now follows from a lemma

and it takes 6.6 seconds to check that (!).
The lemma includes an "admit", to work on next.