[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$.
[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]
[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]
