Problem Statement
The original can be found here: https://www.reddit.com/r/mathriddles/comments/mgsg6n/a_game_between_elves/
The empress has organised a game for the elves of elf city. In her very large park she has positioned stations, each labelled by a non-negative real number. Initially, there is an elf at each station. Because there are so many elves, she has had to create many stations — indeed, every \(x \geq 0\) corresponds to some station \(S_x\).
The empress will have elves run between stations in the following way: at every station \(S_x\) where \(x > 0\), there is a note telling the elves currently positioned there where they should go next. Crucially, the index of this next station will always be smaller than the index of the current one (so if at \(S_x\) the note says to go to \(S_y\), we must have \(y < x\)). The station \(S_0\) does not have a note: if an elf reaches \(S_0\), they stay put. Every time the horn is blown, all elves travel to their next station, and wait till the next horn blow. The game ends after \(\omega\) horn blows (elves live forever, of course).
Is it possible for uncountably many stations to be occupied when the game ends?
(as with previous elf problems, AC is a law of the land)
Mathematical formulation
This problem can be reformulated mathematically.
Build a function \(f\) with the following properties.
\(f: \mathbb{R}^+ \rightarrow \mathbb{R}^+ \)
\(\forall x > 0 \in \mathbb{R}, f(x) < x\)
\(f(0) = 0\)
\(\forall y \in \mathbb{R}, \exists x \in \mathbb{R} : \lim_{n \rightarrow \infty} f^n(x) = y\)
Note that \(\forall n, \forall y \in \mathbb{R}, \exists x \in \mathbb{R} :f^n(x) = y\)
Is not sufficient to make this work in the limit.
Because obviously \(f(x) = x/2\) works for every \(n\), but \(\lim_{n \rightarrow \infty} f^n(x) = 0\)
Solution
Let us note \(\lim_{n \rightarrow \infty} f^n(x)\) as \(f^\omega(x)\).
Consider the equivalence relation \(x \sim y \Leftrightarrow x-y \in \mathbb{Q}\)
Call the partitions created by this equivalence relation \(\mathcal{S}\)
The fact that this relation is an equivalence relation is trivial. The partitions \(\mathcal{S}\) has the following properties:
Each subset is dense in the positive reals (cause \(\mathbb{Q}\) is)
Each subset is countable (cause there exists bijection with \(\mathbb{Q}\))
There are uncountable subsets (cause the union is uncountable, and each set is countable).
According to the Axiom of choice, there exists an bijection from \(\mathcal{S}\) to \(\mathbb{R}\). Call this bijection \(\mu\).
Create for each \(S \in \mathcal{S}\) a subset \(T_S\) defined by \[T_S = \left\{s \in S \middle| s > \mu(S) \right\}\]
This set of subsets \(\mathcal{T}\) has the following properties:
All subsets are disjunct.
Each subset is dense in the reals larger than \(\mu(S)\).
Each subset is countable
There are uncountable subsets
Define \(\mu'\) such that \(\mu'(T_S) = \mu(S)\).
Now note that \(\inf T_S = \mu'(T_S)\) This is trivial because the subset is dense in the reals larger than \(\mu'(T_S)\).
From this follows that for each \(T_S\) there exists a deceasing sequence that as \(\mu'(T_S)\) as limit. Call this \(a_{TS}\).
Define \(\varphi : T_S \rightarrow \mathbb{R}\) such that \(\varphi(x)\) equals the first value in \(a_{TS}\) smaller than \(x\). This is well defined, as the limit is lower than \(x\) so a value exists.
Define \(\phi : \mathbb{R} \rightarrow \mathbb{R}\) such that \(\phi(x)\) is \(\varphi(x)\) if \(x \in T_S\), and 0 otherwise. As all options for \(T_S\) are disjunct, this is well defined.
After one application, the value becomes an element of the sequence \(a_{TS}\). After another application of the function, the value becomes an element further on in the sequence. This means that the sequence \(\phi^i(x)\) for \(i > 0\) is a subsequence of \(a_{TS}\), so as \(a_{TS}\) converges to \(\mu'(T_S)\), so does \(\phi^i(x)\).
This means that if \(x \in T_S\) then \(\phi^\omega(x) = \mu'(T_S)\)
This means that the range of \(\phi^\omega(x)\) is the range of \(\mu'\), which is the range of \(\mu\) which is all real numbers. So we have found the function we where looking for.