Choice-free regular open completion of forcing preorders

Declare a set open when it is downward closed. The empty set and $P$ qualify, and arbitrary unions and finite intersections of downward-closed sets remain downward closed, giving a topology. Every open neighborhood of $p$ contains $\downarrow p$, and this downset is itself open. Consequently $p\in \bar{A}$ iff $\downarrow p\cap A\mathrm{\ne }\mathrm{\varnothing }$, and $p\in \mathrm{int}A$ iff $\downarrow p\subseteq A$. In particular $\overline{\downarrow q}$ consists of the conditions compatible with $q$, and $p\in e(q)⟺(\mathrm{\forall }r\le p)r\text{ is compatible with }q⟺p{\le }^{\ast }q$. F2 ensures $e(q)$ is regular open; it is nonempty since $q{\le }^{\ast }q$.

If $p{\le }^{\ast }q$, transitivity from F1 shows that every $r\in e(p)$ is in $e(q)$, so $e(p)\subseteq e(q)$. Conversely that inclusion puts $p\in e(q)$, since $p\in e(p)$, and step 1.1 gives $p{\le }^{\ast }q$. A common original extension $r\le p,q$ belongs to $e(p)\cap e(q)$. Conversely if $r$ belongs to the intersection, $r{\le }^{\ast }p,q$. First choose $s\le r,p$, then, because $s\le r$, choose $t\le s,q$. This $t$ is a common original extension of $p,q$. Thus the two displayed equivalences hold. By F2, a nonempty intersection is exactly a nonzero Boolean meet, which is equivalent to compatibility in the Boolean algebra's nonzero part: the meet itself is a common nonzero lower bound, and any such bound lies below the meet.

Let $U$ be a nonzero regular open, so $U\mathrm{\ne }\mathrm{\varnothing }$. Take one $p\in U$. Downward openness gives $\downarrow p\subseteq U$, and regularization is monotone, so $e(p)\subseteq \mathrm{int}\bar{U}=U$. Step 1.1 gives $e(p)\mathrm{\ne }\mathrm{\varnothing }$. This proves density among nonzero Boolean elements. If $P$ is separative, F1 and step 2.1 make $e$ an order embedding, hence injective by antisymmetry. For a general preorder, step 2.1 makes $e$ constant exactly on the mutual-${\le }^{\ast }$ classes, and gives a well-defined injective order map from the quotient with the same range. F1 and step 2.1 give compatibility preservation and reflection for that map. Alternatively the same construction can be applied directly to the quotient. When $P$ has one element, its open algebra is $\{\mathrm{\varnothing },P\}$ and its single condition maps to $P$; the Boolean zero is excluded from the target forcing order. Empty preorders are outside the stated convention. Every witness selection above is finite, and neither a filter extension nor a maximal-family argument occurs. QED.