# Compactness of domino tilings

I've read in Lemma 2 of the paper 1 that if every square region of the plane admits a tiling, then the whole plain admits a tiling, but the proof is omitted. This sounds like a compactness property, but I don't see how easy can be proven.

I added the tag "automata theory" because there is a correspondence between Wang tilings and finite state transducers.

Yes, this is a compactness property.

Let $$X$$ be the region you want to tile, and $$T$$ the finite set of possible tiles. The space $$T^X$$ of all assignments of tiles to $$X$$ is compact by Tychonoff’s theorem. For any finite $$X_0\subseteq X$$, the set $$C_{X_0}\subseteq T^X$$ of all correct tilings of $$X_0$$ is closed (in fact, clopen), and since $$C_{X_0\cup X_1}\subseteq C_{X_0}\cap C_{X_1}$$, they generate a filter. Thus, assuming every finite subset of $$X$$ can be tiled, the system $$\{C_{X_0}:X_0\subseteq X\text{ finite}\}$$ has fip, and by compacteness, its intersection is nonempty. This intersection is the set of all correct tilings of $$X$$.

Instead of all finite $$X_0$$, it suffices to use any family of finite subsets which is upwards directed and covers $$X$$, such as, in your case, the set of all finite square subregions of the plane.

Alternatively, you may set up the argument to use the compacteness of classical propositional logic: let $$\{p_{x,t}:x\in X,t\in T\}$$ be a set of propositional variables, and let $$C$$ be the theory consisting of the formulas $$\begin{gather*} \bigvee_{t\in T}p_{x,t},\qquad x\in X,\\ \neg(p_{x,t}\land p_{x,t'}),\qquad x\in X,t\ne t'\in T, \end{gather*}$$ and $$\neg(p_{x,t}\land p_{x',t'})$$ for all $$x,x'\in X$$ that are neighbours, and $$t,t'\in T$$ that are incompatible when placed on $$x$$ and $$x'$$, respectively. If each finite subset of $$X$$can be tiled, then $$C$$ is consistent, and any satisfying assignment gives a tiling of $$X$$.

• Yes, I thought about an argument using compactness of propositional logic. Yet this argument is in a sense not constructive because implicitly uses the Axiom of Chioce and hides an algorithmic property that should sound as follows: if $t_1: X \to T$ is a tiling and $t_2: Y \to T$ is another one whose with $Y\supseteq X$, then there exists a finite sequence of transformations of $t_2$ yielding a $t_3: Y \to T$ that extends $t_1$. Something similar is detailed in this answer math.stackexchange.com/a/36109/34750 but concerns other domini pieces rather than Wang tiles. – Alberto Apr 1 '19 at 7:23

First, there is an infinite tiling of the plane if and only if there are square tilings $$T_1 < T_2 < T_3 < \ ...$$ such that $$T_i$$ is an $$i \times i$$ square tiling, and $$T_i$$ is a subtiling of $$T_{i+1}$$.

Now, for each $$T_i$$ define $$f(T_i)$$ to be the size of the largest square tiling that $$T_i$$ is a subtiling of, where $$f(T_i) = \infty$$ if for all $$n > i$$, $$T_i$$ is a subtiling of some $$n\times n$$ tiling.

Lemma 1: if for an $$i \times i$$ tiling $$T_i$$, $$f(T_i) = \infty$$, then there is some $$(i+1) \times (i+1)$$ tiling $$T_{i+1}$$ with $$T_i < T_{i+1}$$ and $$f(T_{i+1}) = \infty$$.

Proof: Suppose not. Then look at the maximum value $$n$$ of $$f(T)$$ for $$(i+1) \times (i+1)$$ tilings containing $$T_i$$:

$$n = \max_{T > T_i \atop T \mathrm{\ is\ } (i+1) \times (i+1)} f(T).$$

If this is finite, then no tiling containing $$T_i$$ can be larger than $$n \times n$$, contradicting $$f(T_i) = \infty$$. And if it is infinite, one of the $$(i +1) \times (i+1)$$ tilings $$T$$ must have $$f(T) = \infty$$, as otherwise we have $$\infty$$ is the maximum of a finite number of finite integers (since there are a finite number of $$(i+1) \times (i+1)$$ tilings).

So at least one of the $$(i+1) \times (i+1)$$ tilings containing $$T$$ must have an infinite value for $$f$$. QED

Now, we can ask whether $$f(T_1) = \infty$$ for any single $$1 \times 1$$ tile. If not, then there is a maximum size square that admits a tiling. And if so, then given a tiling $$T_1$$ with $$f(T_1) = \infty$$, we can use lemma 1 to find tilings $$T_1 < T_2 < T_3 < \ ...$$ such that $$f(T_i) = \infty$$ for all $$i$$, showing that there is an infinite tiling of the plain.