WeightedPhysicalCollars.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-cost smooth physical collars of an actual collapsed component. The regular level containing the chosen boundary is retained explicitly.

theorem OAI.CircleDomainRigidity.exists_weighted_small_physical_disk line 16