OAI/Analysis/CircleDomains/Sobolev/ExteriorOmittedAreaInput.lean

Quantified numerical exterior-area bound: Ahlfors, Conformal Invariants (1973), Exterior Area Theorem, Theorem 5-1, p.83. Only the omitted-area inequality for an injective holomorphic exterior map with principal normalization is retained. This is an explicit published-input parameter, not an axiom.