MacNeille completion and profinite completion can coincide on finitely generated modal algebras

Following Bezhanishvili and Vosmaer, we confirm a conjecture of Yde Venema by piecing together results from various authors. Specifically, we show that if \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{A}}$$\end{document} is a residually finite, finitely generated modal algebra such that HSP(\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{A}}$$\end{document}) has equationally definable principal congruences, then the profinite completion of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{A}}$$\end{document} is isomorphic to its MacNeille completion, and ◊ is smooth. Specific examples of such modal algebras are the free K4-algebra and the free PDL-algebra.