PuncturedPhysicalCollar.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Punctured disk collars for a continuous physical coordinate, including coordinates pulled back through the component quotient. Boundary avoidance suffices: compactness supplies one common inward width.

theorem OAI.CircleDomainRigidity.exists_punctured_physical_collar line 15