一类无限双饱和$R(3,t)$-好图族
An infinite family of doubly saturated $R(3,t)$-good graphs
浏览论文内容
中文总结 AI 辅助
该研究针对$t\ge17$的奇数，构造顶点数为$5t-10$的循环双饱和$R(3,t)$-好图，解决了相关猜想，形式化论证并得出$\operatorname{DS}(3,t)$的上下界。
中文摘要 AI 辅助
对于每个满足$t\ge17$的奇数，我们证明了一个顶点数为$5t-10$的显式循环图是双饱和$R(3,t)$-好图。该图无三角形，独立数为$t-1$；添加任意非边会形成三角形，删除任意边会形成阶为$t$的独立集。这解决了Przybocki、Mackey、Heule和Subercaseaux提出的猜想2。利用循环和集恒等式与显式见证证明了局部饱和性质；令$t=2m+1$，通过五层归约，对$m\ge30$用均匀仿射证书证明独立数界，对$8\le m\le29$用穷举校验器证明，校验器的正确性与完整论证在Lean 4.32.2中形式化。由此可得，当$t\ge17$的奇数时，$2t-1\le \operatorname{DS}(3,t)\le 5t-10$。
英文摘要
For every odd integer $t\ge17$, we prove that an explicit circulant graph on $5t-10$ vertices is doubly saturated $R(3,t)$-good. The graph is triangle-free and has independence number $t-1$. Adding any nonedge creates a triangle, whereas deleting any edge creates an independent set of order $t$. This settles Conjecture 2 of Przybocki, Mackey, Heule, and Subercaseaux. A cyclic sumset identity and explicit witnesses prove the local saturation properties. Writing $t=2m+1$, a five-layer reduction proves the independence bound via a uniform affine certificate for $m\ge30$ and an exhaustive checker for $8\le m\le29$. The checker soundness and the complete argument are formalized in Lean 4.32.2. Consequently, $2t-1\le \operatorname{DS}(3,t)\le 5t-10$ for odd $t\ge17$.
