OAI/Probability/SLE/Geometry/PublishedConformalCompactness.lean

The classical published normal-family input, restricted to the interior normalization used in the ribbon proof.

P. L. Duren, Univalent Functions, Springer, 1983, §1.3, unnumbered theorem on p. 9: compactness of the normalized schlicht class. The half-plane specialization below follows by disk automorphisms and affine normalization, using the growth/distortion bounds in §2.3. The moving normalization points stay on one compact semicircle, their images are bounded, and the derivative norms stay bounded above and away from zero. The nonvanishing derivative of the univalent limit is the local mapping property in §1.2, p. 5.

This is an explicit hypothesis, not an axiom. It contains no boundary guide, SLE passage, sausage estimate, or uniformity over stopped pasts.