Finite states, word complexity, and periodic forcing

Section 5.1 of paper/nivat.tex: Lemma 5.2 (lem:finite-states), Corollary 5.3 (cor:morse), and Lemma 5.4 (lem:forcing). Bilaterality makes the deterministic successor map on occurring states a permutation. A complexity plateau supplies a finite-state presentation of a word; a periodic parameter is handled by recording its phase together with the finite memory.

theorem Nivat.TwoFactors.periodic_of_deterministic_successor_bounded {A : Type u_1} (s : ℤ → A) (hs : (Set.range s).Finite) (hdet : ∀ (i j : ℤ), s i = s j → s (i + 1) = s (j + 1)) : ∃ (p : ℕ), 0 < p ∧ p ≤ (Set.range s).ncard ∧ Function.Periodic s ↑p

A finite-range bilateral sequence with a uniquely determined successor has a positive period bounded by its number of occurring states. Bilaterality makes the successor map surjective on those states. Lemma 5.2 (lem:finite-states).

theorem Nivat.TwoFactors.periodic_of_deterministic_successor {A : Type u_1} (s : ℤ → A) (hs : (Set.range s).Finite) (hdet : ∀ (i j : ℤ), s i = s j → s (i + 1) = s (j + 1)) : ∃ (p : ℕ), 0 < p ∧ Function.Periodic s ↑p

A finite-range bilateral sequence whose next state is determined by its current state has a positive period. Lemma 5.2 (lem:finite-states).

theorem Nivat.TwoFactors.periodic_of_deterministic_predecessor_bounded {A : Type u_1} (s : ℤ → A) (hs : (Set.range s).Finite) (hdet : ∀ (i j : ℤ), s i = s j → s (i - 1) = s (j - 1)) : ∃ (p : ℕ), 0 < p ∧ p ≤ (Set.range s).ncard ∧ Function.Periodic s ↑p

A uniquely determined predecessor gives a positive period bounded by the number of occurring states, by reversing the integer index. Lemma 5.2 (lem:finite-states).

theorem Nivat.TwoFactors.periodic_of_deterministic_predecessor {A : Type u_1} (s : ℤ → A) (hs : (Set.range s).Finite) (hdet : ∀ (i j : ℤ), s i = s j → s (i - 1) = s (j - 1)) : ∃ (p : ℕ), 0 < p ∧ Function.Periodic s ↑p

A finite-range bilateral sequence with a uniquely determined predecessor is periodic; this is the form applied to strip states. Lemma 5.2 (lem:finite-states).

theorem Nivat.TwoFactors.periodic_eq_of_emod_eq {F : Type u_1} (f : ℤ → F) (p : ℤ) (hf : Function.Periodic f p) {i j : ℤ} (h : i % p = j % p) : f i = f j

Equal residues modulo a period give equal parameter values, so the residue class records all the forcing information needed in a finite state. Lemma 5.4 (lem:forcing).

theorem Nivat.TwoFactors.periodic_of_periodic_forcing {A : Type u_1} {F : Type u_2} (a : ℤ → A) (f : ℤ → F) (ha : (Set.range a).Finite) (p k : ℕ) (hp : 0 < p) (hf : Function.Periodic f ↑p) (hrule : ∀ (i j : ℤ), f i = f j → (∀ (r : Fin k), a (i + ↑↑r) = a (j + ↑↑r)) → a (i + ↑k) = a (j + ↑k)) : ∃ (q : ℕ), 0 < q ∧ Function.Periodic a ↑q

A finite-range word with a periodic parameter and a uniquely determined next letter from its occurring memory data has a positive period. The state contains the phase and k + 1 letters, including when k = 0. Lemma 5.4 (lem:forcing).

def Nivat.TwoFactors.word {A : Type u_1} (a : ℤ → A) (k : ℕ) (i : ℤ) : Fin k → A

The length-k word beginning at an arbitrary integer index of a bilateral sequence. Corollary 5.3 (cor:morse).

Equations

• Nivat.TwoFactors.word a k i r = a (i + ↑↑r)

noncomputable def Nivat.TwoFactors.wordComplexity {A : Type u_1} (a : ℤ → A) (k : ℕ) : ℕ

The number of distinct length-k words over all integer starting indices; finite range ensures that the counted set is finite. Corollary 5.3 (cor:morse).

Equations

• Nivat.TwoFactors.wordComplexity a k = (Set.range (Nivat.TwoFactors.word a k)).ncard

theorem Nivat.TwoFactors.finite_word_range {A : Type u_1} (a : ℤ → A) (ha : (Set.range a).Finite) (k : ℕ) : (Set.range (word a k)).Finite

A finite alphabet gives only finitely many occurring words of any fixed finite length. Corollary 5.3 (cor:morse).

@[simp]

theorem Nivat.TwoFactors.wordComplexity_zero {A : Type u_1} (a : ℤ → A) : wordComplexity a 0 = 1

There is exactly one empty word, providing the initial value p(0) = 1 in the plateau argument. Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.word_restriction_image {A : Type u_1} (a : ℤ → A) {m n : ℕ} (hmn : m ≤ n) : (fun (b : Fin n → A) (r : Fin m) => b ⟨↑r, ⋯⟩) '' Set.range (word a n) = Set.range (word a m)

Taking the initial subword maps the occurring longer words onto all occurring shorter words. Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.wordComplexity_mono {A : Type u_1} (a : ℤ → A) (ha : (Set.range a).Finite) : Monotone (wordComplexity a)

Word complexity is nondecreasing with word length because initial restriction is surjective. Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.exists_wordComplexity_plateau {A : Type u_1} (a : ℤ → A) (ha : (Set.range a).Finite) (k : ℕ) (_hk : 0 < k) (hbound : wordComplexity a k ≤ k) : ∃ j < k, wordComplexity a (j + 1) = wordComplexity a j

If length-k complexity is at most k, one of the first k increases is zero, since empty-word complexity is one. Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.word_extension_unique_of_complexity_eq {A : Type u_1} (a : ℤ → A) (ha : (Set.range a).Finite) (k : ℕ) (heq : wordComplexity a (k + 1) = wordComplexity a k) (i j : ℤ) : word a k i = word a k j → word a (k + 1) i = word a (k + 1) j

At a complexity plateau, initial restriction is bijective on occurring words, so a word determines its following letter. Corollary 5.3 (cor:morse).

theorem Nivat.TwoFactors.morse_hedlund {A : Type u_1} (a : ℤ → A) (ha : (Set.range a).Finite) (k : ℕ) (hk : 0 < k) (hbound : wordComplexity a k ≤ k) : ∃ (p : ℕ), 0 < p ∧ p ≤ k ∧ Function.Periodic a ↑p

A bilateral finite-range word with at most k length-k words has a positive period at most k. The states at a plateau use one extra letter so projection to the original word also covers a plateau at zero. Corollary 5.3 (cor:morse).