[proofplan]
Let $w_1(X) \in H^1(X/(\mathbb Z/2);\mathbb F_2)$ denote the first Stiefel--Whitney class of the quotient double cover $X \to X/(\mathbb Z/2)$, and let $\operatorname{coind}_{\mathbb Z/2}(X) := \sup\{k \in \mathbb N_0 : w_1(X)^k \neq 0\}$ be the Stiefel--Whitney height of this cover. Here $\mathbb RP^n$ denotes real projective $n$-space, namely the quotient of $S^n$ by the antipodal $\mathbb Z/2$-action. We show that any equivariant map from $X$ to an antipodal sphere forces a nilpotence bound on this class. The equivariant map descends to a map of quotient spaces $X/(\mathbb Z/2) \to \mathbb RP^n$, and compatibility of the two double covers identifies $w_1(X)$ with the pullback of the standard generator of $H^1(\mathbb RP^n;\mathbb F_2)$. Since this generator has zero $(n+1)$-st power, the same is true of $w_1(X)$, so no nonzero power of $w_1(X)$ can occur above degree $n$. Taking the infimum over all such $n$ gives the desired inequality.
[/proofplan]
[step:Reduce the inequality to an arbitrary equivariant map into an antipodal sphere]
Recall that $\operatorname{ind}_{\mathbb Z/2}(X)$ is the infimum of all $n \in \mathbb N_0$ for which there exists a continuous $\mathbb Z/2$-equivariant map $X \to S^n$, where $S^n$ carries the antipodal action. If $\operatorname{ind}_{\mathbb Z/2}(X)=\infty$, then the asserted inequality holds by the order convention $m \leq \infty$ for every $m \in \mathbb N_0 \cup \{\infty\}$. Assume therefore that $\operatorname{ind}_{\mathbb Z/2}(X)<\infty$.
Let $n \in \mathbb N_0$ be such that there exists a continuous $\mathbb Z/2$-equivariant map
\begin{align*}
f: X \to S^n.
\end{align*}
Here $S^n$ is equipped with the antipodal action. It is enough to prove
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) \leq n,
\end{align*}
because the resulting estimate holds for every admissible $n$, and hence holds after taking the infimum over all such $n$.
[/step]
[step:Descend the equivariant map to a map of orbit spaces]
Let $q_X: X \to X/(\mathbb Z/2)$ be the orbit projection, and let $q_n: S^n \to \mathbb RP^n$ be the quotient map for the antipodal action. Since $f$ is $\mathbb Z/2$-equivariant, it sends each $\mathbb Z/2$-orbit in $X$ into a single $\mathbb Z/2$-orbit in $S^n$. Therefore there is a unique continuous map $\bar f: X/(\mathbb Z/2) \to \mathbb RP^n$ such that
\begin{align*}
\bar f(q_X(x)) = q_n(f(x))
\end{align*}
for every $x \in X$. Equivalently,
\begin{align*}
\bar f \circ q_X = q_n \circ f.
\end{align*}
[guided]
The point of passing to quotient spaces is that the class $w_1(X)$ lives on $X/(\mathbb Z/2)$, not on $X$ itself. We therefore need the equivariant map $f: X \to S^n$ to produce an ordinary continuous map between the bases of the two double covers.
Define $q_X: X \to X/(\mathbb Z/2)$ to be the orbit projection for the given free $\mathbb Z/2$-action on $X$, and define $q_n: S^n \to \mathbb RP^n$ to be the quotient map for the antipodal action on $S^n$. Since $f$ is $\mathbb Z/2$-equivariant, for every $x \in X$ and every $g \in \mathbb Z/2$ we have
\begin{align*}
f(g \cdot x) = g \cdot f(x).
\end{align*}
Thus $x$ and $g \cdot x$ have images in the same antipodal orbit in $S^n$. This means that the formula
\begin{align*}
\bar f(q_X(x)) := q_n(f(x))
\end{align*}
is independent of the chosen representative $x$ of the orbit $q_X(x)$. Hence it defines a map
\begin{align*}
\bar f: X/(\mathbb Z/2) \to \mathbb RP^n.
\end{align*}
The map $\bar f$ is continuous by the quotient property of $q_X$, because the composite $q_n \circ f: X \to \mathbb RP^n$ is continuous and is constant on the fibers of $q_X$. The defining relation is
\begin{align*}
\bar f \circ q_X = q_n \circ f.
\end{align*}
This relation records that the two double covers are compatible through $f$ and $\bar f$.
[/guided]
The nilpotence argument below will turn this quotient-space construction into the cohomological bound.
[/step]
[step:Identify the first Stiefel--Whitney class as a pullback from projective space]
Let $a \in H^1(\mathbb RP^n;\mathbb F_2)$ denote the first Stiefel--Whitney class of the antipodal double cover $q_n: S^n \to \mathbb RP^n$. By the covering hypothesis in the theorem statement, the orbit projection $q_X: X \to X/(\mathbb Z/2)$ is a double covering projection. The class $w_1(X)$ is, by definition in this theorem, the first Stiefel--Whitney class of this quotient double cover associated to the free $\mathbb Z/2$-action on $X$.
We verify that the square determined above is a morphism of double covers. The map on total spaces is $f: X \to S^n$, the map on base spaces is $\bar f: X/(\mathbb Z/2) \to \mathbb RP^n$, and the compatibility condition is exactly
\begin{align*}
\bar f \circ q_X = q_n \circ f.
\end{align*}
For each orbit $q_X(x) \in X/(\mathbb Z/2)$, the restriction of $f$ sends the fiber $q_X^{-1}(q_X(x)) = \{x, g \cdot x\}$, where $g$ denotes the nonidentity element of $\mathbb Z/2$, into the fiber $q_n^{-1}(\bar f(q_X(x))) = \{f(x), g \cdot f(x)\}$ because $f(g \cdot x) = g \cdot f(x)$. Since the antipodal action on $S^n$ is free, these two points are distinct, so the fiber map is a bijection.
Let $P$ denote the pullback total space of $q_n$ along $\bar f$:
\begin{align*}
P := \{(b,y) \in X/(\mathbb Z/2) \times S^n : \bar f(b)=q_n(y)\}.
\end{align*}
Define
\begin{align*}
\Phi: X \to P, \qquad x \mapsto (q_X(x),f(x)).
\end{align*}
The defining identity $\bar f \circ q_X = q_n \circ f$ makes $\Phi$ well-defined and continuous. The preceding fiberwise bijectivity says that $\Phi$ restricts to a bijection from each fiber of $q_X$ onto the corresponding fiber of the pullback cover $P \to X/(\mathbb Z/2)$. Since both maps are double covering projections over the same base and $\Phi$ covers the identity map on $X/(\mathbb Z/2)$, the local trivializations of the two covers show that $\Phi$ is a homeomorphism over $X/(\mathbb Z/2)$. Thus $q_X$ is isomorphic to the pullback double cover $\bar f^*q_n$ over $X/(\mathbb Z/2)$.
By the naturality property in the definition of the first Stiefel--Whitney class of a double cover, applied to this verified pullback square of double covers, we obtain
\begin{align*}
w_1(X) = \bar f^*(a)
\end{align*}
in $H^1(X/(\mathbb Z/2);\mathbb F_2)$.
[/step]
[step:Pull back the nilpotence relation from $H^*(\mathbb RP^n;\mathbb F_2)$]
We use the standard computation of the mod-$2$ [cohomology ring](/theorems/2271) of real projective space:
\begin{align*}
H^*(\mathbb RP^n;\mathbb F_2) \cong \mathbb F_2[a]/(a^{n+1}),
\end{align*}
where $a \in H^1(\mathbb RP^n;\mathbb F_2)$ is the standard degree-one generator. In particular,
\begin{align*}
a^{n+1} = 0
\end{align*}
in $H^{n+1}(\mathbb RP^n;\mathbb F_2)$. Since the induced map
\begin{align*}
\bar f^*: H^*(\mathbb RP^n;\mathbb F_2) \to H^*(X/(\mathbb Z/2);\mathbb F_2)
\end{align*}
is a graded ring homomorphism, it preserves cup powers. Therefore
\begin{align*}
w_1(X)^{n+1} = \bar f^*(a)^{n+1} = \bar f^*(a^{n+1}) = \bar f^*(0) = 0.
\end{align*}
[guided]
The cohomology computation for real projective space is the point where the dimension $n$ enters. We use the standard mod-$2$ cohomology ring computation for real projective space:
\begin{align*}
H^*(\mathbb RP^n;\mathbb F_2) \cong \mathbb F_2[a]/(a^{n+1}),
\end{align*}
where $a \in H^1(\mathbb RP^n;\mathbb F_2)$ is the first Stiefel--Whitney class of the antipodal double cover. This quotient ring relation means precisely that
\begin{align*}
a^{n+1} = 0
\end{align*}
in $H^{n+1}(\mathbb RP^n;\mathbb F_2)$.
From the previous step, $w_1(X) = \bar f^*(a)$. The induced cohomology map
\begin{align*}
\bar f^*: H^*(\mathbb RP^n;\mathbb F_2) \to H^*(X/(\mathbb Z/2);\mathbb F_2)
\end{align*}
is a graded ring homomorphism, so it preserves cup products and therefore preserves powers. Applying this to the nilpotence relation gives
\begin{align*}
w_1(X)^{n+1} = \bar f^*(a)^{n+1} = \bar f^*(a^{n+1}) = \bar f^*(0) = 0.
\end{align*}
[/guided]
[/step]
[step:Conclude that the Stiefel--Whitney height is at most the equivariant index]
We have proved that every $n \in \mathbb N_0$ admitting a continuous $\mathbb Z/2$-equivariant map $X \to S^n$ satisfies
\begin{align*}
w_1(X)^{n+1} = 0.
\end{align*}
Consequently, if $k \geq n+1$, then
\begin{align*}
w_1(X)^k = w_1(X)^{n+1} w_1(X)^{k-n-1} = 0,
\end{align*}
so there is no integer $k \geq n+1$ such that $w_1(X)^k \neq 0$. By the definition
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) := \sup\{k \in \mathbb N_0 : w_1(X)^k \neq 0\},
\end{align*}
this gives
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) \leq n.
\end{align*}
Taking the infimum over all such $n$ gives
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) \leq \operatorname{ind}_{\mathbb Z/2}(X).
\end{align*}
This proves the theorem.
[guided]
We have shown that every admissible equivariant target dimension $n$ forces
\begin{align*}
w_1(X)^{n+1} = 0.
\end{align*}
Now let $k \in \mathbb N_0$ satisfy $k \geq n+1$. Since cup product is associative and $w_1(X)^{n+1}=0$, we have
\begin{align*}
w_1(X)^k = w_1(X)^{n+1}w_1(X)^{k-n-1} = 0.
\end{align*}
Thus no nonzero Stiefel--Whitney power can occur in degree $k \geq n+1$.
By the theorem's definition,
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) := \sup\{k \in \mathbb N_0 : w_1(X)^k \neq 0\}.
\end{align*}
The preceding vanishing says that this supremum is at most $n$. Since the argument holds for every $n \in \mathbb N_0$ admitting a continuous $\mathbb Z/2$-equivariant map $X \to S^n$, taking the infimum over all such $n$ yields
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X) \leq \operatorname{ind}_{\mathbb Z/2}(X).
\end{align*}
This proves the theorem.
[/guided]
[/step]
