[proofplan] The Sharafutdinov retraction is obtained as the endpoint map of the Sharafutdinov flow associated to the standard totally convex exhaustion of a complete open manifold with nonnegative sectional curvature. The essential input is Perelman's distance monotonicity theorem for this flow: every finite-time projection between levels of the exhaustion is distance nonincreasing. We apply this estimate to a sequence of finite-time projections converging pointwise to the endpoint retraction onto the soul, then pass to the limit in the metric inequality. [/proofplan]

[step:Invoke the finite-level distance estimate for the Sharafutdinov flow]Let $d_g: M \times M \to [0,\infty)$ denote the Riemannian distance induced by $g$. Because $(M,g)$ is complete, open, and satisfies $\operatorname{sec} \ge 0$, the [Soul Theorem](/page/Soul%20Theorem) gives a compact totally geodesic soul $S \subset M$. Choose the standard Sharafutdinov convex exhaustion associated to $S$. Concretely, let $h: M \to [b_\infty,\infty)$ denote the exhaustion function used in the [Sharafutdinov retraction](/page/Sharafutdinov%20Retraction), where $b_\infty \in \mathbb{R}$ is its minimal value, define \begin{align*} C_t := h^{-1}([b_\infty,t]) \subset M \end{align*} for every $t \ge b_\infty$, and note that \begin{align*} S = h^{-1}(\{b_\infty\}) = \bigcap_{t>b_\infty} C_t. \end{align*} A regular level means a value $t>b_\infty$ for which the corresponding finite-time Sharafutdinov flow projection is defined on $C_t$ and maps to lower exhaustion levels. For regular levels $a>b>b_\infty$, let \begin{align*} P_{a,b}: C_a \to C_b \end{align*} denote the finite-time Sharafutdinov flow projection from level $a$ to level $b$. We use [Perelman's distance monotonicity theorem for the Sharafutdinov flow](/page/Sharafutdinov%20Retraction): if $C_a$ and $C_b$ are compact totally convex members of the Sharafutdinov exhaustion of a complete open Riemannian manifold with nonnegative sectional curvature, and $P_{a,b}:C_a\to C_b$ is the corresponding finite-time Sharafutdinov projection, then $P_{a,b}$ is distance nonincreasing. Its hypotheses are satisfied here: completeness, openness, and $\operatorname{sec}\ge0$ are assumptions of the theorem; the sets $C_t$ are the compact totally convex sets in the standard Sharafutdinov exhaustion; and $P_{a,b}$ is exactly the finite-time projection associated to that exhaustion. Therefore \begin{align*} d_g(P_{a,b}(u),P_{a,b}(v)) \le d_g(u,v) \end{align*} for all $u,v \in C_a$.[/step]

[guided]The point of the proof is not to reconstruct the Sharafutdinov flow from scratch, but to use the precise finite-stage property that implies the theorem. Let $d_g: M \times M \to [0,\infty)$ be the distance function of the Riemannian metric $g$. Since $(M,g)$ is complete, open, and has $\operatorname{sec} \ge 0$, the [Soul Theorem](/page/Soul%20Theorem) supplies a compact totally geodesic soul $S \subset M$. We now name the objects in the Sharafutdinov construction. Let $h: M \to [b_\infty,\infty)$ be the standard convex exhaustion function whose minimal level is the soul. For every $t \ge b_\infty$, define \begin{align*} C_t := h^{-1}([b_\infty,t]) \subset M. \end{align*} These sets are compact and totally convex, they exhaust $M$, and their intersection over $t>b_\infty$ is \begin{align*} \bigcap_{t>b_\infty} C_t = h^{-1}(\{b_\infty\}) = S. \end{align*} A regular level is a value $t>b_\infty$ for which the finite-time Sharafutdinov flow projection between level sets is defined. Thus, for regular levels $a>b>b_\infty$, the projection is the map \begin{align*} P_{a,b}: C_a \to C_b. \end{align*} The needed finite-stage theorem is [Perelman's distance monotonicity theorem for the Sharafutdinov flow](/page/Sharafutdinov%20Retraction). It applies to compact totally convex levels of the Sharafutdinov exhaustion in a complete open manifold with nonnegative sectional curvature and asserts that the finite-time projection $P_{a,b}$ is $1$-Lipschitz. We verify the hypotheses in this setting: the manifold is complete and open by assumption, the curvature bound $\operatorname{sec}\ge0$ is a hypothesis of the theorem statement, the sets $C_a$ and $C_b$ are members of the standard compact totally convex exhaustion, and $P_{a,b}$ is the associated finite-time Sharafutdinov projection. Therefore \begin{align*} d_g(P_{a,b}(u),P_{a,b}(v)) \le d_g(u,v) \end{align*} for all $u,v \in C_a$. This is the mechanism that will survive in the endpoint limit and become the distance nonincreasing property of $p$.[/guided]

[step:Approximate the endpoint retraction by finite-level projections] Fix arbitrary points $x,y \in M$. Since the family $(C_t)_{t>b_\infty}$ exhausts $M$, choose a regular exhaustion level $a>b_\infty$ with $x,y \in C_a$. Let $(b_k)_{k=1}^{\infty}$ be a decreasing sequence of regular levels in $(b_\infty,a)$ with $b_k \downarrow b_\infty$. The phrase $b_k \downarrow b_\infty$ means that $b_{k+1}\le b_k$ for every $k\in\mathbb{N}$ and $\lim_{k\to\infty} b_k=b_\infty$; the limiting level set is \begin{align*} h^{-1}(\{b_\infty\}) = S. \end{align*} For each $k \in \mathbb{N}$, define \begin{align*} x_k &= P_{a,b_k}(x), & y_k &= P_{a,b_k}(y). \end{align*} The endpoint Sharafutdinov retraction is the pointwise limit of these finite-level projections as the lower level decreases to the minimal level. Hence the sequences $(x_k)_{k=1}^{\infty}$ and $(y_k)_{k=1}^{\infty}$ converge in $M$ to $p(x)$ and $p(y)$, respectively: \begin{align*} \lim_{k\to\infty} x_k &= p(x), & \lim_{k\to\infty} y_k &= p(y). \end{align*} [/step]

[step:Pass the finite-level metric inequality to the limiting retraction] For every $k \in \mathbb{N}$, the finite-level distance estimate applied to $u=x$ and $v=y$ gives \begin{align*} d_g(x_k,y_k) = d_g(P_{a,b_k}(x),P_{a,b_k}(y)) \le d_g(x,y). \end{align*} The distance function $d_g: M \times M \to [0,\infty)$ is continuous with respect to the manifold topology induced by the complete Riemannian metric. Passing to the limit along $x_k \to p(x)$ and $y_k \to p(y)$ gives \begin{align*} d_g(p(x),p(y)) &= \lim_{k\to\infty} d_g(x_k,y_k) \\ &\le d_g(x,y). \end{align*} Since $x,y \in M$ were arbitrary, the associated Sharafutdinov retraction $p:M\to S$ is distance nonincreasing on all of $M$. [/step]