I’m thinking about the well known pattern generated by constructing a series of squares with side lengths following the Fibonacci sequence. Each time we add in a new square, we choose a side of the current rectangle for it to be ‘branching off from’, for lack of a better term. If we loop around so that we first choose the right side, the top, the left and then the bottom side in that order repeatedly, we obtain something like the image below.
It is often stated that this iterative procedure will ‘tile the plane’. I take this to mean that given any point on the infinite two-dimensional Euclidean plane, there exists at least one (or possibly exactly one, depending on our definition) square that contains this point. More loosely: in the limit (as the number of squares approaches infinity), the whole plane is covered by this pattern of squares.
Here it is fairly obvious that this is going to be the case, and yet as always I’m wondering if there is a more formal way that we can prove this, or whether such a proof is even a sensible notion.
Could we perhaps show that the function (from the set of squares to 2D Euclidean space) mapping a given square to the set of points that it contains is a surjection in the sense that all of the points in the plane exist in at least one of these sets? Or, I suppose, show that there exists a function from the points to the squares with the opposite relation that is defined on the whole plane?
Maybe we could start by observing that the space occupied by the first square is covered, and then use an induction step to show that given any point on the plane, the surrounding points (in some sense) are also covered at some point in the iteration.
In order to even construct such a proof we would need a more rigorous definition of ‘tiles the plane’ than ‘it covers the whole thing after a long enough time’. Does such a definition exist? Surely it must, and yet I can’t find it anywhere.