Unary in $P$, binary not in $P$ I would like to know if there is a known decision problem with the following characteristics:


Represented in unary, the problem is decidable in polynomial time.
Represented in binary, the problem is not decidable in polynomial time (and this fact has been proved, not just conjectured).


For example, Subset-Sum is in $P$ when represented in unary, but it is $NP$-complete in binary. However, this problem does not satisfy my second requirement because we do not know whether $P=NP$.
Every single-exponential (i.e. known to be solvable in $O(c^n)$ for some constant $c$) EXPTIME-complete problem will answer your requirements.

For example, see checking thorough rerefinement on finite modal transition systems.