Uniqueness in the Riemann mapping theorem

This file proves the uniqueness companion to the Riemann mapping theorem. Two biholomorphic maps from the same open subset of ℂ onto the unit disc differ by a standard disc automorphism. If both maps send the same base point to zero, that automorphism is a rotation.

The proof uses the classical transition-map argument: the inverse of one map is holomorphic on its image, so composing it with the other map gives a holomorphic automorphism of the disc. The classification in TauCeti.Analysis.Complex.Conformal.UnitDisc.Automorphism.Classification then supplies the standard Moebius formula. The inverse is represented by Mathlib's Function.invFunOn; its holomorphy follows from Mathlib's analytic inverse-function theorem and Tau Ceti's local injectivity criterion.

This advances TauCetiRoadmap/ConformalMapping/README.md, layer L3, specifically “Uniqueness up to Aut(𝔻)”. The argument follows Ahlfors, Complex Analysis, Chapter 6. As with all L0--L3 material in this roadmap, it is coordinated with the upstream Riemann-mapping work in leanprover-community/mathlib4#33505 and should be replaced by public human-curated Mathlib API when that becomes available.

theorem TauCeti.exists_eqOn_unitDiscStandardAutomorphismFormula_comp {U : Set ℂ} (hU : IsOpen U) {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) (hfi : Set.InjOn f U) (hgi : Set.InjOn g U) (hfimage : f '' U = Metric.ball 0 1) (hgimage : g '' U = Metric.ball 0 1) : ∃ (u : Circle) (a : Complex.UnitDisc), Set.EqOn g (fun (z : ℂ) => ↑u * ((f z - ↑a) / (1 - (starRingEnd ℂ) ↑a * f z))) U

Uniqueness in the Riemann mapping theorem, up to a disc automorphism. If f and g are holomorphic injections from an open set U onto the open unit disc, then there are u on the unit circle and a in the unit disc such that

g z = u * (f z - a) / (1 - conj a * f z)

for every z ∈ U.

theorem TauCeti.exists_eqOn_const_mul_of_image_eq_ball_of_apply_eq_zero {U : Set ℂ} (hU : IsOpen U) {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) (hfi : Set.InjOn f U) (hgi : Set.InjOn g U) (hfimage : f '' U = Metric.ball 0 1) (hgimage : g '' U = Metric.ball 0 1) {z₀ : ℂ} (hz₀ : z₀ ∈ U) (hfzero : f z₀ = 0) (hgzero : g z₀ = 0) : ∃ (u : Circle), Set.EqOn g (fun (z : ℂ) => ↑u * f z) U

Normalized uniqueness in the Riemann mapping theorem. If two biholomorphic maps onto the unit disc send the same point of their domain to zero, then they differ by a rotation of the disc.