An infinite family of doubly saturated $R(3,t)$-good graphs
Abhishek Saigal, Akaash R. Parthasarathy
math.CO
Aug 6, 2026 · v1
cs.DM
TL;DR
A complete proof that an explicit circulant graph family is doubly saturated R(3,t)-good, including executable checkers, is formalized in Lean 4 with Mathlib.
Abstract
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$.
Problem
Przybocki, Mackey, Heule, and Subercaseaux conjectured that an explicit circulant graph on 5t-10 vertices is doubly saturated R(3,t)-good for odd t >= 17. Establishing this also bounds the minimum order DS(3,t).
Approach
The paper proves triangle-freeness and maximal triangle-freeness via a cyclic sumset identity in Z_n, showing C+C = Z_n \ C. The independence bound alpha=t-1 uses a five-layer fiber reduction, a uniform affine finite-state certificate for m >= 30, and an exhaustive Boolean checker for 8 <= m <= 29. Deletion-criticality follows from eight explicit families of independent-set witnesses. The full argument, including checker soundness, is formalized in Lean 4.32.2 with Mathlib, using native_decide for finite-state portions.
Results
The conjecture (Conjecture 2 of Przybocki et al.) is settled for all odd t >= 17, yielding 2t-1 <= DS(3,t) <= 5t-10. The Lean development contains no sorry, admit, unsafe, or user-added axioms.
