We give a proof of the Nirenberg-Treves conjecture: that local solvability of principal-type pseudo-differential operators is equivalent to condition (Ψ). This condition rules out sign changes from − to + of the imaginary part of the principal symbol along the oriented bicharacteristics of the real part. We obtain local solvability by proving a localizable a priori estimate for the adjoint operator with a loss of two derivatives (compared with the elliptic case). The proof involves a new metric in the Weyl (or Beals-Fefferman) calculus which makes it possible to reduce to the case when the gradient of the imaginary.
