AI 中文总结
本文证明有限图H存在有限删除诱导饱和图当且仅当H非完全图，解决删除猜想，方法结合自由合并、局部提升定理及半立方体构造。
AI 中文摘要
图$G$对于$H$是删除诱导饱和的，如果$G$有一条边，不包含$H$的诱导副本，并且删除$G$的任何一条边都会产生$H$的诱导副本。我们通过有限证书验证证明了：有限图$H$存在这样的有限图$G$当且仅当$H$不是完全图。这解决了Fan、Hajebi、Hajebi和Spirkl的删除猜想。主要步骤利用Auinger、Bitterlich和Otto的局部提升定理，将合适的自由合并转移到有限扩张。第二个判据通过保护指定的非边然后取最大诱导$H$-自由完备化来处理边的添加。Bonamy、Groenland、Johnston、Morrison和Scott的结构性结果将剩余目标缩减为稠密模板和有限遗传类。在半立方体中的两个统一构造处理稠密模板。有限部分由穷举覆盖证书、结构证书和显式宿主支持，包括一个30个顶点的循环图。
英文摘要
A graph $G$ is deletion-induced-saturated for $H$ if $G$ has an edge, contains no induced copy of $H$, and deleting any edge of $G$ creates an induced copy of $H$. We prove, with finite certificate verification, that a finite graph $H$ admits such a finite graph $G$ if and only if $H$ is not complete. This resolves the deletion conjecture of Fan, Hajebi, Hajebi and Spirkl. The main step transfers suitable free amalgamations to finite extensions using a local lifting theorem of Auinger, Bitterlich and Otto. A second criterion treats edge addition by protecting specified nonedges and then taking a maximal induced-$H$-free completion. Structural results of Bonamy, Groenland, Johnston, Morrison and Scott reduce the remaining targets to dense templates and a finite hereditary class. Two uniform constructions in halved cubes handle the dense templates. The finite part is supported by exhaustive coverage certificates, structural certificates and explicit hosts, including a circulant graph on $30$ vertices.
Comments16 pages. Computer-assisted proof
