Symbolic dynamics on cancellative monoids

This file develops a minimal API for symbolic dynamics over a left-cancellative monoid G—formally, a structure carrying [Monoid G] and [IsLeftCancelMul G] (which becomes [AddMonoid G] and [IsLeftCancelAdd G] in the additive form). Throughout the documentation we use the additive notations, which are the most common in symbolic dynamics, although all the notions introduced are defined in the multiplicative notations and adapted to the additive notation.

Given a finite alphabet A, the ambient configuration space is the set of functions G → A, endowed with the product topology. We define the left-translation action, cylinders, finite patterns, their occurrences, forbidden sets, and subshifts (closed, shift-invariant subsets). Basic topological facts (e.g. cylinders are clopen, occurrence sets are clopen, forbidden sets are closed) are proved under discreteness assumptions on the alphabet.

The development is generic for left-cancellative monoids. This covers both groups (the standard setting of symbolic dynamics) and more general monoids where cancellation holds but inverses may not exist. Geometry specific to ℤ^d (boxes/cubes and the box-based entropy) is deferred to a separate specialization.

Why cancellativity?

Some constructions, such as translating a finite pattern to occur at a point v, require solving equations of the form w + v = h. For this to have a unique solution w given h and v, we assume left-cancellation: if v + a = v + b then a = b. This allows us to define Pattern.shift (which shifts a pattern) without using inverses, so that the theory works not only for groups but also for cancellative monoids.

Main definitions

• shift g x — left translation: in additive notation (shift v x) u = x (v + u) (using the left action of G on configurations).
• cylinder U x — configurations agreeing with x on a finite set U ⊆ G.
• Pattern A G — a configuration which takes default value outside of a finite support, together with this support.
• Pattern.occursInAt p x g — occurrence of p in x at translate g.
• forbidden F — configurations avoiding every pattern in F.
• Subshift A G — closed, shift-invariant subsets of the full shift.
• MulSubshift.ofForbidden F — the subshift defined by forbidding a family of patterns.
• subshift_of_finite_type F — a subshift of finite type defined by a finite set of forbidden patterns.
• languageOn X U — the set of patterns of shape U obtained by restricting some x ∈ X.

Design choice: ambient vs. inner (subshift-relative) viewpoint

All core notions (shift, cylinder, occurrence, language, …) are defined in the ambient full shift G → A. A subshift is then a closed, invariant subset, bundled as Subshift A G. Working inside a subshift is done by restriction.

Motivation.

If cylinders and shifts were defined only inside a subshift, local ergonomics would improve but global operations would become awkward. For instance, to prove that for finite shape U:

languageOn (X ∪ Y) U = languageOn X U ∪ languageOn Y U,

one must eventually move both sides to the ambient pattern type. Similar issues arise for intersections, factors, and products. By contrast, with ambient definitions these set-theoretic identities are tautological. Thus the file develops the theory ambiently, and subshifts reuse it by restriction.

Working inside a subshift.

For Y : Subshift A G, cylinders and occurrence sets inside Y are simply preimages of the ambient ones under the inclusion Y → (G → A). For example:

{ y : Y | ∀ i ∈ U, (y : G → A) i = (x : G → A) i } = (Subtype.val) ⁻¹' (cylinder U (x : G → A)).

Shift invariance guarantees that the ambient shift restricts to Y.

Ergonomics.

Thin wrappers (e.g. Subshift.shift, Subshift.cylinder, Subshift.languageOn) may be added for convenience. They introduce no new theory and unfold to the ambient definitions.

Namespacing policy

All ambient definitions live under the namespace SymbolicDynamics.FullShift. If inner, subshift-relative wrappers are provided, they will be placed in the subnamespace SymbolicDynamics.Subshift. This separation avoids name clashes between the two viewpoints, since both may naturally want to reuse names like cylinder, shift, occursAt, or languageOn.

Implementation notes

• Openness results for cylinders and occurrence sets use [DiscreteTopology A]. Closeness results use [T1Space A].

Full shift and shift action

def SymbolicDynamics.FullShift.mulShift {A : Type u_1} {G : Type u_2} [Monoid G] (g : G) (x : G → A) : G → A

The left-translation shift on configurations.

We call configuration an element of G → A.

Given a configuration x : G → A and an element g : G of the monoid, the shifted configuration mulShift g x is defined by (mulShift g x) h = x (g * h).

Intuitively, this moves the whole configuration "in the direction of g": the value at position h in the shifted configuration is the value that was at position g * h in the original one.

For example, if G = ℤ (with addition) and A = {0, 1}, then mulShift 1 x is the sequence obtained from x by shifting every symbol one step to the left.

Equations

• SymbolicDynamics.FullShift.mulShift g x h = x (g * h)

def SymbolicDynamics.FullShift.shift {A : Type u_1} {G : Type u_2} [AddMonoid G] (g : G) (x : G → A) : G → A

The left-translation shift on configurations, in additive notation.

We call configuration an element of G → A.

Given a configuration x : G → A and an element g : G of the additive monoid, the shifted configuration shift g x is defined by (shift g x) h = x (g + h).

Intuitively, this moves the whole configuration "in the direction of g": the value at position h in the shifted configuration is the value that was at position g + h in the original one.

For example, if G = ℤ and A = {0, 1}, then shift 1 x is the sequence obtained from x by shifting every symbol one step to the left.

Equations

• SymbolicDynamics.FullShift.shift g x h = x (g + h)

@[simp]

theorem SymbolicDynamics.FullShift.mulShift_apply {A : Type u_1} {G : Type u_2} [Monoid G] (g : G) (x : G → A) (h : G) : mulShift g x h = x (g * h)

@[simp]

theorem SymbolicDynamics.FullShift.shift_apply {A : Type u_1} {G : Type u_2} [AddMonoid G] (g : G) (x : G → A) (h : G) : shift g x h = x (g + h)

@[simp]

theorem SymbolicDynamics.FullShift.mulShift_one {A : Type u_1} {G : Type u_2} [Monoid G] (x : G → A) : mulShift 1 x = x

@[simp]

theorem SymbolicDynamics.FullShift.shift_zero {A : Type u_1} {G : Type u_2} [AddMonoid G] (x : G → A) : shift 0 x = x

theorem SymbolicDynamics.FullShift.mulShift_mul {A : Type u_1} {G : Type u_2} [Monoid G] (g₁ g₂ : G) (x : G → A) : mulShift (g₁ * g₂) x = mulShift g₂ (mulShift g₁ x)

Composition of left-translation shifts corresponds to multiplication in the monoid G.

theorem SymbolicDynamics.FullShift.shift_add {A : Type u_1} {G : Type u_2} [AddMonoid G] (g₁ g₂ : G) (x : G → A) : shift (g₁ + g₂) x = shift g₂ (shift g₁ x)

theorem SymbolicDynamics.FullShift.continuous_mulShift {A : Type u_1} {G : Type u_2} [Monoid G] [TopologicalSpace A] (g : G) : Continuous (mulShift g)

The left-translation shift is continuous.

theorem SymbolicDynamics.FullShift.continuous_shift {A : Type u_1} {G : Type u_2} [AddMonoid G] [TopologicalSpace A] (g : G) : Continuous (shift g)

Cylinders

def SymbolicDynamics.FullShift.cylinder {A : Type u_1} {G : Type u_2} (U : Finset G) (x : G → A) : Set (G → A)

A cylinder set is the set of all configurations that agree with a given reference configuration x on a fixed finite subset U of the index set G.

The set U is called the support of the cylinder.

Intuitively, cylinders specify the "letters" on finitely many coordinates, while leaving all other coordinates free. For example, in the full shift {0, 1}^ℤ, the cylinder determined by U = {0, 1} and x 0 = 1, x 1 = 0 consists of all bi-infinite sequences of 0s and 1s whose entries on positions 0 and 1 respectively are 1 and 0.

When A has the discrete topology, cylinder sets form a basis of clopen sets for the product topology on G → A.

Equations

• SymbolicDynamics.FullShift.cylinder U x = {y : G → A | ∀ i ∈ U, y i = x i}

theorem SymbolicDynamics.FullShift.cylinder_eq_set_pi {A : Type u_1} {G : Type u_2} (U : Finset G) (x : G → A) : cylinder U x = (↑U).pi fun (i : G) => {x i}

A cylinder set on U is the Set.pi over U of the singletons {x i}, viewed as a subset of G → A. Equivalently, it is the preimage of that product of singletons in U → A under the restriction map (G → A) → (U → A).

theorem SymbolicDynamics.FullShift.mem_cylinder {A : Type u_1} {G : Type u_2} {U : Finset G} {x y : G → A} : y ∈ cylinder U x ↔ ∀ i ∈ U, y i = x i

theorem SymbolicDynamics.FullShift.isOpen_cylinder {A : Type u_1} {G : Type u_2} [TopologicalSpace A] [DiscreteTopology A] (U : Finset G) (x : G → A) : IsOpen (cylinder U x)

Cylinders are open when A is discrete.

theorem SymbolicDynamics.FullShift.isClosed_cylinder {A : Type u_1} {G : Type u_2} [TopologicalSpace A] [T1Space A] (U : Finset G) (x : G → A) : IsClosed (cylinder U x)

Cylinders are closed when A is a T1 Space.

Patterns and occurrences

structure SymbolicDynamics.FullShift.Subshift (A : Type u_1) [TopologicalSpace A] (G : Type u_2) [AddMonoid G] : Type (max u_1 u_2)

A subshift on an alphabet A is a closed, shift-invariant subset of G → A. Formally, it is composed of:

• carrier: the underlying set of allowed configurations.
• isClosed: the set is topologically closed in A^G.
• mapsTo: the set is invariant under all left-translation shifts (shift g).

• carrier : Set (G → A)

  The underlying set of configurations (additive monoid version).

• isClosed : IsClosed self.carrier

  Closedness of carrier.

• mapsTo (g : G) : Set.MapsTo (shift g) self.carrier self.carrier

  Shift invariance of carrier for the additive shift shift.

structure SymbolicDynamics.FullShift.MulSubshift (A : Type u_1) [TopologicalSpace A] (G : Type u_2) [Monoid G] : Type (max u_1 u_2)

A subshift on an alphabet A over a multiplicative monoid G is a closed, shift-invariant subset of G → A, where the shift is given by left-multiplication. Formally, it is composed of:

• carrier: the underlying set of allowed configurations.
• isClosed: the set is topologically closed in A^G.
• mapsTo: the set is invariant under all left-translation shifts (mulShift g).

• carrier : Set (G → A)

  The underlying set of configurations.

• isClosed : IsClosed self.carrier

  Closedness of carrier.

• mapsTo (g : G) : Set.MapsTo (mulShift g) self.carrier self.carrier

  Shift invariance of carrier.

def SymbolicDynamics.FullShift.mulFullShift (A : Type u_1) (G : Type u_2) [TopologicalSpace A] [Monoid G] : MulSubshift A G

Example: the full shift on alphabet A over the multiplicative monoid G. It is the subshift whose underlying set is the set of all configurations G → A.

Equations

• SymbolicDynamics.FullShift.mulFullShift A G = { carrier := Set.univ, isClosed := ⋯, mapsTo := ⋯ }

def SymbolicDynamics.FullShift.fullShift (A : Type u_1) (G : Type u_2) [TopologicalSpace A] [AddMonoid G] : Subshift A G

Example: the full shift on alphabet A over the additive monoid G.

It is the subshift whose underlying set is the set of all configurations G → A.

Equations

• SymbolicDynamics.FullShift.fullShift A G = { carrier := Set.univ, isClosed := ⋯, mapsTo := ⋯ }

structure SymbolicDynamics.FullShift.Pattern (A : Type u_1) (G : Type u_2) [Inhabited A] : Type (max u_1 u_2)

A pattern is a finite configuration in the full shift A^G.

It consists of:

• a full configuration config : G → A in the full shift;
• a finite subset support : Finset G of coordinates, called the support of p;
• a proof condition that outside support, config takes the default value of A.

Intuitively, a pattern is a "partial configuration" specifying finitely many values of a configuration in G → A (the rest being default). Patterns are the basic building blocks used to define subshifts via forbidden configurations. Note that each pattern corresponds to a cylinder, which is the set of configurations which agree with this pattern on its support.

• config : G → A

  The full configuration in the full shift A^G.

• support : Finset G

  Finite support of the pattern.

• condition (g : G) : g ∉ self.support → self.config g = default

  Outside the support, config takes the default value of A.

def SymbolicDynamics.FullShift.Pattern.mulOccursInAt {A : Type u_1} {G : Type u_2} [Inhabited A] [Monoid G] (p : Pattern A G) (x : G → A) (g : G) : Prop

p.mulOccursInAt x g means that the finite pattern p appears in the configuration x at position g.

Formally: for every position h in the support of p, the value of the configuration at g * h coincides with the value of p.config at h.

Intuitively, if you shift the configuration x by g (using mulShift g), then on the support of p you exactly recover the pattern p. This is the basic notion of "pattern occurrence" used to define subshifts via forbidden patterns.

Equations

• p.mulOccursInAt x g = ∀ h ∈ p.support, x (g * h) = p.config h

def SymbolicDynamics.FullShift.Pattern.occursInAt {A : Type u_1} {G : Type u_2} [Inhabited A] [AddMonoid G] (p : Pattern A G) (x : G → A) (g : G) : Prop

p.occursInAt x g means that the finite pattern p appears in the configuration x at position g.

Formally: for every position h in the support of p, the value of the configuration at g + h coincides with the value of p.config at h.

Intuitively, if you shift the configuration x by g (using shift g), then on the support of p you exactly recover the pattern p. This is the basic notion of "pattern occurrence" used to define subshifts via forbidden patterns.

Equations

• p.occursInAt x g = ∀ h ∈ p.support, x (g + h) = p.config h

def SymbolicDynamics.FullShift.mulForbidden {A : Type u_1} {G : Type u_2} [Inhabited A] [Monoid G] (F : Set (Pattern A G)) : Set (G → A)

mulForbidden F is the set of configurations that avoid every pattern in F.

Formally: x ∈ mulForbidden F if and only if for every pattern p ∈ F and every monoid element g : G, the pattern p does not occur in x at position g.

Intuitively, mulForbidden F is the shift space defined by declaring the finite set (or family) of patterns F to be forbidden. A configuration belongs to the subshift if and only it avoids all the forbidden patterns.

Equations

• SymbolicDynamics.FullShift.mulForbidden F = {x : G → A | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}

def SymbolicDynamics.FullShift.forbidden {A : Type u_1} {G : Type u_2} [Inhabited A] [AddMonoid G] (F : Set (Pattern A G)) : Set (G → A)

forbidden F is the set of configurations that avoid every pattern in F.

Formally: x ∈ forbidden F if and only if for every pattern p ∈ F and every monoid element g : G, the pattern p does not occur in x at position g.

Intuitively, forbidden F is the shift space defined by declaring the finite set (or family) of patterns F to be forbidden. A configuration belongs to the subshift if and only it avoids all the forbidden patterns.

Equations

• SymbolicDynamics.FullShift.forbidden F = {x : G → A | ∀ p ∈ F, ∀ (g : G), ¬p.occursInAt x g}

noncomputable def SymbolicDynamics.FullShift.Pattern.mulShift {A : Type u_1} [Inhabited A] {G : Type u_2} [Monoid G] (p : Pattern A G) (v : G) : G → A

Translate a finite pattern p so that it occurs at the translate v, before completing into a configuration.

On input h : G, we proceed as follows:

• if h lies in the left-translate of the support, i.e. h ∈ p.support.image (v * ·), choose (noncomputably) w ∈ p.support with v * w = h and return p.config w;
• otherwise return default.

This definition does not assume left-cancellation; it only chooses a preimage. Uniqueness (and the usual equations such as Pattern.mulShift p v (v * w) = p.config w) require a left-cancellation hypothesis and are proved in separate lemmas.

Equations

• p.mulShift v h = if hmem : h ∈ Finset.image (fun (x : G) => v * x) p.support then have ex := ⋯; p.config (Classical.choose ex) else default

noncomputable def SymbolicDynamics.FullShift.Pattern.shift {A : Type u_1} [Inhabited A] {G : Type u_2} [AddMonoid G] (p : Pattern A G) (v : G) : G → A

Translate a finite pattern p so that it occurs at the translate v, before completing into a configuration.

On input h : G, we proceed as follows:

• if h lies in the left-translate of the support, i.e. h ∈ p.support.image (v + ·), choose (noncomputably) w ∈ p.support with v + w = h and return p.config w;
• otherwise return default.

This definition does not assume left-cancellation; it only chooses a preimage. Uniqueness (and the usual equations such as Pattern.shift p v (v + w) = p.config w) require a left-cancellation hypothesis and are proved in separate lemmas.

Equations

• p.shift v h = if hmem : h ∈ Finset.image (fun (x : G) => v + x) p.support then have ex := ⋯; p.config (Classical.choose ex) else default

noncomputable def SymbolicDynamics.FullShift.Pattern.fromConfig {A : Type u_1} [Inhabited A] {G : Type u_2} (x : G → A) (U : Finset G) : Pattern A G

Extract the finite pattern given by restricting a configuration x : G → A to a finite subset U : Finset G.

The pattern has config g = x g for g ∈ U and config g = default outside U, with support U. In other words, Pattern.fromConfig x U is the partial configuration of x visible on the coordinates in U, padded with default elsewhere.

Equations

• SymbolicDynamics.FullShift.Pattern.fromConfig x U = { config := fun (g : G) => if g ∈ U then x g else default, support := U, condition := ⋯ }

theorem SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem {A : Type u_1} [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] (p : Pattern A G) (v w : G) (hw : w ∈ p.support) : p.mulShift v (v * w) = p.config w

On the translated support, p.mulShift v agrees with p.config at the preimage.

More precisely, if w ∈ p.support, then at the translated site v * w, the configuration p.mulShift v takes the value p.config w.

This uses [IsLeftCancelMul G] to identify the unique preimage of v * w under left-multiplication by v.

theorem SymbolicDynamics.FullShift.Pattern.shift_apply_add_left_of_mem {A : Type u_1} [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] (p : Pattern A G) (v w : G) (hw : w ∈ p.support) : p.shift v (v + w) = p.config w

On the translated support, p.shift v agrees with p.config at the preimage.

More precisely, if w ∈ p.support, then at the translated site v + w, the configuration p.shift v takes the value p.config w.

This uses [IsLeftCancelAdd G] to identify the unique preimage of v + w under left-translation by v.

theorem SymbolicDynamics.FullShift.Pattern.mulOccursInAt_mulShift {A : Type u_3} {G : Type u_4} [Inhabited A] [Monoid G] (p : Pattern A G) (x : G → A) (g h : G) : p.mulOccursInAt (mulShift g x) h ↔ p.mulOccursInAt x (g * h)

Shifting a configuration commutes with occurrences of a pattern.

Formally: a pattern p occurs in the shifted configuration mulShift h x at position g if and only if it occurs in the original configuration x at position g * h.

theorem SymbolicDynamics.FullShift.Pattern.occursInAt_shift {A : Type u_3} {G : Type u_4} [Inhabited A] [AddMonoid G] (p : Pattern A G) (x : G → A) (g h : G) : p.occursInAt (shift g x) h ↔ p.occursInAt x (g + h)

Shifting a configuration commutes with occurrences of a pattern.

Formally: a pattern p occurs in the shifted configuration shift h x at position g if and only if it occurs in the original configuration x at position g + h.

theorem SymbolicDynamics.FullShift.Pattern.mapsTo_mulShift_mulForbidden {A : Type u_3} {G : Type u_4} [Inhabited A] [Monoid G] (F : Set (Pattern A G)) (h : G) : Set.MapsTo (mulShift h) (mulForbidden F) (mulForbidden F)

Configurations that avoid a family F of patterns are stable under the shift.

Formally: if x avoids every p ∈ F at every position, then for any h : G, the shifted configuration mulShift h x also avoids every p ∈ F at every position.

theorem SymbolicDynamics.FullShift.Pattern.mapsTo_shift_forbidden {A : Type u_3} {G : Type u_4} [Inhabited A] [AddMonoid G] (F : Set (Pattern A G)) (h : G) : Set.MapsTo (shift h) (forbidden F) (forbidden F)

Configurations that avoid a family F of patterns are stable under the shift.

Formally: if x avoids every p ∈ F at every position, then for any h : G, the shifted configuration shift h x also avoids every p ∈ F at every position.

theorem SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder {A : Type u_1} [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] (p : Pattern A G) (g : G) : {x : G → A | p.mulOccursInAt x g} = cylinder (Finset.image (fun (x : G) => g * x) p.support) (p.mulShift g)

We call occurrence set for pattern p and position g the set of configurations in which a pattern p occurs at position g.

This proves that it is exactly the cylinder corresponding to the pattern obtained by translating p by g.

Equivalently, p.mulOccursInAt x g iff on every translated site g * w (with w ∈ p.support) the configuration x agrees with the translated pattern Pattern.mulShift p g.

(This uses [IsLeftCancelMul G] to identify the preimage along left-multiplication by g.)

theorem SymbolicDynamics.FullShift.occursInAt_eq_cylinder {A : Type u_1} [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] (p : Pattern A G) (g : G) : {x : G → A | p.occursInAt x g} = cylinder (Finset.image (fun (x : G) => g + x) p.support) (p.shift g)

We call occurrence set for pattern p and position g the set of configurations in which a pattern p occurs at position g.

This proves that it is exactly the cylinder corresponding to the pattern obtained by translating p by g.

Equivalently, p.occursInAt x g iff on every translated site g + w (with w ∈ p.support) the configuration x agrees with the translated pattern Pattern.shift p g.

(This uses [IsLeftCancelMul G] to identify the preimage along left-multiplication by g.)

Forbidden sets and subshifts

theorem SymbolicDynamics.FullShift.isOpen_mulOccursInAt {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] [DiscreteTopology A] (p : Pattern A G) (g : G) : IsOpen {x : G → A | p.mulOccursInAt x g}

Occurrence sets are open.

theorem SymbolicDynamics.FullShift.isOpen_occursInAt {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] [DiscreteTopology A] (p : Pattern A G) (g : G) : IsOpen {x : G → A | p.occursInAt x g}

theorem SymbolicDynamics.FullShift.isClosed_mulForbidden {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] [DiscreteTopology A] (F : Set (Pattern A G)) : IsClosed (mulForbidden F)

Avoiding a fixed family of patterns is a closed condition (in the product topology on G → A).

Since each occurrence set { x | p.mulOccursInAt x v } is open (when A is discrete), its complement { x | ¬ p.mulOccursInAt x v } is closed; forbidden F is the intersection of these closed sets over p ∈ F and v ∈ G.

theorem SymbolicDynamics.FullShift.isClosed_forbidden {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] [DiscreteTopology A] (F : Set (Pattern A G)) : IsClosed (forbidden F)

Avoiding a fixed family of patterns is a closed condition (in the product topology on G → A).

Since each occurrence set { x | p.occursInAt x v } is open (when A is discrete), its complement { x | ¬ p.occursInAt x v } is closed; forbidden F is the intersection of these closed sets over p ∈ F and v ∈ G.

theorem SymbolicDynamics.FullShift.isClosed_mulOccursInAt {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] [T1Space A] (p : Pattern A G) (g : G) : IsClosed {x : G → A | p.mulOccursInAt x g}

Occurrence sets are closed.

theorem SymbolicDynamics.FullShift.isClosed_occursInAt {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] [T1Space A] (p : Pattern A G) (g : G) : IsClosed {x : G → A | p.occursInAt x g}

def SymbolicDynamics.FullShift.MulSubshift.ofForbidden {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [Monoid G] [IsLeftCancelMul G] [DiscreteTopology A] (F : Set (Pattern A G)) : MulSubshift A G

The subshift defined by a family of forbidden patterns F.

This is a standard way to construct subshifts: MulSubshift.ofForbidden F consists of all configurations x : G → A in which no pattern p ∈ F occurs at any position.

Formally:

• the carrier is forbidden F (configurations avoiding F),
• it is closed because each occurrence set is open, and
• it is shift-invariant since avoidance is preserved by shifts.

Equations

• SymbolicDynamics.FullShift.MulSubshift.ofForbidden F = { carrier := SymbolicDynamics.FullShift.mulForbidden F, isClosed := ⋯, mapsTo := ⋯ }

def SymbolicDynamics.FullShift.Subshift.ofForbidden {A : Type u_1} [TopologicalSpace A] [Inhabited A] {G : Type u_2} [AddMonoid G] [IsLeftCancelAdd G] [DiscreteTopology A] (F : Set (Pattern A G)) : Subshift A G

The subshift defined by a family of forbidden patterns F.

This is a standard way to construct subshifts: Subshift.ofForbidden F consists of all configurations x : G → A in which no pattern p ∈ F occurs at any position.

Formally:

• the carrier is forbidden F (configurations avoiding F),
• it is closed because each occurrence set is open, and
• it is shift-invariant since avoidance is preserved by shifts.

Equations

• SymbolicDynamics.FullShift.Subshift.ofForbidden F = { carrier := SymbolicDynamics.FullShift.forbidden F, isClosed := ⋯, mapsTo := ⋯ }

theorem SymbolicDynamics.FullShift.finite_setOf_pattern_support_eq {A : Type u_3} {G : Type u_4} [Finite A] [Inhabited A] (U : Finset G) : {p : Pattern A G | p.support = U}.Finite

Patterns with support exactly U form a finite set.

def SymbolicDynamics.FullShift.LanguageOn {A : Type u_1} [Inhabited A] {G : Type u_2} (X : Set (G → A)) (U : Finset G) : Set (Pattern A G)

The language of a set of configurations X on a finite shape U.

This is the set of all finite patterns obtained by restricting some configuration x ∈ X to U.

Equations

• SymbolicDynamics.FullShift.LanguageOn X U = {p : SymbolicDynamics.FullShift.Pattern A G | ∃ x ∈ X, SymbolicDynamics.FullShift.Pattern.fromConfig x U = p}

def SymbolicDynamics.FullShift.MulSubshift.languageOn {A : Type u_3} {G : Type u_4} [TopologicalSpace A] [Inhabited A] [Monoid G] (Y : MulSubshift A G) (U : Finset G) : Set (Pattern A G)

The language of a subshift Y on a finite shape U.

Equations

• Y.languageOn U = SymbolicDynamics.FullShift.LanguageOn Y.carrier U