Solution (source code)

= Solution

With this paper's order convention, larger conditions are stronger. A <generic filter> $G\subseteq P$ over $M$ is nonempty, closed toward weaker conditions, and directed toward stronger conditions: if $p,q\in G$, some $r\in G$ satisfies $r\ge p,q$. \b[It also meets every $D\in M$ which $M$ regards as dense in $\mathbb P$.]

For a countable transitive $M$, such a filter containing any prescribed condition can be built by enumerating its dense sets and successively choosing stronger conditions in them. The definition does not require $G\notin M$: for an atomic <forcing> a <generic filter> may already belong to $M$.