# A counterexample to periodic tiling in dimension three

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A translational tile with no fully periodic tiling in dimension three](../../preprints/A-translational-tile-with-no-fully-periodic-tiling-in-dimension-three-September-23-2026/paper.pdf)

## Scope

The periodic-tiling question asks whether a finite tile that tiles a lattice must admit a periodic tiling. The formalized counterexample is a finite tile in $\mathbb Z^3$ that tiles but has no complement invariant under a finite-index subgroup. Its unit-cube thickening also tiles $\mathbb R^3$ almost everywhere but admits no fully periodic tiling, even with arbitrary real translation vectors. The result also establishes that dimension three is the least lattice dimension where this failure occurs.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Aperiodic translational tile in dimension three | [PeriodicTilingThree.lean](../ComparatorChallenges/PeriodicTilingThree.lean) |