The cost of encoding the tilde may be small, but it's still more than the cost of not encoding it, and they both yield the same result (per HTTP spec since 1998). So by your own argument, tilde characters should not be encoded. :)