Hamiltonian packings with prescribed symmetry in de Bruijn graphs
Justin Lyson · Zenodo (CERN European Organization for Nuclear Research) · 2026
This preprint presents a constructive proof of Kása’s fixed-symmetry conjecture for directed de Bruijn graphs. For every alphabet size q > 2 and word length k ≥ 2, it constructs a Hamiltonian cycle whose q−1 images under the alphabet permutation fixing 0 and cycling 1 through q−1 are pairwise arc-disjoint, including their closing arcs. The construction also gives an optimal packing of q−1 Hamiltonian cycles. The argument combines initial constructions with a lifting and cycle-joining procedure that preserves the prescribed symmetry. The manuscript describes an associated Lean 4 formalization and its verification evidence and reproducibility limitations. This version is an author-review preprint and has not undergone independent specialist peer review. The accompanying source archive contains the manuscript sources, Lean 4 formalization, checking code, reproduction instructions and verification records. All 950 project modules were freshly rebuilt and all five audit harnesses passed, using pinned external library objects. The manuscript is licensed under CC BY 4.0; the original Lean sources and checking software are licensed under Apache License 2.0. Third-party materials retain their existing licenses. The archive documents the license scope for each file.