I'm aware of the constructive proof of Brouwer's fixed-point theorem via Sperner's Lemma, and I love it for its simplicity, directness, and constructiveness.
However, I still have a lingering frustration at the proof of the theorem I originally encountered, which instead proceeds by contradiction via a diagram-chasing argument. Try as I might, it's hard for me to see a clear "mapping" between the two.
I'm wondering if there's any sort of "happy middle-ground" between the continuous, machinery-heavy contradiction proof and the fairly direct discrete constructive proof. Can we prove Brouwer's fixed-point theorem constructively without applying Sperner's lemma to a suitable triangulation? If so, how?
Best Answer
There is no constructive proof of Brouwer’s fixed point theorem at all.
In particular, the following is not provable constructively:
Informally, the reason this theorem isn’t constructively valid is that a very small change in $f$ can result in a large change in the location of a root of $f$. So there is no algorithm to actually locate a root of $f$, which should be present if the intermediate value theorem can be proved constructively.
However, the intermediate value theorem follows from Brouwer’s Theorem in 1D.
To show this, note that piecewise definitions of continuous functions are constructively valid.
For consider some continuous $f : [-1, 1] \to \mathbb{R}$ with $f(0) \leq 0 \leq f(1)$. We wish to show $f$ has a root.
Our first step is "squishing" $f$. Define $g(x) = f(2x)$, $g : [-1/2, 1/2] \to \mathbb{R}$. Note that $g$ has a root if and only if $f$ does, and that $g$ is continuous.
The next step is bounding the range of $g$. Define
$h(x) = \begin{cases} -1/3 & g(x) \leq -1/3 \\ g(x) & -1/3 \leq g(x) \leq 1/3 \\ 1/3 & 1/3 \leq g(x) \end{cases}$
Note that $h : [-1/2, 1/2] \to [-1/3, 1/3]$, and that $c$ is a root of $h$ if and only if $c$ is a root of $g$. So $h$ has a root iff $c$ does.
Now, we apply the transformation which connects the two theorems. Define $i(x) = h(x) - x$, $i : [-1/2, 1/2] \to [-1, 1]$. Note that $i$ has a fixed point if and only if $h$ has a root.
Finally, we define
$j(x) = \begin{cases} i(-1/2) & x \leq -1/2 \\ i(x) & -1/2 \leq x \leq 1/2 \\ i(1/2) & 1/2 \leq x \end{cases}$
We see that $j : [-1, 1] \to [-1, 1]$ is a continuous function. Furthermore, note that any fixed point of $j$ must occur in the interval $[-1/2, 1/2]$. This is because if $x < -1/2$, then $j(x) = i(-1/2) = h(-1/2) + 1/2$. Since $h(-1/2) \geq -1/3$, we have $h(-1/2) + 1/2 \geq -1/3 + 1/2 = 1/6 > 0 > x$. Therefore, $x \geq -1/2$. A similar argument shows that $x \leq 1/2$. So a fixed point of $j$ is a fixed point of $i$. And if we have Brouwer's fixed point theorem, the closed unit ball in 1D is $[-1, 1]$, so $j$ must have a fixed point. $\square$
Note that Sperner's Lemma itself is perfectly constructively valid. So there must be some constructive issue in showing that Brouwer's Lemma is implied by Sperner's Lemma.
The issue is that the proof typically goes something like this. We triangulate the unit ball with increasing fineness. At each stage of the triangulation, we use Sperner's lemma to pick a particular point. This gives us a sequence of points. The sequence of points has a convergent subsequence by sequential compactness; this convergent subsequence must converge to a fixed point of our function.
The major issue here is actually the use of sequential compactness, which is constructively invalid. It cannot be shown constructively that every infinite sequence in $[0, 1]$ has a convergent subsequence. In fact, it cannot even be shown that every infinite sequence of zeroes and ones takes either $0$ or $1$ as a value infinitely often. The other parts of the proof have some minor constructive issues, but it appears to me that they can be rephrased reasonably enough.
However, if one assumes the compactness of $[0, 1]$, a classical equivalent of Brouwer's Theorem seems to be valid. The equivalent: there is no retraction from the closed unit ball to the closed unit sphere. Brouwer himself adopted axioms which allowed him to show $[0, 1]$ was compact, though he famously rejected classical logic (and thus, ironically, the very theorem which made him famous - the fixed point theorem).