OAI/Analysis/CircleDomains/Rigidity/UniformizedMaskedTransfer.lean

Circle models for the actual masked finite transfer

The metric and filled coordinates come from the common good-width construction. The completed surface is the actual complement of the terminal disks. Compact metric uniformization and finite circle uniformization then produce a bijective circle model, conformal on the retained core and metric-conformal throughout the completed interior.