The brute force part about our proof.

Refer to the paper for a proof. This page is to illustrate how 'brute' the force is in my proof!

Consider a transformation y=x²z, which maps the set D to a strip in the first quadrant, and for (X,Y)=grad W, put G(x,z) = X(x,x²z)/x and F(x,z) = z X²(x,x²z)/Y(x,x²z). Obviously, fixed points of grad W in D and the solutions of F(x,z)=G(x,z)=1 in D'={(x,z) = x>0, 0<= z <= 1} are in 1 to 1 correspondence.

Let J_GF= G_x F_z - F_x G_z be the Jacobian of the map (x,z) to (G(x,z),F(x,z)). The inverse function theorem implies that if J_GF is not 0 (i.e., does not change signs) then at least locally the map is 1 to 1 (hence in particular, fixed point is unique in a small neighborhood). Conditions in the Theorem implies certain global properties with which the uniqueness of the fixed point follows in D.

We need a proof of J_GF>0. With a little thought one sees that it is sufficient to prove J_GF>0 on F=1 instead of whole D'.

Put Rem₀=e(x,z) =(1-z)x² Y²/X²(x,x²z) (J_GF-F(1-F)/(z(1-z)) G_x)(x,z). (Rem₀ is the name in Mathematica; in the paper it is e(x,z). Each software suggests its own 'simple names' ...) If we prove that this is a polynomial in x, z, and 1-z with positive coefficients, then the proof is complete. We want to find a polynomial in 3 variables with positive coefficients f(x,z,s) such that Rem₀=e(x,z)=f(x,z,1-z).

By trial and error I found e_c(x,z,s) = ct[x,z,s] (r.h.s. is for Mathematica) and e_r(x,z,s) = res = Sum_n=9³⁰ resC[n,z,s] xⁿ such that f(x,z,s)=e_c(x,z,s)+e_r(x,z,s) has the desired property; nameley,
Rem₀=ct[x,z,1-z] + res /. s->1-z
is proved by Mathematica. The figures below shows ct[x,z,s], res, and the formula.

Note that Mathematica does not help me much. I had to find out and type in ALL the terms in ct[x,z,s] by hand! The rather lengthy lines in ct is not a computer-calculated output. A formula F(1-F)/(z(1-z)) G_x(x,z) is also my invention.

Mathematica just subtracts them from Rem₀ to return res as a function of x and z, and I had to sort out some terms so that all the coefficients are positive. So all the terms in res with the variable s is by my hand again. The existing proof is obtained by such lengthy trial and error and by brute force. Lack of either mathematical or physical intuitions prevents its generalization. The worst part about it is that it is non-trivial to generalize our results directly to higher dimensions.

A nice proof is wanted!

Completion of a proof.

'Counter term' e_c(x,z,s) = ct[x,z,s] contains no negative signs!

'Residue' e_r(x,z,s) = res = Sum_n=9³⁰ resC[n,z,s] xⁿ contains no negative signs!