SingletonPathDetour.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A path whose contacts with a closed level all belong to singleton components can be deformed off that level, inside its prescribed open mask. The small neighborhoods come from the actual component quotient.

theorem OAI.CircleDomainRigidity.exists_path_avoiding_singleton_level line 15