OAI/Analysis/CircleDomains/Development.lean

Koebe uniformization and removable-boundary rigidity

Both assigned main statements are proved without published-input hypotheses: koebeCircleDomainConjecture and circleDomainRemovabilityRigidity. Result047 gives explicit theorem statements for the two papers. The original koebeCircleDomainConjecture_of_published_inputs and circleDomainRemovabilityRigidity_of_published_inputs are preserved.

Finite analytic and Jordan models are constructed using invariant Beltrami coefficients, actual reflected conjugates, and exact round boundary images. The downstream proof constructs its retained tests and null axial traces, finite-hole and principal outer flux, and removable-dust extensions.