Commit 2026-04-23 19:18 785d93ce

feat(Analysis/SpecialFunctions/Complex/Circle): Anticlockwise Path on Circle (#37815) This PR introduces explicit path constructions on the unit circle (Circle) and proves fundamental topological properties regarding its connectedness. Main Definitions:

• Circle.angleDiff: The directed angle length from x to y along the anti-clockwise arc, using the principal arg.
• Circle.path: An explicit Path x y on the circle traversing in the anti-clockwise direction, constructed using Circle.exp. Main Instances and Theorems:
• instPathConnectedSpaceCircle
• Circle.range_path_union_range_path & Circle.range_path_inter_range_path: The anti-clockwise path from x to y and the path from y to x are internally disjoint and covers the entire circle.
• Circle.singleton_compl_isPathConnected: The circle minus a single point remains path-connected.
• Circle.not_isPreconnected_pair_compl: The circle minus two distinct points is disconnected (not preconnected).