The finite description of whole-strip states

Lemma 5.6 (lem:strip-states) of paper/nivat.tex. The differences of transverse translates have a horizontal period, so finitely many coordinates distinguish their restrictions to an infinite strip. A deterministic predecessor gives a transverse period. Otherwise the greatest disagreeing row positions an agreeing strip immediately above a disagreement.

def Nivat.TwoFactors.Strip (W : ℕ) : Set Lattice

The infinite horizontal strip consisting of all sites on rows 1 through W. Lemma 5.6 (lem:strip-states).

Equations

• Nivat.TwoFactors.Strip W = {z : Nivat.Lattice | 1 ≤ z.2 ∧ z.2 ≤ ↑W}

def Nivat.TwoFactors.stripState {A : Type u_1} (c : Configuration A) (W : ℕ) (t : Lattice) (n : ℤ) : ↑(Strip W) → A

The restriction of the nth transverse translate to the whole infinite strip. Lemma 5.6 (lem:strip-states).

Equations

• Nivat.TwoFactors.stripState c W t n z = Nivat.shift (n • t) c ↑z

theorem Nivat.TwoFactors.translate_difference_periodic {A : Type u_1} [AddCommGroup A] (c : Configuration A) (h t : Lattice) (hmix : difference h (difference t c) = 0) (m n : ℤ) : IsPeriod (shift (m • t) c - shift (n • t) c) h

A mixed-difference identity makes the difference of any two integer transverse translates periodic in the first direction. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.strip_eq_of_finite_test {A : Type u_1} [AddCommGroup A] (x y : Configuration A) (q W : ℕ) (hq : 0 < q) (hdiff : IsPeriod (x - y) (↑q, 0)) (htest : ∀ (i j : ℤ), 0 ≤ i → i < ↑q → 1 ≤ j → j ≤ ↑W → x (i, j) = y (i, j)) (z : Lattice) : 1 ≤ z.2 → z.2 ≤ ↑W → x z = y z

When a strip difference has horizontal period q, equality on q consecutive sites of every row implies equality on the entire strip. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.finite_stripState_range {A : Type u_1} [AddCommGroup A] (c : Configuration A) (hc : FiniteRange c) (q W : ℕ) (hq : 0 < q) (t : Lattice) (hmix : difference (↑q, 0) (difference t c) = 0) : (Set.range (stripState c W t)).Finite

Only finitely many whole-strip states occur: restriction to q * W sites is injective on them because their pairwise differences have horizontal period q. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.exists_transverse_strip_representative (a M : ℤ) (hM : 0 < M) (z : Lattice) : ∃ (n : ℤ) (w : Lattice), 1 ≤ w.2 ∧ w.2 ≤ M ∧ z = w + n • (a, M)

Every lattice site can be moved by an integer multiple of (a,M) into rows 1 through M; arbitrary horizontal shear is allowed. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.global_period_of_stripState_period {A : Type u_1} (c : Configuration A) (W : ℕ) (a M : ℤ) (hM : 0 < M) (hMW : M ≤ ↑W) (p : ℕ) (hper : Function.Periodic (stripState c W (a, M)) ↑p) : IsPeriod c (p • (a, M))

A period of the bilateral strip-state sequence gives a global multiple of the transverse direction, since a strip at least M rows wide meets every transverse orbit. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.shift_at_greatest_disagreement {A : Type u_1} (x y : Configuration A) (W : ℕ) (b : ℤ) (hagree : ∀ (z : Lattice), 1 ≤ z.2 → z.2 ≤ ↑W → x z = y z) (hne : ∃ (i : ℤ) (s : ℤ), b ≤ s ∧ s ≤ 0 ∧ x (i, s) ≠ y (i, s)) : ∃ (s : ℤ), b ≤ s ∧ s ≤ 0 ∧ (∀ (z : Lattice), 1 ≤ z.2 → z.2 ≤ ↑W → shift (0, s) x z = shift (0, s) y z) ∧ ∃ (i : ℤ), shift (0, s) x (i, 0) ≠ shift (0, s) y (i, 0)

Translating the greatest nonpositive disagreement row to row zero places a full agreeing strip directly above a disagreement. Lemma 5.6 (lem:strip-states).

theorem Nivat.TwoFactors.finite_strip_dichotomy {A : Type u_1} [AddCommGroup A] (c : Configuration A) (hc : FiniteRange c) (q W : ℕ) (hq : 0 < q) (a M : ℤ) (hM : 0 < M) (hMW : M ≤ ↑W) (hmix : difference (↑q, 0) (difference (a, M) c) = 0) : (∃ (p : ℕ), 0 < p ∧ IsPeriod c (p • (a, M))) ∨ ∃ (u : Lattice) (v : Lattice), (∀ (z : Lattice), 1 ≤ z.2 → z.2 ≤ ↑W → shift u c z = shift v c z) ∧ (∃ (i : ℤ), shift u c (i, 0) ≠ shift v c (i, 0)) ∧ IsPeriod (shift u c - shift v c) (↑q, 0) ∧ ∃ (k : ℤ), v - u = k • (a, M)

Either a positive integer multiple of the transverse step is a global period, or two translates agree on the whole strip, disagree on its lower boundary, and have a horizontally periodic difference. Their relative translation remains an integer multiple of the transverse step. Lemma 5.6 (lem:strip-states).