Forcing equivalence and Boolean completion

Let $\pi :P\to S=P\mathrm{/}\sim$ be the quotient in F1. It preserves order and both compatibility directions. It is onto, hence has dense image: every class has some representative, and its own class is below itself. This uses the representative of one specified class at a time, not a choice of representatives of all classes. Therefore $\pi$ meets all of F3's hypotheses, even though it may fail to reflect the original order or to be injective.

In the downward-open topology on $P$, F2 constructs $B=\mathrm{RO}(P)$ and $e(p)=\mathrm{int}\overline{\downarrow p}$. It proves $e(p)\subseteq e(q)$ iff $p{\le }^{\ast }q$ and nonzero intersection iff original compatibility, and proves image density in $B\setminus \{0_B\}$. Thus $e$ too meets F3's hypotheses. Factoring through the quotient gives the dense order embedding $[p]\mapsto e(p)$ of $S$. The factor is well-defined and injective because mutual inclusion of the regular opens is exactly mutual ${\le }^{\ast }$. A nonzero Boolean meet is a common nonzero lower bound, so Boolean compatibility is exactly nonzero intersection.

Apply F3 separately to $\pi$, to $e$, and to the factored dense embedding. In each case its explicit $T$ translates coefficients forward and its $R$ uses all coefficients whose images refine an original coefficient. Both fixed-formula forcing directions follow, including existential names, from its syntactic proof. For supplied generics its inverse-image/upward-image maps are inverse, and its two valuation equalities give both inclusions between the generic extensions. In particular all three presentations produce the same extensions. This conclusion uses the proved forced equality of round-trip names; it does not identify their sets of pairs literally.

Finally an arbitrary dense order embedding $j:P\to Q$ has the same properties. Order preservation preserves compatibility. If $j(p),j(r)$ have a common lower bound $q$, image density supplies $j(s)\le q$; order reflection gives $s\le p,r$, proving compatibility reflection. F3 therefore applies to this embedding as well. The singleton preorder yields the two-element regular-open algebra and its singleton nonzero part. Boolean zero is excluded because the nonzero image cannot be dense below zero in the full algebra; retaining zero still gives a preorder in the two-element case, but not the dense target required by F3. All uses of F1–F3 are in ZF, and no filter-extension principle is involved. [F1, F2, F3, step 2.1] QED.