A proper domain with holomorphic square roots injects holomorphically into the unit disc

The first step of the Riemann mapping theorem: the competing family is nonempty. Every open, proper subset of ℂ with holomorphic square roots (TauCeti.HasHolomorphicSquareRoots) — in particular every simply connected one — admits an injective holomorphic map into the open unit disc.

This is the classical square-root construction. Pick a ∉ U. On U the nonvanishing function z - a has a holomorphic square root h; when U is simply connected this is TauCeti.exists_differentiableOn_pow_eq at n = 2, constructed as exp (L / 2) from the upgraded holomorphic logarithm branch L, not from Mathlib's continuous root branch. Then:

• h is injective, since h z₁ = h z₂ forces z₁ - a = z₂ - a after squaring;
• h '' U is open (open mapping theorem: h is injective, hence nonconstant near each point of the open U), so it contains a ball ball w₀ r;
• -h z avoids that ball for every z ∈ U: otherwise -h z = h z', and squaring gives z' = z, hence h z = -h z and so h z = 0, which is impossible;
• therefore r ≤ ‖h z + w₀‖ throughout U.

Inverting, z ↦ (r/2) / (h z + w₀) is holomorphic, injective, and bounded by 1/2. Halving r is what makes the bound strict, landing in the open disc rather than its closure.

Attribution and upstream coordination

Two pieces of prior Mathlib work stand behind this file, both © Yury Kudryashov.

The construction. This follows the in-tree Mathlib proof of the same step, Complex.exists_mapsTo_unitBall_injOn_deriv_ne_zero (Mathlib.Analysis.Complex.RiemannMapping): the same plan — pick a ∉ U, take a holomorphic square root of z - a, obtain an open image ball, observe that -h avoids it, and invert. That lemma is present in this checkout but is not exported from its module (it carries no public marker under the module system, so an importer cannot name it — a direct reference elaborates to Unknown constant, while a public lemma from the same file resolves), which is why this file re-derives the construction rather than reusing it.

The square root it rests on. The branch used here comes from TauCeti.exists_differentiableOn_pow_eq, which derives the root as exp (L / n) from the holomorphic upgrade of Mathlib's continuous logarithm branch Complex.exists_continuousOn_eqOn_exp_comp (Mathlib.Analysis.Complex.BranchLogRoot); Mathlib's continuous root API Complex.exists_continuousOn_pow_eq is not used. The existence half of this step is therefore Mathlib's; the sibling file BranchLogRoot.lean records that debt in detail.

The Riemann mapping theorem is also being formalized upstream at mathlib4#33505, which proves the L0–L3 prerequisites internally as private lemmas. This declaration is an explicitly temporary shim: delete it and refactor downstream consumers onto the exported Mathlib version once it lands.

Main statements

• TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall — the nonempty-family step.
• TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall_apply_eq_zero — the same step for the normalized family, whose members fix a chosen base point. This is the form the roadmap's maximization argument consumes.

theorem TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall {U : Set ℂ} (hUs : HasHolomorphicSquareRoots U) (hUo : IsOpen U) (hUne : U ≠ Set.univ) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.InjOn f U ∧ Set.MapsTo f U (Metric.ball 0 1)

A proper open set with holomorphic square roots injects into the unit disc. The Riemann mapping theorem's competing family — injective holomorphic maps U → 𝔻 — is nonempty. A simply connected open set has holomorphic square roots (IsSimplyConnected.hasHolomorphicSquareRoots).

theorem TauCeti.exists_differentiableOn_injOn_mapsTo_unitBall_apply_eq_zero {U : Set ℂ} (hUs : HasHolomorphicSquareRoots U) (hUo : IsOpen U) (hUne : U ≠ Set.univ) {z₀ : ℂ} (hz₀ : z₀ ∈ U) : ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.InjOn f U ∧ Set.MapsTo f U (Metric.ball 0 1) ∧ f z₀ = 0

The normalized competing family is nonempty. The roadmap's maximization step ranges over injective holomorphic maps U → 𝔻 that fix a chosen base point z₀, so the nonemptiness it needs is this one, not the bare version above.

The normalization is the textbook one: post-compose with the disc automorphism centred at c = f z₀, w ↦ (w - c) / (1 - conj c * w). That is the L2 disc-automorphism API of this roadmap, already available here as TauCeti.unitDiscMoebius and its scalar formula, so this step consumes it rather than substituting a weaker correction:

• holomorphy — TauCeti.differentiableOn_unitDiscMoebiusFormula_of_norm_lt_one;
• self-map of 𝔻 — TauCeti.mapsTo_ball_unitDiscMoebiusFormula_of_norm_lt_one;
• injectivity on 𝔻 — the factor centred at -c is a left inverse (TauCeti.leftInvOn_unitDiscMoebiusFormula_of_norm_lt_one).

Each is stated for a scalar centre of norm < 1, which is exactly what f z₀ ∈ 𝔻 supplies, so no passage through the bundled Complex.UnitDisc is needed. The Moebius factor is onto 𝔻, which the uniqueness half of the Riemann mapping theorem will need; the nonempty normalized family obligation proved here uses only the three properties above.