[proofplan]
We argue by contradiction from an arbitrary proper coloring with $m$ colors. The coloring induces an equivariant map between the standard box complexes associated to the graph and to the complete graph on the color set. The source has the same homotopy type as the neighborhood complex, while the target has the equivariant homotopy type of an antipodal sphere of dimension $m-2$. The index form of the [Borsuk-Ulam theorem](/theorems/6462) then forces $r \le m-2$, so every proper coloring uses at least $r+2$ colors.
[/proofplan]
[step:Turn a proper coloring into an equivariant map of Hom complexes]
Let $m \in \mathbb{N}$, and suppose that $G$ has a proper $m$-coloring. Let $K_m$ denote the complete graph on the vertex set $\{1,\dots,m\}$. The coloring is equivalently a graph homomorphism, meaning a vertex map $\varphi: G \to K_m$ preserving adjacency.
For a finite simple graph $H$, define $\mathcal{P}_H$ to be the poset whose elements are ordered pairs $(A,B)$ of nonempty subsets $A,B \subseteq V(H)$ such that every vertex of $A$ is adjacent in $H$ to every vertex of $B$, ordered by coordinatewise inclusion. Let $\operatorname{Hom}(K_2,H)$ denote the Hom complex given by the order complex of $\mathcal{P}_H$, so its vertices are elements of $\mathcal{P}_H$ and its simplices are finite chains in $\mathcal{P}_H$.
The group $\mathbb{Z}/2$ acts on $\mathcal{P}_H$ by the order-preserving involution $\tau_H: \mathcal{P}_H \to \mathcal{P}_H$ defined by $\tau_H(A,B)=(B,A)$. This induces a simplicial involution, still denoted $\tau_H$, on $\operatorname{Hom}(K_2,H)$. Because $H$ has no loops, no poset element satisfies $(A,B)=(B,A)$: if $A=B$, then any $a \in A$ would be adjacent to itself. Hence $\tau_H$ has no fixed vertex. Since $\tau_H$ sends every poset element to an incomparable distinct element, it sends every chain disjointly from itself; therefore the induced action on the geometric realization of $\operatorname{Hom}(K_2,H)$ is free.
The graph homomorphism $\varphi$ induces an order-preserving map of Hom posets, and hence a simplicial map on order complexes, $\operatorname{Hom}(K_2,\varphi): \operatorname{Hom}(K_2,G) \to \operatorname{Hom}(K_2,K_m)$, defined on poset elements by $\operatorname{Hom}(K_2,\varphi)(A,B)=(\varphi(A),\varphi(B))$. Indeed, if every vertex of $A$ is adjacent to every vertex of $B$ in $G$, then every vertex of $\varphi(A)$ is adjacent to every vertex of $\varphi(B)$ in $K_m$, since $\varphi$ preserves adjacency; coordinatewise inclusion is also preserved under image. Moreover, for every $(A,B) \in \mathcal{P}_G$, applying $\operatorname{Hom}(K_2,\varphi)$ after swapping the two coordinates gives the same ordered pair as swapping the two coordinates after applying $\operatorname{Hom}(K_2,\varphi)$. Thus $\operatorname{Hom}(K_2,\varphi)$ is a $\mathbb{Z}/2$-equivariant map of free $\mathbb{Z}/2$-complexes.
[/step]
[step:Replace the source by the neighborhood complex]
Let $\mathcal{F}(N(G))$ denote the face poset of the neighborhood complex $N(G)$, whose elements are the nonempty simplices of $N(G)$ ordered by inclusion. Define the order-preserving map $\pi_G: \mathcal{P}_G \to \mathcal{F}(N(G))$ by $\pi_G(A,B)=A$. This map is well-defined: if $(A,B) \in \mathcal{P}_G$, then every vertex of the nonempty set $B$ is a common neighbor of $A$, so $A$ is a simplex of $N(G)$. Passing to order complexes gives a simplicial map from $\operatorname{Hom}(K_2,G)$ to the barycentric subdivision of $N(G)$, and the latter has the same homotopy type as $N(G)$.
We use the standard Lovasz [projection theorem](/theorems/1985) for neighborhood complexes in the following precise form: for every finite simple graph $H$, if $N(H)$ is defined as the simplicial complex of nonempty vertex sets having a common neighbor and $\operatorname{Hom}(K_2,H)$ is interpreted as the order complex of the Hom poset above, then the projection-induced map $\operatorname{Hom}(K_2,H) \to \operatorname{sd} N(H)$ is a homotopy equivalence. The graph $G$ is finite and simple by the theorem statement, and the preceding definition of $N(G)$ is exactly the common-neighbor neighborhood complex. Applying the theorem with $H=G$, the complex $\operatorname{Hom}(K_2,G)$ is homotopy equivalent to $N(G)$. Since $N(G)$ is $(r-1)$-connected by hypothesis, with $(-1)$-connected understood as nonempty when $r=0$, and connectedness up to degree $r-1$ is invariant under homotopy equivalence, $\operatorname{Hom}(K_2,G)$ is also $(r-1)$-connected.
[/step]
[step:Identify the target with the antipodal sphere]
First exclude the case $m=1$. If $G$ had a proper $1$-coloring, then no two vertices of $G$ would be adjacent, so no nonempty set of vertices could have a common neighbor and $N(G)$ would be empty. Since $r \in \mathbb{Z}_{\ge 0}$ and $N(G)$ is $(r-1)$-connected, with $(-1)$-connected meaning nonempty, $N(G)$ is nonempty when $r=0$ and is path-connected in particular when $r \ge 1$, a contradiction. Hence every proper coloring under consideration has $m \ge 2$.
For the complete graph $K_m$ with $m \ge 2$, we use the standard complete-graph Hom-complex computation: $\operatorname{Hom}(K_2,K_m)$ is $\mathbb{Z}/2$-homotopy equivalent to the sphere $S^{m-2}$ with the antipodal $\mathbb{Z}/2$-action. Therefore, using the antipodal sphere index computation, the $\mathbb{Z}/2$-index of $\operatorname{Hom}(K_2,K_m)$ is $m-2$, where the $\mathbb{Z}/2$-index of a finite free $\mathbb{Z}/2$-complex $X$ is the least integer $d \ge 0$ for which there exists a $\mathbb{Z}/2$-equivariant map $X \to S^d$ with the antipodal action on $S^d$.
[/step]
[step:Apply the index obstruction from Borsuk-Ulam]
Let $X := \operatorname{Hom}(K_2,G)$ and $Y := \operatorname{Hom}(K_2,K_m)$. From the first step, the coloring gives a $\mathbb{Z}/2$-equivariant map $X \to Y$. From the second step, $X$ is $(r-1)$-connected. From the third step, $Y$ has $\mathbb{Z}/2$-index $m-2$.
The external $\mathbb{Z}/2$-index form of the Borsuk-Ulam theorem, equivalently its [Dold theorem](/theorems/6495) index consequence, states that if a finite free $\mathbb{Z}/2$-complex $X$ is $(r-1)$-connected, then $\operatorname{ind}_{\mathbb{Z}/2}(X) \ge r$. The monotonicity theorem for the $\mathbb{Z}/2$-index states that if there is a $\mathbb{Z}/2$-equivariant map $X \to Y$, then $\operatorname{ind}_{\mathbb{Z}/2}(X) \le \operatorname{ind}_{\mathbb{Z}/2}(Y)$. The hypotheses are satisfied: $X$ is finite because $G$ is finite, the involution is free by the looplessness argument in the first step, $X$ is $(r-1)$-connected by the projection theorem step, and the map $X \to Y$ is equivariant by construction. Hence
\begin{align*}
r \le \operatorname{ind}_{\mathbb{Z}/2}(X) \le \operatorname{ind}_{\mathbb{Z}/2}(Y) = m-2.
\end{align*}
Thus $m \ge r+2$.
[guided]
We now extract the numerical lower bound from the three constructions already established. Put $X := \operatorname{Hom}(K_2,G)$ and $Y := \operatorname{Hom}(K_2,K_m)$. The coloring step gives a $\mathbb{Z}/2$-equivariant map $X \to Y$, because the graph homomorphism $\varphi: G \to K_m$ sends $(A,B)$ to $(\varphi(A),\varphi(B))$ and this assignment commutes with the coordinate-swap involutions. The same step also verified that the $\mathbb{Z}/2$-action on $X$ is free: a fixed poset element would have $A=B$, forcing a loop at any $a \in A$.
The source $X$ is $(r-1)$-connected. Indeed, the precise Lovasz projection theorem for neighborhood complexes applies because $G$ is a finite simple graph and $N(G)$ is the common-neighbor neighborhood complex. More precisely, the assignment $(A,B) \mapsto A$ is an order-preserving map from $\mathcal{P}_G$ to the face poset of $N(G)$, hence induces a simplicial map from $X$ to the barycentric subdivision of $N(G)$, and the external projection theorem says this induced map is a homotopy equivalence. Since $N(G)$ is $(r-1)$-connected by hypothesis, with $(-1)$-connected interpreted as nonempty when $r=0$, and connectivity up to degree $r-1$ is invariant under homotopy equivalence, $X$ is $(r-1)$-connected.
The target $Y$ has index $m-2$. The case $m=1$ cannot occur under the present hypotheses: a proper $1$-coloring would make $G$ edgeless, hence $N(G)$ empty, contradicting $(r-1)$-connectedness for $r \in \mathbb{Z}_{\ge 0}$ under the convention that $(-1)$-connected means nonempty. Thus $m \ge 2$. For $m \ge 2$, the external complete-graph Hom-complex computation gives a $\mathbb{Z}/2$-homotopy equivalence from $Y$ to the antipodal sphere $S^{m-2}$. Therefore, by the antipodal sphere index computation, $\operatorname{ind}_{\mathbb{Z}/2}(Y) = m-2$.
The relevant obstruction is the $\mathbb{Z}/2$-index. For a finite free $\mathbb{Z}/2$-complex $Z$, define $\operatorname{ind}_{\mathbb{Z}/2}(Z)$ to be the least integer $d \ge 0$ such that there exists a $\mathbb{Z}/2$-equivariant map $Z \to S^d$, where $S^d$ carries the antipodal action. The external $\mathbb{Z}/2$-index form of the Borsuk-Ulam theorem, equivalently the Dold theorem index consequence, says that if $Z$ is $(r-1)$-connected, then $\operatorname{ind}_{\mathbb{Z}/2}(Z) \ge r$. The monotonicity theorem for the $\mathbb{Z}/2$-index says that an equivariant map $Z \to W$ forces $\operatorname{ind}_{\mathbb{Z}/2}(Z) \le \operatorname{ind}_{\mathbb{Z}/2}(W)$. These hypotheses are satisfied for $X$: it is finite because $G$ is finite, the action is free by the looplessness check above, and it is $(r-1)$-connected by the projection theorem. The monotonicity hypothesis is satisfied by the equivariant map $X \to Y$ constructed from the coloring.
Applying the lower bound to $X$ gives
\begin{align*}
r \le \operatorname{ind}_{\mathbb{Z}/2}(X).
\end{align*}
Applying monotonicity of index to the equivariant map $X \to Y$ gives
\begin{align*}
\operatorname{ind}_{\mathbb{Z}/2}(X) \le \operatorname{ind}_{\mathbb{Z}/2}(Y).
\end{align*}
Using the complete-graph computation for $Y$, we get
\begin{align*}
\operatorname{ind}_{\mathbb{Z}/2}(Y) = m-2.
\end{align*}
Combining the three relations gives
\begin{align*}
r \le \operatorname{ind}_{\mathbb{Z}/2}(X) \le \operatorname{ind}_{\mathbb{Z}/2}(Y) = m-2.
\end{align*}
Therefore $m \ge r+2$.
[/guided]
[/step]
[step:Conclude the chromatic lower bound]
The integer $m$ was the number of colors in an arbitrary proper coloring of $G$. The previous step shows that every such $m$ satisfies $m \ge r+2$. By definition, the chromatic number $\chi(G)$ is the minimum number of colors in a proper coloring of $G$. Taking the minimum over all proper colorings gives $\chi(G) \ge r+2$. This is the desired lower bound.
[/step]