Minimality of the Golden Word Subshift

Abstract

Uniform recurrence makes every member of the golden word subshift share its factor language, hence every forward orbit is dense and no proper nonempty closed shift-invariant subsystem exists.

Write X_x for the prefix-language subshift generated by a one-sided word x, and F_x(n) for its set of length-n factors. Uniform recurrence supplies the reverse language inclusion needed to turn the general subshift inclusion into equality for every member of X_g.

Theorem 1.1 (A subshift member has no new factors).

$$y\in X_x\Rightarrow F_y(n)\subseteq F_x(n)$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.wordFactorSet_subset_of_mem_wordSubshift (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an arbitrary finite alphabet, shift invariance keeps every forward shift of y inside X_x. Applying the prefix condition at the start of an occurring factor of y places that factor in the language of x.

Theorem 1.2 (Every golden factor occurs in every golden-subshift member).

$$y\in X_g\Rightarrow F_g(n)\subseteq F_y(n)$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordFactorSet_subset_of_mem_wordSubshift (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose a golden recurrence window of length B(n) whose word is realized as a prefix of y. Uniform recurrence places the prescribed golden factor wholly inside that window, and translating its start yields an occurrence in y.

Theorem 1.3 (Every golden-subshift member has the golden language).

$$y\in X_g\Rightarrow F_y(n)=F_g(n)$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordFactorSet_eq_of_mem_wordSubshift (✓ std3). ∎

Source. Repository-derived.

Commentary.

The general factor inclusion and the uniform-recurrence reverse inclusion give equality at every finite length.

Theorem 1.4 (Every member generates the golden subshift).

$$y\in X_g\Rightarrow X_y=X_g$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.wordSubshift_eq_of_mem_golden_wordSubshift (✓ std3). ∎

Source. Repository-derived.

Commentary.

A prefix-language subshift is determined length by length by its factor sets, so equality of all finite languages gives equality of the generated subshifts.

Theorem 1.5 (Every forward orbit is dense in the golden subshift).

$$y\in X_g\Rightarrow \mathrm{cl}({\mathrm{Orb}}^{+}(y))=X_g$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordSubshift_minimal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The closure of a word’s forward shift orbit is its prefix-language subshift. Since every golden-subshift member generates X_g, its orbit closure is exactly X_g.

Theorem 1.6 (There is no proper nonempty closed invariant subsystem).

$$S\subseteq X_g\wedge S\ne \varnothing \wedge \mathrm{Closed}(S)\wedge \sigma (S)\subseteq S\Rightarrow S=X_g$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordSubshift_eq_of_isClosed_shift_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose a member y of the subsystem. Shift invariance contains its whole forward orbit, closedness contains the orbit closure, and minimality makes that closure all of X_g. The assumed reverse inclusion then gives equality. Registering mathlib’s AddAction.IsMinimal instance on the subshift subtype is deliberately left to a future node.

References

• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordFactorSet_eq_of_mem_wordSubshift
• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordFactorSet_subset_of_mem_wordSubshift
• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordSubshift_eq_of_isClosed_shift_invariant
• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.golden_wordSubshift_minimal
• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.wordFactorSet_subset_of_mem_wordSubshift
• Truth anchor: D5/S1/Words/Complexity/GoldenSubshiftMinimality.wordSubshift_eq_of_mem_golden_wordSubshift
• Dependency: D5/S1/Words/Complexity/SubshiftTopology
• Dependency: D5/S1/Words/GoldenUniformRecurrence