Ambiguous boundaries and a common interior period

Lemma 5.7 (lem:periodic-interior) of paper/nivat.tex. A forward boundary rule propagates agreement to a right half-line. Periodicity of the difference then rules out agreement on any complete boundary edge. Counting the resulting ambiguous extensions bounds the complexity of a word whose letters collect all the interior rows; Morse–Hedlund gives one period for those rows.

theorem Nivat.TwoFactors.agreement_extends_right {A : Type u_1} (a b : ℤ → A) (k e : ℕ) (hke : k < e) (hrule : ∀ (i : ℤ), (∀ (r : Fin k), a (i + ↑↑r) = b (i + ↑↑r)) → a (i + ↑k) = b (i + ↑k)) (i : ℤ) (hinit : ∀ (r : Fin e), a (i + ↑↑r) = b (i + ↑↑r)) (n : ℕ) : a (i + ↑n) = b (i + ↑n)

An agreeing boundary block extends indefinitely to the right when the next value is determined by the preceding k agreeing letters. Lemma 5.7 (lem:periodic-interior).

theorem Nivat.TwoFactors.periodic_zero_of_right_ray {G : Type u_1} [AddGroup G] (d : ℤ → G) (q : ℕ) (hq : 0 < q) (hp : Function.Periodic d ↑q) (i : ℤ) (hz : ∀ (n : ℕ), d (i + ↑n) = 0) (j : ℤ) : d j = 0

A periodic difference that vanishes on a right half-line vanishes at every integer index. Lemma 5.7 (lem:periodic-interior).

theorem Nivat.TwoFactors.boundaryRule_shift {A : Type u_1} (c : Configuration A) (C : Finset Lattice) (k : ℕ) (hr : BoundaryRule c C k) (u : Lattice) : BoundaryRule (shift u c) C k

The occurring-pattern boundary rule holds for every translate of the configuration, because translating both test positions preserves the rule. Lemma 5.8 (lem:row-lifting).

theorem Nivat.TwoFactors.every_edge_differs (c : Configuration ℚ) (C : Finset Lattice) (k e q : ℕ) (hke : k < e) (hq : 0 < q) (hrule : BoundaryRule c C k) (u v : Lattice) (hinner : ∀ (i : ℤ), patternAt (shift u c) C (i, 0) = patternAt (shift v c) C (i, 0)) (hperiod : IsPeriod (shift u c - shift v c) (↑q, 0)) (hne : ∃ (i : ℤ), shift u c (i, 0) ≠ shift v c (i, 0)) (i : ℤ) : patternAt (shift u c) (rowPrefix e) (i, 0) ≠ patternAt (shift v c) (rowPrefix e) (i, 0)

Two translates with agreeing interiors and a nonzero periodic boundary difference cannot agree on any complete translated boundary edge: agreement would propagate to a half-line and then to the whole boundary. Lemma 5.7 (lem:periodic-interior).

def Nivat.TwoFactors.innerOrbit {A : Type u_1} (x : Configuration A) (C : Finset Lattice) : Set (↥C → A)

The interior patterns encountered by translating one configuration in the horizontal basis direction. Lemma 5.7 (lem:periodic-interior).

Equations

• Nivat.TwoFactors.innerOrbit x C = Set.range fun (i : ℤ) => Nivat.patternAt x C (i, 0)

theorem Nivat.TwoFactors.innerOrbit_finite {A : Type u_1} {x : Configuration A} (hx : FiniteRange x) (C : Finset Lattice) : (innerOrbit x C).Finite

The horizontal interior orbit is finite because it is a subset of the patterns of a finite-range configuration on a finite window. Lemma 5.7 (lem:periodic-interior).

theorem Nivat.TwoFactors.innerOrbit_budget {A : Type u_1} (c : Configuration A) (hc : FiniteRange c) (C : Finset Lattice) (e : ℕ) (u v : Lattice) (hinner : ∀ (i : ℤ), patternAt (shift u c) C (i, 0) = patternAt (shift v c) C (i, 0)) (hedge : ∀ (i : ℤ), patternAt (shift u c) (rowPrefix e) (i, 0) ≠ patternAt (shift v c) (rowPrefix e) (i, 0)) : (innerOrbit (shift u c) C).ncard + complexity c C ≤ complexity c (prefixWindow C e)

When every horizontally translated edge differs but the interiors agree, each encountered interior pattern has two boundary extensions, so their number is bounded by the total boundary cost. Lemma 5.7 (lem:periodic-interior).

theorem Nivat.TwoFactors.common_inner_period {A : Type u_1} (x : Configuration A) (hx : FiniteRange x) (C : Finset Lattice) (H r : ℕ) (hr : 0 < r) (α : Fin H → ℤ) (hblocks : ∀ (j : Fin H) (t : Fin r), (α j + ↑↑t, ↑↑j + 1) ∈ C) (hcount : (innerOrbit x C).ncard ≤ r) : ∃ (p : ℕ), 0 < p ∧ p ≤ r ∧ ∀ (j : Fin H), Function.Periodic (fun (i : ℤ) => x (i, ↑↑j + 1)) ↑p

Collecting one staggered coordinate from each interior row gives a finite-alphabet word whose length-r complexity is at most r; Morse–Hedlund supplies one period for every entire interior row. Lemma 5.7 (lem:periodic-interior).