SubordinateDustCover.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Preliminary smooth dust covers subordinate to prescribed local branch neighborhoods. This retains which neighborhood contains each closed physical fill, for the mixed period-coordinate construction.

theorem OAI.CircleDomainRigidity.exists_subordinate_smooth_physical_dust_cover line 14