CountableUnavailableLevelEndpoints.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Countability of endpoints with no small compatible barrier. The transfinite positive-law recursion retains all earlier laws and their dust marks, and alternating disk crossings give the contradiction.

theorem OAI.CircleDomainRigidity.countable_unavailable_endpoints_for_levels line 23