Full shift and cellular automata

AbbreviationFull shift space#✓fully proved

For \(N \in \mathbb{N}\), the configuration space of the two-sided full shift on \(N\) symbols is the set \(\{0, \dots, N-1\}^{\mathbb{Z}}\) of all bi-infinite sequences \(x = (x_i)_{i \in \mathbb{Z}}\) of symbols. It carries the product of the discrete topologies.

abbrev FullShiftSpace (N : ℕ) := ℤ → Fin N

Used by 11

Used byShift on the aperiodic part of the full 2-shift · Shift on the aperiodic part of the 3-colouring shift · The full 2-shift · The full 3-shift · Automorphism group of the full shift · One-dimensional cellular automaton · Joint periodic count · Joint periodic growth rate · Jointly periodic points · The unit shift as a homeomorphism · Unit shift

DefinitionUnit shift#✓fully proved

The unit shift on the full shift on \(N\) symbols is the map \(\sigma\) from \(\{0, \dots, N-1\}^{\mathbb{Z}}\) to itself given by \((\sigma x)_i = x_{i+1}\) for all \(i \in \mathbb{Z}\), the left translation by one step.

def unitShift (N : ℕ) : FullShiftSpace N → FullShiftSpace N :=
  shift (A := Fin N) (1 : ℤ)

Uses 1 · Used by 8

Statement usesFull shift space

Used byAperiodic part of the full 2-shift · Aperiodic part of the 3-colouring shift · Shift on the aperiodic part of the full 2-shift · Shift on the aperiodic part of the 3-colouring shift · One-dimensional cellular automaton · Joint periodic count · Jointly periodic points · The unit shift as a homeomorphism

DefinitionThe unit shift as a homeomorphism#✓fully proved

The unit shift \(\sigma\) of the full shift on \(N\) symbols, given by \((\sigma x)_i = x_{i+1}\), is a homeomorphism of \(\{0, \dots, N-1\}^{\mathbb{Z}}\) onto itself, with inverse given by \((\sigma^{-1} x)_i = x_{i-1}\).

def shiftHomeomorph (N : ℕ) : FullShiftSpace N ≃ₜ FullShiftSpace N where
  toFun := unitShift N
  invFun := shift (A := Fin N) (-1 : ℤ)
  left_inv x := by
    change shift (-1) (shift 1 x) = x
    rw [← shift_add]
    simp
  right_inv x := by
    change shift 1 (shift (-1) x) = x
    rw [← shift_add]
    simp
  continuous_toFun := continuous_shift 1
  continuous_invFun := continuous_shift (-1)

Uses 2 · Used by 3

Statement usesFull shift space · Unit shift

Used byShift on the aperiodic part of the full 2-shift · Shift on the aperiodic part of the 3-colouring shift · Automorphism group of the full shift

DefinitionAutomorphism group of the full shift#✓fully proved

The automorphism group of the full shift on \(N\) symbols is the subgroup of the group of homeomorphisms of \(\{0, \dots, N-1\}^{\mathbb{Z}}\) onto itself consisting of the homeomorphisms \(\varphi\) that commute with the unit shift \(\sigma\), given by \((\sigma x)_i = x_{i+1}\), that is, \(\varphi \circ \sigma = \sigma \circ \varphi\).

def automorphismGroup (N : ℕ) : Subgroup (FullShiftSpace N ≃ₜ FullShiftSpace N) :=
  Subgroup.centralizer {shiftHomeomorph N}

Uses 2

Statement usesFull shift space · The unit shift as a homeomorphism

DefinitionOne-dimensional cellular automaton#✓fully proved

A map \(f\) from the full shift \(\{0, \dots, N-1\}^{\mathbb{Z}}\) on \(N\) symbols to itself is a one-dimensional cellular automaton if \(f\) is continuous and commutes with the unit shift \(\sigma\), given by \((\sigma x)_i = x_{i+1}\), that is, \(f \circ \sigma = \sigma \circ f\).

This is the Curtis–Hedlund–Lyndon characterization of cellular automata.

def IsOneDimensionalCA (N : ℕ) (f : FullShiftSpace N → FullShiftSpace N) : Prop :=
  Continuous f ∧ Function.Commute f (unitShift N)

Uses 2

Statement usesFull shift space · Unit shift

DefinitionJointly periodic points#✓fully proved

For a map \(f\) from the full shift \(\{0, \dots, N-1\}^{\mathbb{Z}}\) on \(N\) symbols to itself, the jointly periodic points of \(f\) are the configurations \(x\) that are periodic for \(f\) and periodic for the unit shift \(\sigma\), given by \((\sigma x)_i = x_{i+1}\): there are \(m \ge 1\) and \(n \ge 1\) with \(f^m(x) = x\) and \(\sigma^n(x) = x\).

No common period for \(f\) and \(\sigma\) is required.

def jointlyPeriodicPoints (N : ℕ) (f : FullShiftSpace N → FullShiftSpace N) :
    Set (FullShiftSpace N) :=
  Function.periodicPts f ∩ Function.periodicPts (unitShift N)

Uses 2

Statement usesFull shift space · Unit shift

DefinitionJoint periodic count#✓fully proved

For \(k \in \mathbb{N}\) and a map \(f\) from the full shift \(\{0, \dots, N-1\}^{\mathbb{Z}}\) on \(N\) symbols to itself, \(P(f, k)\) is the number of configurations \(x\) with \(\sigma^k(x) = x\), where \(\sigma\) is the unit shift given by \((\sigma x)_i = x_{i+1}\), that are also periodic for \(f\), that is, \(f^n(x) = x\) for some \(n \ge 1\). Here \(k\) need not be the least period of \(x\) under \(\sigma\).

The count is the cardinality of a set, taken to be \(0\) when the set is infinite, which can happen only for \(k = 0\).

noncomputable def jointPeriodicCount (N : ℕ)
    (f : FullShiftSpace N → FullShiftSpace N) (k : ℕ) : ℕ :=
  Set.ncard {x | Function.IsPeriodicPt (unitShift N) k x ∧ x ∈ Function.periodicPts f}

Uses 2 · Used by 1

Statement usesFull shift space · Unit shift

Used byJoint periodic growth rate

DefinitionJoint periodic growth rate#✓fully proved

For a map \(f\) from the full shift \(S_N\) on \(N\) symbols to itself, the joint periodic growth rate is the real number

\[\nu(f, S_N) = \limsup_{k \to \infty} P(f, k)^{1/k},\]

where \(k\) ranges over the positive integers and \(P(f, k)\) is the joint periodic count: the number of configurations fixed by the \(k\)-th power of the unit shift that are also periodic for \(f\).

noncomputable def jointPeriodicGrowthRate (N : ℕ)
    (f : FullShiftSpace N → FullShiftSpace N) : ℝ :=
  Filter.limsup
    (fun k : ℕ =>
      Real.rpow (jointPeriodicCount N f (k + 1) : ℝ) (((k + 1 : ℕ) : ℝ)⁻¹))
    Filter.atTop

Uses 2

Statement usesFull shift space · Joint periodic count

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.