{"id":"palomar/PALOMAR-2026-10-27-000007","url":"https://github.com/methuku-git-hub/Nearly-linear-directed-cycles-in-vertex-transitive-digraphs/tree/16f43c7731a2d973e989c5e9006b62088dd3068d/directed-cycles-lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000007-v1.json","repo":"https://github.com/methuku-git-hub/Nearly-linear-directed-cycles-in-vertex-transitive-digraphs","tags":["math.CO","msc:05C20","msc:05C38"],"score":0,"title":"Nearly linear directed cycles in vertex-transitive digraphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Abhishek Methuku"],"reviews":0,"subject":"math.CO","summary":"Formalization of the near-linear directed-cycle theorem: for every real epsilon greater than zero, all sufficiently large finite connected vertex-transitive loopless digraphs on n vertices contain a simple directed cycle of length at least n^(1-epsilon). Connectedness means connectedness of the underlying undirected graph; cycles of length two are allowed. This is Theorem 1.5 of the archived revised manuscript by Bowen Li and Abhishek Methuku, with repaired arguments and replacement lemmas in its proof dependencies. It does not assert Hamiltonicity.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Nearly linear directed cycles in vertex-transitive digraphs","identifier":"Revised manuscript, Theorem 1.5; source SHA-256 ec10beaeb937736b36c081a4ca7fb25b1b1ea34f8a614acda7a4ee45cded9543","relationship":"formalizes"},{"title":"A finitary structure theorem for vertex-transitive graphs of polynomial growth","identifier":"Combinatorica 41 (2021), 263–298; doi:10.1007/s00493-020-4295-6","relationship":"adapts"}]}