# Koebe’s circle-domain conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Removable Boundaries and Rigidity of Circle Domains](../../preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/paper.pdf)
- [Koebe's Circle-Domain Conjecture](../../preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf)

## Scope

The formalization proves the removability-to-rigidity direction of the He–Schramm conjecture. If a circle domain has conformally removable boundary, then every conformal equivalence from it to another circle domain agrees on the source with a Möbius transformation. There is no bound on the number of complementary components.

The same Comparator file also states Koebe's circle-domain theorem, which gives a circle-domain representative for every domain in the Riemann sphere.

Koebe's circle-domain conjecture asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, whose complementary components are round disks or points. The formalization proves this for every domain. It also proves rigidity under a separate hypothesis: a conformal equivalence between circle domains is a Möbius transformation when the source boundary is conformally removable.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Removable-boundary rigidity and the circle-domain theorem | [KoebeCircleDomains.lean](../ComparatorChallenges/KoebeCircleDomains.lean) |
| Koebe's circle-domain theorem and removable-boundary rigidity | [KoebeCircleDomains.lean](../ComparatorChallenges/KoebeCircleDomains.lean) |