[proofplan] We prove first that the regular-open embedding is dense by unpacking the regular-open topology of the forcing poset: every non-zero regular [open set](/page/Open%20Set) contains a basic open neighbourhood generated by some condition. A $P$-generic filter then induces an upward closed Boolean filter by taking all Boolean elements above some embedded condition, and genericity is transferred by pulling dense subsets of $B^+$ back along $e$. Conversely, a Boolean-generic ultrafilter induces a $P$-generic filter by taking the preimage of the ultrafilter under $e$. Finally, we compare the two forcing extensions by recursively translating $P$-names into $B$-names and $B$-names into $P$-names, proving by induction on rank that valuation is preserved. [/proofplan]

[step:Define the canonical regular-open embedding and prove its density]For each $p\in P$, define the basic open cone below $p$ by \begin{align*} N_p=\{q\in P:q\le_P p\}. \end{align*} The forcing topology on $P$ has the sets $N_p$ as a base, and $B=\operatorname{RO}(P)$ is the complete Boolean algebra of regular open subsets of this topology. The canonical embedding is the map \begin{align*} e:P&\to B^+,\quad p\mapsto \operatorname{int}(\overline{N_p}), \end{align*} where closure and interior are taken in the forcing topology on $P$. We first show that $e(p)\neq 0_B$ for every $p\in P$. Since $N_p\subseteq \operatorname{int}(\overline{N_p})$, the set $e(p)$ contains $p$, hence is non-empty. Therefore $e(p)\in B^+$. The map $e$ is order preserving: if $p\le_P q$, then $N_p\subseteq N_q$, hence \begin{align*} \operatorname{int}(\overline{N_p})\subseteq \operatorname{int}(\overline{N_q}), \end{align*} so $e(p)\le_B e(q)$. We also record the order-reflection property used below. If $e(q)\le_B e(p)$ and $q\not\le_P p$, separativity of $P$ gives $r\le_P q$ such that $r$ is incompatible with $p$. Then $e(r)\le_B e(q)\le_B e(p)$ by order preservation, while incompatibility gives $e(r)\wedge e(p)=0_B$, contradicting $e(r)\in B^+$. Hence \begin{align*} e(q)\le_B e(p)\implies q\le_P p. \end{align*} Now let $b\in B^+$. Since $b$ is a non-empty open subset of $P$ in the forcing topology, there exists $p\in b$ and a basic open neighbourhood $N_p$ with $N_p\subseteq b$. Because $b$ is regular open and $N_p\subseteq b$, we have \begin{align*} e(p)=\operatorname{int}(\overline{N_p})\subseteq \operatorname{int}(\overline{b})=b. \end{align*} Thus $e(p)\le_B b$. Therefore $e[P]$ is dense in $B^+$.[/step]

[guided]The Boolean completion is built so that ordinary forcing conditions become regular open sets. For a condition $p\in P$, the relevant open set is not just the cone $N_p=\{q\in P:q\le_P p\}$, but its regular-open hull: \begin{align*} e(p)=\operatorname{int}(\overline{N_p}). \end{align*} This ensures that $e(p)$ belongs to $\operatorname{RO}(P)$, because regular open sets are exactly those open sets $u$ satisfying $u=\operatorname{int}(\overline{u})$. We verify first that $e(p)$ is non-zero. The set $N_p$ contains $p$, and $N_p\subseteq \operatorname{int}(\overline{N_p})$ because $N_p$ is open and contained in its own closure. Hence $e(p)$ is non-empty, so $e(p)\in B^+$. Next, suppose $p\le_P q$. Then every extension of $p$ is also an extension of $q$, so $N_p\subseteq N_q$. Taking closures preserves inclusion, and taking interiors preserves inclusion, so \begin{align*} e(p)=\operatorname{int}(\overline{N_p})\subseteq \operatorname{int}(\overline{N_q})=e(q). \end{align*} Thus $e$ respects the forcing order and the Boolean order. The embedding also reflects the order. Suppose $e(q)\le_B e(p)$. If $q\not\le_P p$, separativity of $P$ provides a condition $r\le_P q$ incompatible with $p$. Order preservation gives $e(r)\le_B e(q)\le_B e(p)$, but incompatibility means that no condition can lie below both $r$ and $p$, so $e(r)\wedge e(p)=0_B$. This contradicts $e(r)\neq 0_B$. Therefore $q\le_P p$. The density argument is the point of passing to regular open sets. Let $b\in B^+$ be non-zero. Since $b$ is a non-empty open subset of the forcing topology, some condition $p\in P$ has its basic neighbourhood contained in $b$: \begin{align*} N_p\subseteq b. \end{align*} Because $b$ is regular open, taking the regular-open hull of $N_p$ still remains inside $b$: \begin{align*} e(p)=\operatorname{int}(\overline{N_p})\subseteq \operatorname{int}(\overline{b})=b. \end{align*} Therefore every non-zero Boolean condition has a stronger condition coming from $P$, which is exactly the density of $e[P]$ in $B^+$.[/guided]

[step:Construct a Boolean-generic ultrafilter from a $P$-generic filter]Let $G\subset P$ be $P$-generic over $M$, and define \begin{align*} H=\{b\in B:\exists p\in G\text{ such that }e(p)\le_B b\}. \end{align*} The set $H$ is upward closed in $B$ by definition. To see that $H$ is closed under finite meets, let $b_0,b_1\in H$. Choose $p_0,p_1\in G$ such that $e(p_0)\le_B b_0$ and $e(p_1)\le_B b_1$. Since $G$ is a filter, there is $r\in G$ with $r\le_P p_0$ and $r\le_P p_1$. Order preservation of $e$ gives \begin{align*} e(r)\le_B e(p_0)\wedge e(p_1)\le_B b_0\wedge b_1. \end{align*} Thus $b_0\wedge b_1\in H$. Also $0_B\notin H$. If $0_B\in H$, then for some $p\in G$ we would have $e(p)\le_B 0_B$, contradicting $e(p)\in B^+$. We next prove that $H$ is an ultrafilter. Fix $b\in B\cap M$. Define \begin{align*} D_b=\{p\in P:e(p)\le_B b\text{ or }e(p)\le_B \neg b\}. \end{align*} We show that $D_b$ is dense in $P$. Given $p\in P$, the Boolean element $e(p)$ is non-zero. Since \begin{align*} e(p)=\bigl(e(p)\wedge b\bigr)\vee\bigl(e(p)\wedge \neg b\bigr), \end{align*} at least one of $e(p)\wedge b$ and $e(p)\wedge\neg b$ is non-zero. If $e(p)\wedge b\neq 0_B$, density of $e[P]$ in $B^+$ gives $q\in P$ with $e(q)\le_B e(p)\wedge b$, and then $q\le_P p$ by separativity of the canonical embedding, so $q\in D_b$. The case $e(p)\wedge\neg b\neq 0_B$ is identical, producing $q\le_P p$ with $e(q)\le_B\neg b$. Thus $D_b$ is dense. Since $D_b\in M$ and $G$ is $P$-generic over $M$, choose $p\in G\cap D_b$. Then either $e(p)\le_B b$, giving $b\in H$, or $e(p)\le_B\neg b$, giving $\neg b\in H$. Since $H$ is proper, it cannot contain both $b$ and $\neg b$. Therefore $H$ is an ultrafilter on $B$. Finally let $D\in M$ be dense in $B^+$. Define \begin{align*} D^P=\{p\in P:\exists d\in D\text{ such that }e(p)\le_B d\}. \end{align*} The set $D^P$ is dense in $P$: given $p\in P$, choose $d\in D$ with $d\le_B e(p)$, then choose $q\in P$ with $e(q)\le_B d$ by density of $e[P]$. Hence $q\le_P p$ and $q\in D^P$. Since $D^P\in M$, choose $p\in G\cap D^P$. Then for some $d\in D$ we have $e(p)\le_B d$, so $d\in H\cap D$. Thus $H$ meets every [dense subset](/page/Dense%20Subset) of $B^+$ belonging to $M$, and $H$ is $M$-generic.[/step]

[guided]Define \begin{align*} H=\{b\in B:\exists p\in G\text{ such that }e(p)\le_B b\}. \end{align*} This set is upward closed by construction. If $b_0,b_1\in H$, choose $p_0,p_1\in G$ with $e(p_0)\le_B b_0$ and $e(p_1)\le_B b_1$. Since $G$ is a filter on $P$, there is $r\in G$ with $r\le_P p_0$ and $r\le_P p_1$. Order preservation gives \begin{align*} e(r)\le_B e(p_0)\wedge e(p_1)\le_B b_0\wedge b_1. \end{align*} Hence $b_0\wedge b_1\in H$. Also $0_B\notin H$, because $0_B\in H$ would give $p\in G$ with $e(p)\le_B0_B$, contradicting $e(p)\in B^+$. To prove maximality, fix $b\in B\cap M$ and define \begin{align*} D_b=\{p\in P:e(p)\le_B b\text{ or }e(p)\le_B \neg b\}. \end{align*} For any $p\in P$, the Boolean element $e(p)$ is non-zero and decomposes as \begin{align*} e(p)=\bigl(e(p)\wedge b\bigr)\vee\bigl(e(p)\wedge\neg b\bigr). \end{align*} At least one of the two meets is non-zero. If $e(p)\wedge b\neq0_B$, density of $e[P]$ gives $q\in P$ with $e(q)\le_B e(p)\wedge b$. The order-reflection property proved above gives $q\le_P p$, and $q\in D_b$. The case $e(p)\wedge\neg b\neq0_B$ is the same. Thus $D_b$ is dense. Since $D_b\in M$ and $G$ is $P$-generic over $M$, choose $p\in G\cap D_b$. Then either $b\in H$ or $\neg b\in H$. Properness prevents both, so $H$ is an ultrafilter. Now let $D\in M$ be dense in $B^+$. Define \begin{align*} D^P=\{p\in P:\exists d\in D\text{ such that }e(p)\le_B d\}. \end{align*} Given $p\in P$, choose $d\in D$ with $d\le_B e(p)$, then use density of $e[P]$ to choose $q\in P$ with $e(q)\le_B d$. Order reflection gives $q\le_P p$, and $q\in D^P$. Thus $D^P$ is dense in $P$. Since $D^P\in M$, choose $p\in G\cap D^P$. Then $e(p)\le_B d$ for some $d\in D$, so $d\in H\cap D$. Therefore $H$ meets every dense subset of $B^+$ in $M$, which is exactly $M$-genericity.[/guided]

[step:Recover a $P$-generic filter from a Boolean-generic ultrafilter]Let $H\subset B$ be an $M$-generic ultrafilter, and define \begin{align*} G=\{p\in P:e(p)\in H\}. \end{align*} The set $G$ is non-empty because $e[P]$ is dense in $B^+$ and $H\cap B^+$ is $B^+$-generic over $M$. If $p\in G$ and $p\le_P q$, then $e(p)\le_B e(q)$, so upward closure of $H$ gives $e(q)\in H$, hence $q\in G$. If $p_0,p_1\in G$, then $e(p_0),e(p_1)\in H$, so \begin{align*} e(p_0)\wedge e(p_1)\in H. \end{align*} Because $H$ is proper, this meet is non-zero. By density of $e[P]$, choose $r\in P$ such that \begin{align*} e(r)\le_B e(p_0)\wedge e(p_1). \end{align*} Then $r\le_P p_0$ and $r\le_P p_1$, and $e(r)\in H$, so $r\in G$. Thus $G$ is a filter on $P$. Let $D\in M$ be dense in $P$. Define \begin{align*} E_D=\{e(p):p\in D\}. \end{align*} The set $E_D$ is dense in $B^+$. Indeed, given $b\in B^+$, choose $q\in P$ with $e(q)\le_B b$ by density of $e[P]$. Since $D$ is dense in $P$, choose $p\in D$ with $p\le_P q$. Order preservation of $e$ gives \begin{align*} e(p)\le_B e(q)\le_B b. \end{align*} Thus every $b\in B^+$ has a stronger element of $E_D$ below it. Since $D\in M$ and $e\in M$, we have $E_D\in M$. Because $H\cap B^+$ is $B^+$-generic over $M$, choose an element of $H\cap E_D$. By definition of $E_D$, this element has the form $e(p)$ for some $p\in D$. Hence $e(p)\in H$, so $p\in G\cap D$. Therefore $G$ meets every dense subset of $P$ in $M$, so $G$ is $P$-generic over $M$. It remains to identify the Boolean ultrafilter generated from this recovered $G$ with the original $H$. Define \begin{align*} K=\{b\in B:\exists p\in G\text{ such that }e(p)\le_B b\}. \end{align*} If $b\in K$, then $e(p)\in H$ for some $p\in G$ and $e(p)\le_B b$, so upward closure of $H$ gives $b\in H$. Thus $K\subseteq H$. Conversely let $b\in H$. Since $H$ is proper, $b\neq 0_B$. Define \begin{align*} E_b=\{e(p):p\in P\text{ and }e(p)\le_B b\}\cup\{c\in B^+:c\le_B\neg b\}. \end{align*} The set $E_b$ belongs to $M$ and is dense in $B^+$. Indeed, given $a\in B^+$, if $a\wedge\neg b\neq 0_B$, then $a\wedge\neg b\in E_b$ and $a\wedge\neg b\le_B a$. If $a\wedge\neg b=0_B$, then $a=a\wedge b$, so $a\le_B b$; density of $e[P]$ in $B^+$ gives $p\in P$ with $e(p)\le_B a\le_B b$, and then $e(p)\in E_b$. Since $H\cap B^+$ is $B^+$-generic over $M$, choose $c\in H\cap E_b$. The second alternative $c\le_B\neg b$ is impossible, because $b\in H$ and $H$ is proper. Therefore $c=e(p)$ for some $p\in P$ with $e(p)\le_B b$. Since $e(p)=c\in H$, we have $p\in G$ and $b\in K$. Therefore $H\subseteq K$, and hence $K=H$.[/step]

[guided]The converse construction gives a filter $G=\{p\in P:e(p)\in H\}$ on the original poset. To use the name-translation argument later, we must check one more compatibility fact: if we rebuild a Boolean ultrafilter from this recovered $G$, we recover the same ultrafilter $H$ we started with. Define \begin{align*} K=\{b\in B:\exists p\in G\text{ such that }e(p)\le_B b\}. \end{align*} The inclusion $K\subseteq H$ follows directly from the definition of $G$. If $b\in K$, then $e(p)\le_B b$ for some $p\in G$. Since $p\in G$ means $e(p)\in H$, and since an ultrafilter is upward closed, $b\in H$. For the reverse inclusion, fix $b\in H$. Since $H$ is proper, $b\neq 0_B$. We need an embedded condition $e(p)$ which lies in $H$ and sits below $b$. Density of $e[P]$ alone gives embedded conditions below $b$, but it does not guarantee that the embedded condition belongs to the ultrafilter. We force that membership by meeting a dense set tailored to $b$. Define \begin{align*} E_b=\{e(q):q\in P\text{ and }e(q)\le_B b\}\cup\{c\in B^+:c\le_B\neg b\}. \end{align*} This set belongs to $M$ because $P$, $B$, $e$, $b$, and the Boolean order all belong to $M$. It is dense in $B^+$. To see this, take $a\in B^+$. If $a\wedge\neg b\neq 0_B$, then $a\wedge\neg b\in E_b$ and $a\wedge\neg b\le_B a$. If $a\wedge\neg b=0_B$, then the Boolean decomposition $a=(a\wedge b)\vee(a\wedge\neg b)$ gives $a=a\wedge b$, hence $a\le_B b$. By density of $e[P]$, choose $q\in P$ with $e(q)\le_B a\le_B b$; then $e(q)\in E_b$ and lies below $a$. Since $H\cap B^+$ is $B^+$-generic over $M$, it meets $E_b$. Choose $c\in H\cap E_b$. The alternative $c\le_B\neg b$ cannot occur, because then $b\wedge c=0_B$ would belong to $H$, contradicting propriety. Therefore $c=e(p)$ for some $p\in P$ with $e(p)\le_B b$. Since $e(p)=c\in H$, we have $p\in G$, and the inequality $e(p)\le_B b$ shows $b\in K$. We have proved $K\subseteq H$ and $H\subseteq K$, so $K=H$. This identification is what allows the later valuation comparison to use the original Boolean ultrafilter $H$, not merely a newly generated one.[/guided]

[step:Translate $P$-names into Boolean names without changing valuation]We now prove that the extension generated by a $P$-generic filter is contained in the extension generated by its associated Boolean ultrafilter. For each $P$-name $\sigma\in M$, define recursively a $B$-name $\widehat{\sigma}\in M$ by \begin{align*} \widehat{\sigma}=\{(\widehat{\rho},e(p)):(\rho,p)\in\sigma\}. \end{align*} This recursion is well-founded because every name is defined from names of smaller rank. We prove by induction on the rank of $\sigma$ that \begin{align*} \widehat{\sigma}^{\,H}=\sigma^G. \end{align*} By the definition of valuation for $P$-names, \begin{align*} x\in\sigma^G\iff \exists(\rho,p)\in\sigma\text{ such that }p\in G\text{ and }x=\rho^G. \end{align*} By the definition of $G$ and $H$, the condition $p\in G$ is equivalent to $e(p)\in H$. By the induction hypothesis, $\rho^G=\widehat{\rho}^{\,H}$. Therefore \begin{align*} x\in\sigma^G\iff \exists(\widehat{\rho},e(p))\in\widehat{\sigma}\text{ such that }e(p)\in H\text{ and }x=\widehat{\rho}^{\,H}. \end{align*} The right-hand side is exactly $x\in\widehat{\sigma}^{\,H}$. Hence $\sigma^G=\widehat{\sigma}^{\,H}$ for every $P$-name $\sigma\in M$. Therefore every element of $M[G]$ belongs to $M[H]$.[/step]

[guided]The goal is to show that no new set is lost when we replace the forcing poset $P$ by its Boolean completion $B$. A $P$-name is a set of pairs $(\rho,p)$, where $\rho$ is a smaller $P$-name and $p\in P$ is the condition deciding that $\rho$ appears. Since $P$ sits inside $B$ through $e$, the natural translation is to keep the name part and replace the condition $p$ by the Boolean condition $e(p)$. Formally, for every $P$-name $\sigma\in M$, define the Boolean name $\widehat{\sigma}$ recursively by \begin{align*} \widehat{\sigma}=\{(\widehat{\rho},e(p)):(\rho,p)\in\sigma\}. \end{align*} This is a legitimate recursion because the names $\rho$ appearing inside $\sigma$ have smaller rank than $\sigma$. We prove by induction on rank that valuation is preserved: \begin{align*} \widehat{\sigma}^{\,H}=\sigma^G. \end{align*} Fix a set $x$. By the valuation rule for $P$-names, \begin{align*} x\in\sigma^G\iff \exists(\rho,p)\in\sigma\text{ such that }p\in G\text{ and }x=\rho^G. \end{align*} The definition of the recovered filter says exactly that $p\in G$ iff $e(p)\in H$. Also, by the induction hypothesis applied to the smaller name $\rho$, we have \begin{align*} \rho^G=\widehat{\rho}^{\,H}. \end{align*} Substituting these two equivalences into the valuation formula gives \begin{align*} x\in\sigma^G\iff \exists(\widehat{\rho},e(p))\in\widehat{\sigma}\text{ such that }e(p)\in H\text{ and }x=\widehat{\rho}^{\,H}. \end{align*} But the right-hand side is precisely the Boolean valuation rule for $\widehat{\sigma}$ by $H$. Hence $x\in\sigma^G$ iff $x\in\widehat{\sigma}^{\,H}$ for every set $x$, so $\sigma^G=\widehat{\sigma}^{\,H}$. Thus each set obtained by interpreting a $P$-name with $G$ is also obtained by interpreting a Boolean name with $H$. This proves $M[G]\subseteq M[H]$.[/guided]

[step:Translate Boolean names into $P$-names without changing valuation]It remains to prove the reverse inclusion. Let $\tau\in M$ be a $B$-name. We use the standard functional presentation of complete Boolean-valued names: after joining duplicate coefficients, $\tau$ is a function whose domain $\operatorname{dom}(\tau)$ is a set of smaller $B$-names and whose value $\tau(\rho)\in B$ is the Boolean coefficient attached to $\rho$. This is equivalent to the pair presentation of names, since a set of pairs can be replaced by the function assigning to each name the join of all Boolean coefficients paired with it. Since $B=\operatorname{RO}(P)$ is a complete Boolean algebra and $M$ is a transitive model of ZFC, arbitrary joins of sets of elements of $B$ that belong to $M$ exist in $B\cap M$, and [Zorn's lemma](/theorems/1226) may be applied inside $M$ to set-sized partially ordered collections in $M$. For each $\rho\in\operatorname{dom}(\tau)$ with $\tau(\rho)\neq 0_B$, define in $M$ the partially ordered collection $\mathcal{A}_{\tau,\rho}$ of all antichains $A\subset P$ such that \begin{align*} \forall p\in A\quad e(p)\le_B\tau(\rho), \end{align*} ordered by inclusion. This collection belongs to $M$, because $P$, $B$, $e$, $\tau$, $\rho$, and the Boolean order relation all belong to $M$. Every chain in $\mathcal{A}_{\tau,\rho}$ has union again an antichain satisfying the same bound below $\tau(\rho)$, so Zorn's lemma in $M$ gives a maximal member $A_{\tau,\rho}\subset P$. We verify that this maximality gives the Boolean join \begin{align*} \bigvee_{p\in A_{\tau,\rho}}e(p)=\tau(\rho). \end{align*} The left-hand side is at most $\tau(\rho)$ because every $e(p)$ lies below $\tau(\rho)$. If the difference \begin{align*} c=\tau(\rho)\wedge\neg\bigvee_{p\in A_{\tau,\rho}}e(p) \end{align*} were non-zero, density of $e[P]$ in $B^+$ would give $q\in P$ with $e(q)\le_B c$. Then $q$ is incompatible in $P$ with every $p\in A_{\tau,\rho}$, because otherwise a common extension $r\le_P p,q$ would satisfy $0_B\neq e(r)\le_B e(p)\wedge e(q)$, contradicting $e(q)\le_B\neg e(p)$. Hence $A_{\tau,\rho}\cup\{q\}$ is a larger member of $\mathcal{A}_{\tau,\rho}$, contradicting maximality. Thus $c=0_B$, proving the displayed join equality. If $\tau(\rho)=0_B$, set $A_{\tau,\rho}=\varnothing$. Define recursively a $P$-name $\tau^*\in M$ by \begin{align*} \tau^*=\{(\rho^*,p):\rho\in\operatorname{dom}(\tau)\text{ and }p\in A_{\tau,\rho}\}. \end{align*} We prove by induction on the rank of $\tau$ that \begin{align*} (\tau^*)^G=\tau^H. \end{align*} Fix a set $x$. By the valuation rule for Boolean names, \begin{align*} x\in\tau^H\iff \exists\rho\in\operatorname{dom}(\tau)\text{ such that }\tau(\rho)\in H\text{ and }x=\rho^H. \end{align*} For each $\rho$, we prove \begin{align*} \tau(\rho)\in H\iff \exists p\in A_{\tau,\rho}\text{ such that }e(p)\in H. \end{align*} If $e(p)\in H$ for some $p\in A_{\tau,\rho}$, then $e(p)\le_B\tau(\rho)$, so upward closure of $H$ gives $\tau(\rho)\in H$. Conversely, assume $\tau(\rho)\in H$. If $\tau(\rho)=0_B$, this contradicts propriety of $H$, so $\tau(\rho)\neq 0_B$. The set \begin{align*} C_{\tau,\rho}=\{\neg\tau(\rho)\}\cup\{e(p):p\in A_{\tau,\rho}\} \end{align*} is a maximal antichain of $B$ belonging to $M$, because the elements $e(p)$ for $p\in A_{\tau,\rho}$ are pairwise incompatible below $\tau(\rho)$ and their join is $\tau(\rho)$. Since $H$ is $M$-generic, it meets the dense downward closure of the maximal antichain $C_{\tau,\rho}$, using the standard maximal-antichain characterization of generic filters; equivalently, as $H$ is an ultrafilter, it contains exactly one member of $C_{\tau,\rho}$. It cannot contain $\neg\tau(\rho)$ because it contains $\tau(\rho)$ and is proper. Therefore $e(p)\in H$ for some $p\in A_{\tau,\rho}$. Since $e(p)\in H$ is equivalent to $p\in G$, and the induction hypothesis gives $\rho^H=(\rho^*)^G$, we obtain \begin{align*} x\in\tau^H\iff \exists\rho\in\operatorname{dom}(\tau)\exists p\in A_{\tau,\rho}\text{ such that }p\in G\text{ and }x=(\rho^*)^G. \end{align*} The right-hand side is exactly $x\in(\tau^*)^G$. Therefore $\tau^H=(\tau^*)^G$ for every $B$-name $\tau\in M$, and so $M[H]\subseteq M[G]$.[/step]

[guided]The reverse translation is subtler than the first one because a Boolean name may attach an arbitrary Boolean value $\tau(\rho)$ to a smaller name $\rho$, while a $P$-name must attach actual conditions from $P$. The dense embedding lets us refine each non-zero Boolean value into a maximal antichain of embedded $P$-conditions below it. We represent the Boolean name $\tau$ as a function: $\operatorname{dom}(\tau)$ is the set of smaller Boolean names appearing in $\tau$, and $\tau(\rho)\in B$ is the Boolean coefficient of $\rho$. This is equivalent to the set-of-pairs presentation because duplicate coefficients for the same $\rho$ can be joined in the complete Boolean algebra $B$. Here we use two structural facts. First, $B=\operatorname{RO}(P)$ is complete, so joins such as $\bigvee_{p\in A}e(p)$ exist for every set $A\in M$. Second, $M$ is a transitive model of ZFC, so Zorn's lemma is available inside $M$ for the set-sized collections of antichains we are about to define. For each $\rho\in\operatorname{dom}(\tau)$ with $\tau(\rho)\neq 0_B$, consider in $M$ the collection of antichains $A\subset P$ such that every $p\in A$ satisfies $e(p)\le_B\tau(\rho)$. This collection is a set in $M$, and the union of any inclusion-chain of such antichains is again such an antichain. Zorn's lemma in $M$ gives a maximal antichain $A_{\tau,\rho}$ below $\tau(\rho)$. Why does this antichain cover the whole Boolean value $\tau(\rho)$? Since every $e(p)$ lies below $\tau(\rho)$, the join is at most $\tau(\rho)$. If the leftover Boolean value \begin{align*} c=\tau(\rho)\wedge\neg\bigvee_{p\in A_{\tau,\rho}}e(p) \end{align*} were non-zero, density of $e[P]$ would give $q\in P$ with $e(q)\le_B c$. Then $q$ is incompatible with every element of $A_{\tau,\rho}$, so adding $q$ would contradict maximality. Therefore \begin{align*} \bigvee_{p\in A_{\tau,\rho}}e(p)=\tau(\rho). \end{align*} Define the translated $P$-name by \begin{align*} \tau^*=\{(\rho^*,p):\rho\in\operatorname{dom}(\tau)\text{ and }p\in A_{\tau,\rho}\}. \end{align*} We prove by induction on rank that $(\tau^*)^G=\tau^H$. For a fixed set $x$, Boolean valuation gives \begin{align*} x\in\tau^H\iff \exists\rho\in\operatorname{dom}(\tau)\text{ such that }\tau(\rho)\in H\text{ and }x=\rho^H. \end{align*} The antichain equality implies \begin{align*} \tau(\rho)\in H\iff \exists p\in A_{\tau,\rho}\text{ such that }e(p)\in H. \end{align*} Indeed, the forward direction follows because an ultrafilter meeting the maximal antichain below $\tau(\rho)$ must contain one of its members; the reverse direction follows from upward closure. Since $e(p)\in H$ is equivalent to $p\in G$, and the induction hypothesis gives $\rho^H=(\rho^*)^G$, we obtain \begin{align*} x\in\tau^H\iff \exists\rho\in\operatorname{dom}(\tau)\exists p\in A_{\tau,\rho}\text{ such that }p\in G\text{ and }x=(\rho^*)^G. \end{align*} This is exactly the valuation rule for $(\tau^*)^G$. Hence $\tau^H=(\tau^*)^G$, proving $M[H]\subseteq M[G]$.[/guided]

[step:Conclude that the two generic extensions are equal] From the translation of $P$-names to $B$-names, every element of $M[G]$ belongs to $M[H]$. From the translation of $B$-names to $P$-names, every element of $M[H]$ belongs to $M[G]$. Therefore \begin{align*} M[G]=M[H]. \end{align*} This completes the proof of the density of the canonical embedding, the equivalence of $P$-generic filters and Boolean-generic ultrafilters, and the equality of the corresponding generic extensions. [/step]