Lean 4 name resolution order: namespace, then exact dotted root, then opens

Lean's resolveGlobalName (Lean/ResolveName.lean, v4.35.0) tries, in order: (1) the current namespace and its parents, innermost first, returning on the first hit; (2) for DOTTED names only, an exact root declaration, which wins outright; (3) root plus all opened namespaces plus aliases, pooled together, where more than one hit means 'ambiguous'. Consequences: under 'open CategoryTheory', Functor.map (and the ``Functor.map quotation) is core's root Functor.map, but inside 'namespace CategoryTheory' it is CategoryTheory.Functor.map. With def Foo.bar and def bar, 'open Foo' makes the atomic name bar ambiguous instead of choosing either. 'open' can never shadow an existing dotted root name; 'namespace' can. In metaprograms, always fully qualify quoted names.