Periodic tiling conjecture

AbbreviationTiling of an abelian group by translates#✓fully proved

Let \(G\) be an abelian group and let \(F, A \subseteq G\). Then \(F\) tiles \(G\) with tiling set \(A\) if the map \(A \times F \to G\), \((a, f) \mapsto a + f\), is a bijection; equivalently, every element of \(G\) lies in \(a + F\) for exactly one \(a \in A\).

abbrev IsTiling (F A : Set G) : Prop := AddSubgroup.IsComplement A F

Used by 1

Used byAperiodic tiling equation

DefinitionPeriodic tiling set#✓fully proved

A subset \(A\) of an abelian group \(G\) is periodic if there exist a subgroup \(H\) of \(G\) of finite index and a finite set \(S \subseteq G\) such that \(A = S + H\), that is, \(A\) is the union of finitely many cosets of \(H\).

def IsPeriodicTilingSet (A : Set G) : Prop :=
  ∃ H : AddSubgroup G, H.FiniteIndex ∧ ∃ s : Finset G, A = s + H

Used by 1

Used byAperiodic tiling equation

StructureAperiodic tiling equation#✓fully proved

Let \(G\) be an abelian group. A set \(F \subseteq G\) forms an aperiodic tiling equation if \(F\) tiles \(G\) with some tiling set \(A \subseteq G\), and no tiling set \(A \subseteq G\) with which \(F\) tiles \(G\) is periodic.

structure IsAperiodicTilingEquation (F : Set G) where
  solvable : ∃ A, IsTiling F A
  aperiodic : ∀ A, IsTiling F A → ¬ IsPeriodicTilingSet A

Uses 2 · Used by 2

Statement usesPeriodic tiling set · Tiling of an abelian group by translates

Used byAperiodic tiling equations in high-dimensional integer lattices · Greenfeld–Tao counterexample to the periodic tiling conjecture

TheoremGreenfeld–Tao counterexample to the periodic tiling conjecture#●ready to prove

There exist a finite abelian group \(G_0\) and a finite non-empty set \(F \subseteq \mathbb{Z}^2 \times G_0\) that forms an aperiodic tiling equation in the group \(\mathbb{Z}^2 \times G_0\).

public theorem_wanted theorem_1_4 : ∃ (G₀ : Type) (_ : AddCommGroup G₀) (_ : Finite G₀),
    ∃ F : Set (ℤ × ℤ × G₀), F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F

Sources

• R. Greenfeld and T. Tao, A counterexample to the periodic tiling conjecture, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_periodic_tiling_conjecture of the lean-eval benchmark.

Uses 1

Statement usesAperiodic tiling equation

TheoremAperiodic tiling equations in high-dimensional integer lattices#●ready to prove

There is a natural number \(d_0\) such that for every natural number \(d \ge d_0\) there exists a finite non-empty set \(F \subseteq \mathbb{Z}^d\) that forms an aperiodic tiling equation in \(\mathbb{Z}^d\).

public theorem_wanted corollary_1_6 : ∀ᶠ d in atTop, ∃ (F : Set (Fin d → ℤ)),
    F.Finite ∧ F.Nonempty ∧ IsAperiodicTilingEquation F

Sources

• R. Greenfeld and T. Tao, A counterexample to the periodic tiling conjecture, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_periodic_tiling_conjecture of the lean-eval benchmark.

Uses 1

Statement usesAperiodic tiling equation

DefinitionContinuous tiling of Euclidean space#✓fully proved

For \(d \in \mathbb{N}\), a set \(\sigma \subseteq \mathbb{R}^d\) continuously tiles \(\mathbb{R}^d\) with tiling set \(\Lambda \subseteq \mathbb{R}^d\) if for almost every \(x \in \mathbb{R}^d\) (with respect to Lebesgue measure) there is exactly one \(v \in \Lambda\) with \(x \in v + \sigma\).

def IsContinuousTiling (σ Λ : Set (Fin d → ℝ)) : Prop := ∀ᵐ x, ∃! v ∈ Λ, x ∈ (v +ᵥ σ)

Used by 1

Used byAperiodic continuous tiling equation

DefinitionPeriodic continuous tiling set#✓fully proved

For \(d \in \mathbb{N}\), a set \(\Lambda \subseteq \mathbb{R}^d\) is periodic if there exist a lattice \(L \subseteq \mathbb{R}^d\), that is, a discrete additive subgroup that spans \(\mathbb{R}^d\) over \(\mathbb{R}\), and a finite set \(S \subseteq \mathbb{R}^d\) such that \(\Lambda = S + L\), so that \(\Lambda\) is the union of finitely many cosets of \(L\).

def IsPeriodicContinuousTilingSet (Λ : Set (Fin d → ℝ)) : Prop :=
    ∃ (L : Submodule ℤ (Fin d → ℝ)) (_ : DiscreteTopology L) (_ : IsZLattice ℝ L),
      ∃ s : Finset (Fin d → ℝ), Λ = s + L

Used by 1

Used byAperiodic continuous tiling equation

StructureAperiodic continuous tiling equation#✓fully proved

For \(d \in \mathbb{N}\), a set \(\sigma \subseteq \mathbb{R}^d\) forms an aperiodic continuous tiling equation if \(\sigma\) continuously tiles \(\mathbb{R}^d\) with some tiling set \(\Lambda \subseteq \mathbb{R}^d\), and no tiling set \(\Lambda\) with which \(\sigma\) continuously tiles \(\mathbb{R}^d\) is periodic.

structure IsAperiodicContinuousTilingEquation (σ : Set (Fin d → ℝ)) where
  solvable : ∃ Λ, IsContinuousTiling σ Λ
  aperiodic : ∀ Λ, IsContinuousTiling σ Λ → ¬ IsPeriodicContinuousTilingSet Λ

Uses 2 · Used by 1

Statement usesContinuous tiling of Euclidean space · Periodic continuous tiling set

Used byAperiodic continuous tiling equations in high-dimensional Euclidean space

TheoremAperiodic continuous tiling equations in high-dimensional Euclidean space#●ready to prove

There is a natural number \(d_0\) such that for every natural number \(d \ge d_0\) there exists a bounded measurable set \(\sigma \subseteq \mathbb{R}^d\) of positive Lebesgue measure that forms an aperiodic continuous tiling equation.

public theorem_wanted corollary_1_7 : ∀ᶠ d in atTop, ∃ σ : Set (Fin d → ℝ), IsBounded σ ∧ MeasurableSet σ ∧
    0 < volume σ ∧ IsAperiodicContinuousTilingEquation σ

Sources

• R. Greenfeld and T. Tao, A counterexample to the periodic tiling conjecture, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_periodic_tiling_conjecture of the lean-eval benchmark.

Uses 1

Statement usesAperiodic continuous tiling equation

6 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.