Nivat conjecture

### What is the conjecture

The Nivat conjecture is a central open problem in combinatorics on words and symbolic dynamics concerning the relationship between local pattern complexity and global periodicity in two-dimensional configurations.

A two-dimensional configuration is a function
$$x : \mathbb{Z}^2 \mapsto \mathcal{A},$$
where: $\mathcal{A}$ is a finite alphabet.

For integers $n,m \ge 1$, the **block complexity** of $x$ is defined as the number $P_x(n,m)$ of distinct $n \times m$ rectangular patterns appearing in $x$.

A configuration $x$ is called **periodic** if there exists a nonzero vector $(a,b) \in \mathbb{Z}^2$ such that
$$x(i+a, j+b) = x(i,j) \quad \text{for all } (i,j) \in \mathbb{Z}^2.$$

The Nivat conjecture states:

If there exist integers $n,m \ge 1$ such that
$$P_x(n,m) \le nm,$$
then the configuration $x$ is periodic.

In other words, if the number of distinct $n \times m$ patterns appearing in a configuration is at most the area of the pattern, then the configuration must exhibit global periodic structure.

This can be viewed as a two-dimensional analogue of the Morse–Hedlund theorem in one dimension.

**Source:** https://en.wikipedia.org/wiki/Nivat_conjecture, https://en.wikipedia.org/wiki/Morse%E2%80%93Hedlund_theorem

---

### Prerequisites needed

#### Building blocks (from Mathlib):
- Basic discrete mathematics (ℤ², functions on lattices)
- Finite sets and cardinality
- Combinatorics on words (finite patterns, blocks)

#### Missing pieces (not in current Mathlib):
- Formal theory of symbolic dynamics (configurations, shifts, subshifts)
- Block complexity theory for ℤ² actions
- Periodicity criteria in multidimensional symbolic systems

---

### AMS categories

- ams-37 (Dynamical Systems and Ergodic Theory)
- ams-68 (Computer Science — Automata Theory and Formal Languages)
- ams-05 (Combinatorics)

---

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else