(Minor corrections) This is my own take at the corollary to the Intermediate Value theorem on the unit circle. It is not substantially different to the proof linked to, so its value is zero everywhere (maybe except for a countable subset). In particular, this is a special case of the much more general Borsuk-Ulam theorem.
Consider f a continuous function with domain on the unit circle. Then there exists at least a pair of points x0, x1 ∈ [0…2π) such that f(x0) = f(x0 + π) and f(x1) = f(x1 + π).
This is a purely existential statement, so it would be somewhat pointless (!) to strive to identify (or construct) a value x0 witnessing to the theorem. The only obvious possibility is to work with f by itself; that is, by focusing on the range and not on the domain of f. I must head towards something to which I can apply the IVT, and this lets me fix a number of things.
First, f is real-valued, as required by the IVT. Second, f is periodic, since if there were an x for which f(x) ≠ f(x + 2π), the difference |f(x + 2π) - f(x + ε)| would be large for |x + 2π - x - ε| = |ε| arbitrarily small on the unit circle. Third, since I see that the hypothesis mentions f(x) and f(x + π) being equal, I'm forced to consider the difference g(x) = f(x) - f(x + π). Fourth, g is continuous as f is.
Now, I have a choice in stating the proof; or rather, I have two different ways to show the existence of an interval satisfying the IVT.
The first one is to consider an arbitrary x ∈ [0…2π), and to see that g(x + π) = f(x + π) - f(x + 2π) = f(x + π) - f(x) = -g(x). Since -|g(x)| ≤ 0 ≤ |g(x)| and g is continuous, there must be some x0 ∈ [-|g(x)| … |g(x)|] such that g(x0) = 0.
The other possibility is to note that there must be a pair of values x+ and x- such that g(x+) ≥ 0 and g(x-) ≤ 0, or else f would be monotonic, hence discontinuous. Since g(x-) ≤ 0 ≤ g(x+) and g is continuous, there exists an x0 ∈ [x- … x+] such that g(x0) = 0.
Both things amount to the same; namely, there is a zero of g in the unit circle. As the domain is periodic, there must be another zero in the interval "across π" with respect to the original one (that is, the one having the endpoints listed in the opposite order, modulo 2π), call it x1. But this is precisely the posited pair of points that make f(x0) = f(x0 + π) and f(x1) = f(x1 + π).
Note that both choices are not equally potent: the first interval [-|g(x)| … |g(x)|] has the endearing property of being a function of an arbitrary x on the unit circle. This not only means that I can trade two existentials for one universal, making the theorem more constructive; it also permits a direct application of a root-finding method to hone in the zero.
The usual formulation of this is that there exists a pair of antipodal points where the function takes the same value. We see there is more than one, as the inventors of the Gömböc show. Also, as opposed to the proof by contradiction stated there, this is a direct proof.