OAI/Analysis/CircleDomains/Transfer/GridStageContours.lean

The contour selection at one descending grid stage

Preliminary disjoint dust disks localize the compact target on the current grid. Singleton components of the lower-grid obstacle then give actual smooth contours inside each preliminary disk. The output avoids the lower obstacle on its boundary and stays in the prescribed safe open set.

This is the construction in Section 2, Step 3 of the Koebe manuscript; the only external inputs are the scalar Sard and classical contour inputs already used by FiniteDustCover.