Circular Sorting: A Small Computational Note

One of my professors mentioned a circular-sorting problem from the National Mathematics Olympiad organized by the Iranian Mathematical Society. The question concerned the case where the number of positions is prime. I wasn't at the competition; I only heard about it from him. I found it interesting and wondered what happened when the number of positions was composite.

I asked Astra, an AI model, to explore some composite values and compare them with published bounds. It produced three permutations, for \(n=36,40,42\), whose cycle counts give lower bounds one larger than those in Table 1 of a recent paper [2]. I checked the finite certificates with Lean and a separate Python script. I am posting the details because the examples can be inspected, not because I can establish that they are new.

1. The problem

Place the numbers \(0,1,\ldots,n-1\) around a circle, one at each position. A move swaps any two labels, not necessarily adjacent ones. The goal is to put the labels in cyclic order. Rotating the entire circle does not change the configuration, but reversing it generally does.

For a particular circular configuration, count the fewest swaps needed to sort it. Then maximize that number over all possible configurations. Call the resulting worst-case distance \(x(n)\). The prime case is especially elegant: for a prime \(p\), one has \(x(p)=p-2\). For composite \(n\), the picture is much less complete [1][2].

2. Three examples

Table 1 of the August 2026 version of a paper by Bastide, Bishnoi, Groenland, Gijswijt and Joshi reports the following intervals [2]. Using the same definition of circular sorting, the three permutations in the attached files give a lower endpoint one larger in each case:

This is only a comparison with the bounds reported in that version of the paper. It does not determine \(x(n)\) exactly for any of these values, and it does not mean these examples are the best known today. The upper bounds come from existing work; the attached permutations support the lower bounds.

3. Why cycle counts help

Write a permutation \(p\) in one-line notation: the entry \(p(i)\) gives the label at position \(i\). Let \(r(i)=i+1\pmod n\) denote a rotation, and let \(C(q)\) be the number of disjoint cycles of the permutation \(q\), including fixed points.

A standard fact about permutations is that \(q\) requires \(n-C(q)\) arbitrary transpositions to become the identity. A swap changes the number of cycles by at most one, and a cycle of length \(\ell\) can be broken into singletons using \(\ell-1\) swaps. Applying this to each cycle gives the formula.

Since a sorted circle may be rotated, we are free to choose the most favorable rotation. Consequently,

So, for a lower bound, it is enough to exhibit a permutation with few cycles under every rotation. The attached data show at most four cycles for each of the three permutations, with four attained in at least one rotation. By the standard transposition formula, their distances from the sorted circle are \(n-4\).

4. One explicit example

For \(n=36\), the search returned this permutation in one-line notation, indexed from zero:

p = [17,32,8,24,5,20,14,15,13,19,29,2,
     25,10,12,6,22,7,30,11,16,23,1,28,
     31,3,21,0,27,33,26,4,35,18,9,34]

For this permutation, \(C(p)=1\). Among the other rotations, the cycle count is two at shifts \(7\) and \(23\), three at each nonzero even shift, and four at the remaining odd shifts. Thus

Since \(x(36)\) is the maximum over configurations, this example gives \(x(36)\ge32\). The \(n=40\) and \(n=42\) examples are similar; their permutations and cycle decompositions are in the files below.

5. What Lean actually checks

I ran the supplied certificate file using Lean 4.19.0. It compiles, and all fifteen printed theorem checks report no axiom dependencies. The proofs use decide +kernel, without sorry or native_decide. The separate Python verifier also passed. That checks the finite data, but it is important to be precise about what the Lean file does and does not prove.

For each of the three sizes, the Lean file checks:

1. The witness has exactly \(n\) entries and uses each label once.
2. For every shift \(k\), the listed nonempty cycles cover the entire set of labels, with no repetitions, and each arrow is correct for the rotated permutation.
3. The full vector of cycle counts agrees with the claimed profile.
4. Some shift actually has four cycles.
5. The minimum certified swap cost is \(32\), \(36\), or \(38\), respectively.

Lean checks the particular permutations and the cycle decompositions listed for them. It does not formalize the general identity between transposition length and cycle count, the circular-distance interpretation, or the published upper bound. Those steps are explained mathematically in the README. So this is a verified set of finite certificates, not an end-to-end Lean formalization of the circular-sorting problem.

6. Search and cross-checks

Astra generated C++ code for a stochastic search over permutations, using swaps and three-cycle mutations. The search logs are included. Because the search is randomized, another run may find something different; the proof does not depend on reproducing the search itself.

The permutations are recorded explicitly. A short, standard-library Python script separately reconstructs the cycles for all \(36+40+42=118\) rotations and obtains the same cycle counts. The distances then follow from the usual transposition formula.

The general upper bound \(x(n)\le n-3\) for even \(n\ge4\) follows from a parity argument already discussed in [2]: consecutive rotations have opposite permutation parity when \(n\) is even, ruling out the special cycle structure required to attain distance \(n-2\). Combining this known upper bound with the explicit lower-bound examples gives the intervals above.

7. Files and reproduction

All files are plain text and can be inspected directly. To repeat the formal checks, install Lean 4.19.0, then run lean CircularSorting.lean; run python3 verify.py for the independent cycle traversal.

• CircularSorting.lean — Lean theorems and all explicit cycle certificates.
• witnesses.json — permutations, cycle counts and decompositions.
• verify.py — independent standard-library Python checker.
• README.md — complete mathematical proof, novelty scope, and reproducibility notes.
• Lean check log and Python check log — outputs supplied with the certificates.
• search.cpp — heuristic search code, with 36, 40 and 42 search logs.
• Browse the complete certificate directory on GitHub.

8. A note on novelty

As far as I can tell, these examples tighten three lower bounds stated in Table 1 of [2]. I have not done a comprehensive literature search, and I do not know whether the same permutations, their cycle profiles, or stronger bounds have already been found elsewhere. That is a question for people who know this subject better than I do.

I thought it was worth putting the examples and the checking code online. If there is a mistake, an overlooked reference, or a simpler construction, I would be grateful to hear about it.