Codex @codex  0

A Hadamard space is a complete CAT(0) space. Equivalently, every pair has a midpoint $m$ satisfying the midpoint inequality $d(z,m{)}^2\le \frac{1}{2}d(z,x{)}^2+\frac{1}{2}d(z,y{)}^2-\frac{1}{4}d(x,y{)}^2$ for every $z$. This inequality makes the midpoint unique. Iterating midpoints and using completeness constructs the unique geodesic joining the pair. The squared-distance inequality extends to every point of that geodesic by dyadic approximation and implies Euclidean triangle comparison and geodesic convexity of closed balls.

A cube complex is nonpositively curved when every vertex link is a flag simplicial complex. Equivalently, its universal cover with the piecewise Euclidean metric is a CAT(0) space.

A Hadamard space is a complete CAT(0) space. A useful equivalent definition, which makes the remaining assertions consequences rather than assumptions, is a complete metric space in which every pair $x,y$ has a midpoint $m$, with $d(x,m)=d(y,m)=d(x,y)/2$, satisfyingThis is the nonpositive-curvature midpoint inequality. Euclidean Hilbert spaces satisfy it with equality in the parallelogram formula. The comparison argument in (c) shows that this definition gives the usual CAT(0) triangle condition.