ProtrusionAlternatives.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

At a marked-component protrusion, either a small compatible real barrier exists, or positive-law duality constructs a compatible mean coordinate with an open sized exclusion.

theorem OAI.CircleDomainRigidity.exists_protrusion_barrier_or_selectable_mean line 20