Unique solution to system of nonlinear equations (non-singular Jacobian) Suppose I have a system of $n$ nonlinear, $C^\infty$, real implicit functions with $n$ real variables: $\{f_i(x_1,...x_n)\}_{i=1}^n$. To provide more structure, we have
$f_1(x_1,...x_n)= x_1 + g(x_2,...,x_n)$, ... $f_n(x_1,...x_n)= x_n + g(x_1,...,x_{n-1})$, etc. In other words, in each $f_i$, the variable $x_i$ is additively separable.
None of the equations are redundant. When can I assert that there exists at most one solution $(x_1^*,...x_n^*)$ to the system? Following the theory of system of linear equations, is it sufficient that the Jacobian matrix of the system is non-singular everywhere?
The idea is from implicit function theorem. If there are $m+n$ nonlinear equations with $n$ endogenous variables and $m$ exogenous variables, and the Jacobian matrix is nonsingular at a point, then we can express the $n$ endogenous variables as functions of the $m$ exogenous variables near that point. If nonsingular everywhere, then we can do the same everywhere. The question now is what if $m=0$.
 A: It's cleaner to rewrite the question as asking about a single smooth function $F : \mathbb{R}^n \to \mathbb{R}^n$. If the Jacobian is everywhere nonsingular, then by the inverse function theorem, $F$ is a local diffeomorphism: that is, $F$ locally has an inverse everywhere. It does not necessarily follow that $F$ has a global inverse, because there is no guarantee that we can consistently glue all these local inverses together.
For example, if we replace $\mathbb{R}^n$ by a more general manifold $M$, it can be the case that $M$ admits a nontrivial covering map to itself, the simplest example being $M = S^1$. Now this can't happen for $\mathbb{R}^n$, but more subtle things might happen. 
If $F$ is assumed in addition to be surjective and proper, then by Ehresmann's theorem it's a fibration. Its fibers must be connected, and in fact must be contractible, in addition to being zero-dimensional, so the conclusion is that they are points. 
Without properness, it appears that counterexamples are known:

The strong real Jacobian conjecture was that a real polynomial map with a nowhere vanishing Jacobian determinant has a smooth global inverse. That is equivalent to asking whether such a map is topologically a proper map, in which case it is a covering map of a simply connected manifold, hence invertible. Sergey Pinchuk (1994) constructed two variable counterexamples of total degree 25 and higher.

