`suppFun` is continuous (Remark 4.6 of Wedhorn). 

**Huber embedding — Phase 1 main result.** The map `ιSpv : Spv A → (A × A → Prop)`
is a topological embedding (injective + induced topology agrees).

This is the content of the topological half of Wedhorn's Theorem 4.9 / Huber 1993, Lemma
2.1. The compactness conclusion additionally requires closedness of the image, which is
deferred to Phase 2. 

**Alexander sub-basis theorem, applied to `Spv A`.** If every cover of `Spv A`
by sub-basic opens (basic opens `basicOpen f s`) admits a finite subcover, then
`Spv A` is compact.

This is the direct content of Wedhorn Theorem 4.9 / Huber, *Continuous valuations*
(1993), reformulated purely as a statement about covers of the underlying type by
basic opens. 

**Continuity transfer from open subring.** If `v` is a valuation on `A`,
`A₀` is an open subring, and `v|_{A₀}` (the restriction) is continuous
(in the subspace topology on `A₀`), then `v` is continuous on `A`.

This is Wedhorn's Lemma 7.44(2). The proof uses: for any `γ`, the set
`{a ∈ A | v(a) < γ}` is an additive subgroup containing the open set
`A₀.subtype '' {a ∈ A₀ | v(a) < γ}`, hence is open. 

**Continuous valuations are determined by a dense subring** (the injectivity content of
Wedhorn Proposition 7.48 = Huber [Hu2] Prop. 3.9). If `φ : R →+* S` has dense image and two
continuous valuations `v`, `w` on `S` induce the same preorder on `φ(R)`, then `v` and `w`
are equivalent. 

**The point of `Spv S` is determined by a dense subring** (the injectivity content of
Wedhorn Proposition 7.48 = Huber [Hu2] Prop. 3.9). If `φ : R →+* S` has dense image and two
continuous points `v, w ∈ Spv S` have the same pullback `comap φ v = comap φ w`, then `v = w`.
This is the elementary uniqueness half of the Spa–completion comparison; it is the keystone
the completion Spa-injectivity (`comap_coeRingHom_injOn_spa`) reduces to.