Orbit closure and pattern inheritance

This module formalizes the orbit closure and finite-pattern inheritance in Section 1.1 of paper/nivat.tex. It proves that nonperiodicity gives an infinite orbit closure, then applies Lemma 3.1 (lem:halfplane-pair) to the finite range subtype with its discrete topology.

The main results are finite_pattern_occurs, patternAt_mem_patterns_of_mem_orbitClosure, and halfPlane_pair_of_finiteRange_not_periodic. The last theorem returns the full pattern-language inclusion needed for Laurent annihilator inheritance.

def Nivat.Dynamics.orbit {A : Type u_1} (c : Configuration A) : Set (Configuration A)

The set of all integer translates of a configuration, as defined in Section 1.1.

Equations

• Nivat.Dynamics.orbit c = Set.range fun (h : Nivat.Lattice) => Nivat.shift h c

def Nivat.Dynamics.orbitClosure {A : Type u_1} [TopologicalSpace A] (c : Configuration A) : Set (Configuration A)

The closure of the translation orbit in the product topology, denoted by X_c in Section 1.1.

Equations

• Nivat.Dynamics.orbitClosure c = closure (Nivat.Dynamics.orbit c)

theorem Nivat.Dynamics.continuous_shift {A : Type u_1} [TopologicalSpace A] (h : Lattice) : Continuous (shift h)

Each shift is continuous in the product topology. This gives the shift invariance of X_c used in Section 1.1 and Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.isClosed_orbitClosure {A : Type u_1} [TopologicalSpace A] (c : Configuration A) : IsClosed (orbitClosure c)

The orbit closure X_c of Section 1.1 is closed in the product topology.

theorem Nivat.Dynamics.shift_mem_orbitClosure {A : Type u_1} [TopologicalSpace A] (c : Configuration A) (h : Lattice) : shift h c ∈ orbitClosure c

Every translate of the original configuration belongs to its orbit closure X_c, as used in Section 1.1.

theorem Nivat.Dynamics.mem_orbitClosure {A : Type u_1} [TopologicalSpace A] (c : Configuration A) : c ∈ orbitClosure c

The original configuration belongs to the orbit closure X_c of Section 1.1.

theorem Nivat.Dynamics.shift_orbitClosure {A : Type u_1} [TopologicalSpace A] (c : Configuration A) (h : Lattice) {x : Configuration A} (hx : x ∈ orbitClosure c) : shift h x ∈ orbitClosure c

The orbit closure X_c is invariant under every integer shift, as required by Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.finite_pattern_occurs {A : Type u_1} [TopologicalSpace A] [DiscreteTopology A] (c : Configuration A) {x : Configuration A} (hx : x ∈ orbitClosure c) (D : Finset Lattice) : ∃ (h : Lattice), ∀ z ∈ D, x z = c (z + h)

Every finite restriction of a point of X_c occurs in the original configuration. This is the finite-pattern inheritance property of Section 1.1; discreteness is needed only for the alphabet.

theorem Nivat.Dynamics.patternAt_mem_patterns_of_mem_orbitClosure {A : Type u_1} [TopologicalSpace A] [DiscreteTopology A] (c : Configuration A) {x : Configuration A} (hx : x ∈ orbitClosure c) (D : Finset Lattice) (u : Lattice) : patternAt x D u ∈ patterns c D

Every translated pattern of an orbit-closure point belongs to the original pattern language, by the inheritance property of Section 1.1.

theorem Nivat.Dynamics.infinite_orbitClosure_of_not_periodic {A : Type u_1} [TopologicalSpace A] (c : Configuration A) (hn : ¬Periodic c) : (orbitClosure c).Infinite

A nonperiodic configuration has an injective translation orbit and hence infinite orbit closure. This supplies the hypothesis of Lemma 3.1 in Corollary 3.6 (cor:periodic-difference).

theorem Nivat.Dynamics.halfPlane_pair_of_finiteRange_not_periodic {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (hn : ¬Periodic c) : ∃ (x : Configuration A) (y : Configuration A) (ν : ℝ × ℝ), FiniteRange x ∧ FiniteRange y ∧ ν.1 ^ 2 + ν.2 ^ 2 = 1 ∧ x 0 ≠ y 0 ∧ (∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) ∧ (∀ (D : Finset Lattice), patternAt y D 0 ∈ patterns c D) ∧ ∀ (z : Lattice), ν.1 * ↑z.1 + ν.2 * ↑z.2 < 0 → x z = y z

Lemma 3.1 (lem:halfplane-pair) for a nonperiodic configuration with arbitrary finite range, together with the language inheritance of Section 1.1. Compactness is applied to the range subtype with its discrete topology.