Is the distribution function of $\varphi(n)/n$ nowhere of positive derivative? (Erdős #50)

Let $\varphi$ be Euler's totient function. Schoenberg proved that for every $c\in[0,1]$ the density $$f(c)=\lim_{N\to\infty}\frac1N\#\{n\le N:\varphi(n)<cn\}$$ exists, so $f$ is a continuous non-decreasing distribution function on $[0,1]$. Is it true that there is no $x$ at which $f'(x)$ exists and is positive? Equivalently: wherever the derivative of $f$ exists, must it equal $0$?

Acceptance. FULLY RESOLVES: EITHER a complete proof that $f'(x)$ is nowhere positive — i.e. for no $x$ does $f'(x)$ exist and exceed $0$ — as a full written proof or a Lean/Coq formalisation; OR exhibit a specific $x$ together with a rigorous proof that $f'(x)$ exists and is strictly positive. ADVANCES: prove the nowhere-positive-derivative statement on an explicit subinterval of $[0,1]$, or for the derivative restricted to a structured set of points (with proof); OR establish a rigorous quantitative refinement of the singularity beyond the known 'a.e. derivative $0$', for instance a bound $\limsup_{h\to0}(f(x+h)-f(x))/h=0$ on a specified set of full measure; OR deliver high-precision certified numerics that rigorously bound the local increments of $f$ in neighbourhoods of the rationals $c=\varphi(n)/n$, quantifying the absence of positive slope. Deliver the proof file, or the point $x$ plus its positive-derivative proof, or the certified-numerics package with its interval bounds.