Proof of Nivat's conjecture

Theorem 1.1 (thm:main) and its proof in Section 6 of paper/nivat.tex.

nivat_rational carries out strong induction over rectangle area. The exact line ideal gives the smaller low-complexity rectangle of Corollary 2.3, and periodic_of_periodic_line_filter returns from the filtered configuration using Theorem 5.1. nivat then transfers periods through a rational alphabet labeling.

theorem Nivat.periodic_of_periodic_line_filter (c : Configuration ℚ) (hc : FiniteRange c) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hlow : complexity c (rectangle m n) ≤ m * n) (v : Lattice) (hv : v ≠ 0) (q : ℕ) (hq : 0 < q) (φ : Polynomial ℚ) (hdiv : φ ∣ Polynomial.X ^ q - 1) (hfiltered : Periodic (Algebra.act ((Algebra.lineEval v) φ) c)) : Periodic c

The polynomial-quotient step in Section 6. If the line-filtered configuration is periodic, divisibility by Z^q - 1 gives a mixed-difference identity; Theorem 5.1 then makes the original low-complexity configuration periodic.

theorem Nivat.nivat_rational (c : Configuration ℚ) (hc : FiniteRange c) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hlow : complexity c (rectangle m n) ≤ m * n) : Periodic c

The rational form of Theorem 1.1 (thm:main), proved in Section 6. Strong induction runs over rectangle area and all finite rational ranges, so it applies to the alphabet produced by each Laurent filter.

theorem Nivat.nivat {A : Type u_1} [Finite A] (c : Configuration A) (m n : ℕ) (hm : 0 < m) (hn : 0 < n) (hlow : complexity c (rectangle m n) ≤ m * n) : ∃ (h : Lattice), h ≠ 0 ∧ ∀ (z : Lattice), c (z + h) = c z

Theorem 1.1 (thm:main): a finite-alphabet configuration with a low-complexity positive rectangle has one nonzero global period. The proof in Section 6 transfers the rational theorem through the injective labeling of Section 1.1.