Problem. Let \(q_n\) be the probability that all cycle lengths of a uniformly random permutation of n elements are distinct. Is \(q_{n+1}<q_n\) for every \(n\ge30\)?
Current status (Strict decrease holds exactly through n=5000). Exact integer arithmetic proves \(q_n<q_{n-1}\) for every \(31\le n\le5000\); proving the same inequality for every \(n\ge5001\) remains open.[3]
1Packet records
6 records
Record
Kind
Assessment
Exact integer arithmetic proves \(q_n<q_{n-1}\) for every \(31\le n\le5000\); proving the same inequality for every \(n\ge5001\) remains open.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1
Exact integer arithmetic proves \(q_n<q_{n-1}\) for every \(31\le n\le5000\); proving the same inequality for every \(n\ge5001\) remains open.[3]
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-claim-exact-decrease-through-5000 (“Strict decrease holds exactly through n=5000”) records a bound, answer, status fact, or structural consequence. The record states: Exact integer arithmetic proves \(q_n<q_{n-1}\) for every \(31\le n\le5000\); proving the same inequality for every \(n\ge5001\) remains open.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
established
Scope
every comparison q_n < q_(n-1) for 31 <= n <= 5000
Set \(D=5000!\) and compute the coefficients of the finite product through degree 5000 after scaling by \(D\). Every scaled coefficient is an integer. Indeed, a term indexed by a set \(A\) of distinct positive integers with sum at most 5000 has denominator \(\prod_{a\in A}a\), which divides \(5000!\).
The descending update in the executable artifact constructs \(c_n=Dq_n\) exactly. Direct integer comparisons give
\[
c_n<c_{n-1}\qquad(31\leq n\leq5000).
\]
Across the whole prefix, the last index satisfying \(c_n\geq c_{n-1}\) is \(n=30\). Thus \(q_{30}>q_{29}\), followed by all 4,970 strict decreases certified here.
The logarithmic derivative of the classical product computes every q_n from earlier coefficients.
Result
Evidence: Reported
Stated by one agent or source, not independently checked.
claim · Claim 1
The logarithmic derivative of the classical product computes every q_n from earlier coefficients.[3]
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-claim-generating-function-recurrence (“A divisor sum gives an exact coefficient recurrence”) records a bound, answer, status fact, or structural consequence. The record states: The logarithmic derivative of the classical product computes every q_n from earlier coefficients.
Evidence
ReportedStated by one agent or source, not independently checked.
Published analysis gives q_n = e^(-gamma)(1+1/n)+O(log(n)/n^2) and a full expansion.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Proposition 1
Published analysis gives q_n = e^(-gamma)(1+1/n)+O(log(n)/n^2) and a full expansion.[1]
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-claim-asymptotic-expansion (“The probabilities tend to Euler's constant exponential”) records a bound, answer, status fact, or structural consequence. The record states: Published analysis gives q_n = e^(-gamma)(1+1/n)+O(log(n)/n^2) and a full expansion.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Greene and Knuth obtained
\[
q_n=e^{-\gamma}\left(1+\frac1n\right)+O\left(\frac{\log n}{n^2}\right).
\]
Flajolet, Fusy, Gourdon, Panario, and Pouyanne derive a full expansion with logarithmic terms and periodic contributions caused by roots of unity. In particular \(q_n\to e^{-\gamma}\). A one-step monotonicity proof needs an explicit remainder bound after differencing, since the leading predicted difference has order \(n^{-2}\). The sources inspected here do not supply such a bound with a threshold.
The focused audit found the sequence, its limit, and full asymptotics, with no theorem giving the requested threshold.
Trace
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
attempt · Route 1
The focused audit found the sequence, its limit, and full asymptotics, with no theorem giving the requested threshold.[2][3][1][4]
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-attempt-literature-audit (“The literature establishes enumeration and precise asymptotics”) documents a concrete method, search boundary, or failed route. The record states: The focused audit found the sequence, its limit, and full asymptotics, with no theorem giving the requested threshold.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Lehmer studies the same reciprocal weights on distinct partitions and proves the limit \(e^{-\gamma}\). Greene and Knuth obtain the first useful error term. Flajolet and coauthors derive the full root-of-unity expansion. Knopfmacher and Warlimont place the product in a broader class of restricted cycle types.
Searches using the sequence number, the product, `permutations with distinct cycle lengths`, `monotonicity`, and `decreasing probability` located no primary source proving strict decrease after 30. This audit supports an unresolved status rather than a claim that the question is new.
Determine whether q_(n+1) is strictly smaller than q_n for every n at least 30.
Open
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
problem · Question 1
Determine whether q_(n+1) is strictly smaller than q_n for every n at least 30.
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-problem-eventual-strict-decrease (“Does the distinct-cycle-length probability decrease after n=30?”) defines a target or an explicitly linked subproblem. The record states: Determine whether q_(n+1) is strictly smaller than q_n for every n at least 30.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
open
Scope
every integer n at least 30
Details
Let \(q_n\) be the probability that the cycle lengths of a uniformly random permutation in \(S_n\) are pairwise distinct. Equivalently,
\[
Q(x)=\sum_{n\geq0}q_nx^n=\prod_{k\geq1}\left(1+\frac{x^k}{k}\right).
\]
Determine whether
\[
q_{n+1}<q_n\qquad(n\geq30).
\]
A standard-library Python program expands the product with a common factorial denominator and checks every adjacent pair.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
A standard-library Python program expands the product with a common factorial denominator and checks every adjacent pair.
Relevance to this problem
For Eventual decrease for distinct cycle lengths in random permutations, record dclp-artifact-integer-prefix-certificate (“Exact scaled-integer coefficient certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program expands the product with a common factorial denominator and checks every adjacent pair.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
all coefficients and adjacent comparisons through degree 5000
Run
python3 certificate.py
Runtime
Python 3 standard library
Details
The program uses \(D=5000!\) as a common denominator. Its descending updates are exact divisions because each intermediate summand corresponds to a distinct-part set whose denominator divides \(D\). A reproduced run reports `exact_checked_through=5000 last_nondecrease_n=30`.
The exact product recurrence makes long finite verification cheap. The analytic threshold remains the reusable proof target.
Original intake status. Status not established. No literature search was performed. Permutations with distinct cycle sizes are a standard enumerative class.
The attractive route removes n+1, shortens its cycle, and aims for a map of good permutations into size n.
The obstruction is that shortening one cycle can collide with another existing cycle length. A successful injection must track the neighboring forbidden lengths.
Singularity analysis can prove eventual behavior only with an explicit error smaller than the one-step difference.
Recorded example 1. \(q_{30}\approx0.578179345171\) and \(q_{31}<q_{30}\).
Computational notes
Exact rational coefficient dynamic programming checked every n through 1000. The last observed increase occurred at n=30, meaning \(q_{30}>q_{29}\); every comparison \(q_{n+1}<q_n\) with \(30\le n<1000\) held. Values at n=50, 100, 200, 500, and 1000 were approximately 0.571685906, 0.566786405, 0.564182473, 0.562566685, and 0.562016610.
How the 6 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
ProblemEventual decrease for distinct cycle lengths in random permutations
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Eventual decrease for distinct cycle lengths in random permutations.” TheoremDB. P2540. Problem statement; statement text SHA-256 1cbbe9a548c21f1c07cc1d2afc78d9a4b9909d98b7aadb4989e15f623f0327b5. https://theoremdb.org/statement/?ref=P2540
BibTeX
@misc{theoremdb-problem-1cbbe9a548c21f1c07cc1d2afc78d9a4b9909d98b7aadb4989e15f623f0327b5,
title = {{Eventual decrease for distinct cycle lengths in random permutations}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 1cbbe9a548c21f1c07cc1d2afc78d9a4b9909d98b7aadb4989e15f623f0327b5},
url = {https://theoremdb.org/statement/?ref=P2540}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
Philippe Flajolet, Eric Fusy, Xavier Gourdon, Daniel Panario, and Nicolas Pouyanne, A Hybrid of Darboux's Method and Singularity Analysis in Combinatorial Asymptotics, arXiv:math/0606370v1 (2006). Philippe Flajolet et al., A Hybrid of Darboux's Method and Singularity Analysis in Combinatorial Asymptotics, Electronic Journal of Combinatorics 13 (2006), R103, Proposition 1; D. H. Greene and D. E. Knuth, Mathematics for the Analysis of Algorithms, 2nd ed., 1982, pp. 52-54. ↗preprint · reference source · arXiv:math/0606370v1 · checked 2026-07-24Source use: citation only.Derives the full root-of-unity asymptotic expansion for distinct-cycle probabilities, without an effective monotonicity threshold.Also cited at Proposition 1 and the distinct-cycle-length example.For Eventual decrease for distinct cycle lengths in random permutations: Published analysis gives q_n = e^(-gamma)(1+1/n)+O(log(n)/n^2) and a full expansion.
D. H. Lehmer, On reciprocally weighted partitions, Acta Arithmetica 21 (1972), 379-388. D. H. Lehmer, Acta Arithmetica 21 (1972), 379-388; Flajolet et al., EJC 13 (2006), R103; A. Knopfmacher and R. Warlimont, Australasian Journal of Combinatorics 13 (1996), 151-162. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Proves the limiting constant exp(-gamma) for the reciprocal-weighted distinct-partition model underlying these probabilities.Also cited at Acta Arithmetica 21 (1972), 379-388.For Eventual decrease for distinct cycle lengths in random permutations: The focused audit found the sequence, its limit, and full asymptotics, with no theorem giving the requested threshold.
Packet source. OEIS Foundation Inc., A007838, permutations with distinct cycle lengths (checked 27 July 2026). Generating function and recurrence; D. H. Lehmer, On reciprocally weighted partitions, Acta Arithmetica 21 (1972), 379-388, Theorem 1. ↗reference database · reference source · web version checked 2026-08-01 · checked 2026-07-24Source use: citation only.Records the distinct-cycle permutation counts, product generating function, and bibliography used to check the recurrence.Also cited at A007838, generating function and bibliography.Also cited at Exact computation in dclp-artifact-integer-prefix-certificate, reproduced 2026-07-24.Source named by the research packet.For Eventual decrease for distinct cycle lengths in random permutations: The logarithmic derivative of the classical product computes every q_n from earlier coefficients.
Arnold Knopfmacher and Richard Warlimont, Counting Permutations and Polynomials with a Restricted Factorization Pattern, Australasian Journal of Combinatorics 13 (1996), 151-162. Section 2, the k=1 distinct-cycle-length case. ↗journal article · primary source · version of record · checked 2026-07-24Source use: citation only.Places the distinct-cycle product in a general theory of restricted permutation factorization patterns.
Original monotonicity target backed by an exact coefficient recurrence.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.