bibkey: morsehedlund1940symbolic authors: Marston Morse and Gustav A. Hedlund year: 1940 title: Symbolic Dynamics II. Sturmian Trajectories doi: 10.2307/2371431 claim: A one-sided infinite word with at most n factors of some length n is eventually periodic. strata_touched:
- D5/S1/Words/Complexity/MorseHedlund license: citation-only triage: anchor
Symbolic Dynamics II. Sturmian Trajectories
Morse and Hedlund establish the factor-complexity threshold now bearing their
names. In the one-sided form used here, an infinite word over a finite alphabet
is eventually periodic when its number of factors of some length n is at most
n. Equivalently, a word that is not eventually periodic has at least n + 1
factors of every length.
The repository formalization fixes natural starting indices and concludes only eventual periodicity, so a finite nonperiodic prefix is allowed. It does not claim recurrence, balance, a bi-infinite classification, or the converse description of every Sturmian word. The literature attests the classical theorem statement; the Lean proof is a direct repository implementation using finite factor sets, unique right extension, and pigeonhole.
Search log
- 2026-08-13: The accepted GOLD-34 design supplied the classical theorem and
the repository spec supplied the canonical bibkey
morsehedlund1940symbolic. - 2026-08-13: Searched the repository, pinned Mathlib checkout, and git history for Morse-Hedlund names, generic word-factor complexity, and eventual-word periodicity. No reusable generic theorem was found.
- 2026-08-13: The lean4 skill’s local smart search for
Morse Hedlund factor complexity eventually periodic wordreturned no declaration match. - 2026-08-13: No online metadata query was run because network capability was unavailable in the implementation environment. The DOI, authors, year, and title were not independently verified in this turn and must be checked by the repository’s normal literature-observation lane.
Locator
- DOI: https://doi.org/10.2307/2371431