Right, the difference is to some degree syntactic, but then, so is most programming ("it's just math").
The most significant difference, as it appears to me (note that I've done only a bit of research into refined types, and practically none into dependent types), is that dependent types means building top-down whereas refined types means building bottom-up.
Dependent types: everything is proved, by hand, by the user, who has to build up the whole program from basic blocks. Usually the "foundation" is taken to be some kind of type theory, either Martin-Löf Type Theory or more recently Homotopy Type Theory, which has some complexities (e.g. multiple types of equality) and limitations (e.g. languages cannot be Turing complete) that I don't really understand. "Pi types" abound. I'm not sure how much of this description really is fundamental about Type Theory, and how much is just due to the specifics of the implementations I've seen (Coq, Agda, Idris).
Refined types: start with a program and add some assertions about the values (and possibly functions, but this can then get more complicated) in the program. The idea is that many of these can ideally be proven by automated SMT solvers, which support some "theories" (e.g. natural numbers, real numbers, bitfields (i.e. machine integers and floating point numbers), algebraic datatypes) and can prove some statements in these theories. As you mentioned, "linear arithmetics", along with "real number algebra", are complete and decidable theories, so in theory you should be able to prove anything about them, but I'm guessing that in practice you'd still want some timeout parameter on your SMT solver (like in type systems, where there are exponential edge cases, that thankfully don't arise often in practice), but they aren't very useful, so hopefully you can prove more than that, using the heuristics embedded into SMT solvers (e.g. you should be able to prove many non-linear properties of two-dimensional loops by lifting integers into reals). If the solver is unable to solve something, the programmer can still add hints (but this quickly gets complicated).
A concrete difference would be, in dependently-typed language, you define a list type as
type List a n =
| Nil : List 'a 0
| Const : a -> List a n -> List a (n + 1)
in a language with refined types, you can add
length afterwards:
type List a = <... whatever ...>
property length : List a -> Nat
And then the type checker/SMT solver will treat `length` as an
uninterpreted function that always maps the same array to the same integer, and use it to prove things.
Not sure if this makes a lot of sense, I haven't looked into this in a while and am also not aware of the most recent research in these fields. Hopefully someone can explain better!