Problem. 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).
\]
The mathematical status has not passed editorial review.
1Packet records
5 records
Record
Kind
Assessment
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.
Cycle-index enumeration gives
\[
Q(x)=\prod_{k\geq1}\left(1+\frac{x^k}{k}\right).
\]
Define
\[
B_m=\sum_{d\mid m}\frac{(-1)^{m/d-1}}{d^{m/d-1}}.
\]
Expanding the logarithmic derivative factor by factor gives
\[
\frac{xQ'(x)}{Q(x)}=\sum_{m\geq1}B_mx^m.
\]
Coefficient comparison therefore yields the exact recurrence
\[
q_0=1,\qquad nq_n=\sum_{m=1}^nB_mq_{n-m}\quad(n\geq1).
\]
After multiplication by \(n!\), these are the integer permutation counts in OEIS A007838.
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.
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.
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`.
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Does the distinct-cycle-length probability decrease after n=30?.” TheoremDB. P100020. Problem statement; statement text SHA-256 59aca6194890fbaf4f08ea1313d08e17b1da8b0474a4b68f8c7da18eb469e672. https://theoremdb.org/statement/?ref=P100020
BibTeX
@misc{theoremdb-problem-59aca6194890fbaf4f08ea1313d08e17b1da8b0474a4b68f8c7da18eb469e672,
title = {{Does the distinct-cycle-length probability decrease after n=30?}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 59aca6194890fbaf4f08ea1313d08e17b1da8b0474a4b68f8c7da18eb469e672},
url = {https://theoremdb.org/statement/?ref=P100020}
}
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
Reference review is pending for 1 entry. Each affected row names the fields still awaiting review.
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/0606370 (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.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.Also cited at Proposition 1 and the distinct-cycle-length example.
D. Lehmer, “On reciprocally weighted partitions”. Acta Arithmetica 21 (1972), 379-388. DOI 10.4064/aa-21-1-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 · checked 2026-08-01Source use: citation only.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.Also cited at Acta Arithmetica 21 (1972), 379-388.
Packet source. Generating function and recurrence; D. H. Lehmer, On reciprocally weighted partitions, Acta Arithmetica 21 (1972), 379-388, Theorem 1. Generating function and recurrence; D. H. Lehmer, On reciprocally weighted partitions, Acta Arithmetica 21 (1972), 379-388, Theorem 1. ↗reference database · reference source · checked 2026-07-24Source use: citation only.For Eventual decrease for distinct cycle lengths in random permutations: The logarithmic derivative of the classical product computes every q_n from earlier coefficients.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.
Counting permutations and polynomials with a restricted factorization pattern. Section 2, the k=1 distinct-cycle-length case. ↗website · reference source · checked 2026-07-24Reference review pending: relevance note.Source use: citation only.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.