OAI/Analysis/CircleDomains/Uniformization/MetricUniformization.lean

Conditional uniformization of a finite metric completion

CompactMetricSphereUniformization is the smooth metric-sphere specialization of compact genus-zero uniformization: Ahlfors, Conformal Invariants (1973), Theorem 10-3, p. 142, together with the smooth isothermal-coordinate construction in Jost, Compact Riemann Surfaces, third edition (2006), Theorem 3.11.1, pp. 155--158. The metric formulation is also stated at the start of Hedenmalm--Shimorin, Hele--Shaw flow on hyperbolic surfaces, J. Math. Pures Appl. 81 (2002), pp. 187--188, equation (1.1). Its output records metric conformality of the actual real differential in sphere charts, including positive orientation. The metric agrees with the spherical metric near infinity, so it defines a smooth metric on the sphere.

Together with Conway's finite circle theorem, this gives a circle model for the actual terminal-disk completion that retains holomorphy on the prescribed core. Both published inputs remain explicit parameters.