Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Eventual Merging of Infinite Legal Streams

Abstract

Eventual Merging of Infinite Legal Streams.

Theorem 1.1 (The eventual-merging relations of the successor).

Lean statement: D5/S1/Digit/Infinite/PhaseOrbitRelations.phase_orbit_relations

Proof. Machine-checked in Lean as D5/S1/Digit/Infinite/PhaseOrbitRelations.phase_orbit_relations (✓ std3). ∎

Source. Repository-derived.

Commentary.

The rotation orbit relation on the circle and the relation of eventual merging at possibly different successor times are countable Borel equivalence relations. Two legal streams eventually merge at possibly different times exactly when their phases belong to the same rotation orbit; they merge at a common time exactly when their phases agree. For each positive integer j, all streams of phase minus j times the golden ratio reach the zero row after j steps. Two distinct streams in that fibre remain distinct at every earlier step.

References