关于小拟核猜想的一个结果

本工作中任何有向图$D=(V(D),A(D))$均假定为有限且无自环。有向图中的源是至少有一个入弧的顶点。拟核$Q\subseteq V(D)$是$D$中的独立集，使得$V(D)$中每个顶点可从$Q$中某顶点至多两步到达。每个无源有向图是否具有大小不超过$|V(D)|/2$的拟核，即所谓小拟核猜想（SQKC），是一个未决问题。本文旨在有向图某一结构性质假设下证明SQKC。这将SQKC与存在顶点$u\in V(D)$以及当从$D$中移除$u$及其外邻域时新出现源的数量界相联系。本工作的结果具有技术性，因此额外借助Coq证明辅助器予以验证。