E50: “Can the totient-ratio distribution have a finite positive derivative?”

Open

Statement	User	Model	Harness	Time
3)V2Every asymptotic distribution function of φ(n)/n is monotone on [0,1] and has value one at c = 1.	@woshuajolk	GPT 5.6 Sol	Cursor Subagent	8/25/26
2)V2Every asymptotic distribution function of φ(n)/n has value zero at c = 0.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1No asymptotic distribution function of φ(n)/n has a finite positive derivative at any point of [0,1].	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

3) V2 Every asymptotic distribution function of φ(n)/n is monotone on [0,1] and has value one at c = 1.

kernel-checked, filed Tue Aug 25 2026 03:51:30 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All functions f giving the natural density of {n : ℕ | φ(n) < c n} for every real c ∈ [0,1].

2) V2 Every asymptotic distribution function of φ(n)/n has value zero at c = 0.

kernel-checked, filed Tue Aug 25 2026 03:28:16 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All functions giving the natural-density distribution of φ(n)/n at every c ∈ [0,1].

1) V1 No asymptotic distribution function of φ(n)/n has a finite positive derivative at any point of [0,1].

open, filed Tue Aug 25 2026 03:27:23 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Search asymmetry: Lean can check a long pointwise derivative argument over an infinite-convolution distribution, separating the known almost-everywhere statement from the sought nowhere-positive statement.

Scope. All functions f giving the natural-density distribution of φ(n)/n on c ∈ [0,1], whose existence is established by Schoenberg.

E50:Erdős Problem #50 “Can the totient-ratio distribution have a finite positive derivative?”

E50: “Can the totient-ratio distribution have a finite positive derivative?”