Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Addition on Infinite Legal Digit Streams

Abstract

Addition on Infinite Legal Digit Streams.

Definition 1.1 (Agreement with finite addition).

Lean statement: D5/S1/Digit/Infinite/NoContinuousAdditionExtension.ExtendsFiniteAddition

Formalization. D5/S1/Digit/Infinite/NoContinuousAdditionExtension.ExtendsFiniteAddition (✓ std3).

Citation. Guy Barat, Valérie Berthé, Pierre Liardet, Jörg Thuswaldner (2006). Dynamical directions in numeration. DOI: 10.5802/aif.2233.

Commentary.

The operation sends the digit rows of any two natural numbers to the digit row of their sum.

Theorem 1.2 (Separate continuity obstruction).

Lean statement: D5/S1/Digit/Infinite/NoContinuousAdditionExtension.result

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

Citation. Guy Barat, Valérie Berthé, Pierre Liardet, Jörg Thuswaldner (2006). Dynamical directions in numeration. DOI: 10.5802/aif.2233.

Commentary.

There is no binary operation on the legal infinite digit streams that is continuous in each variable separately and agrees with addition on all natural number digit rows. The cited survey treats numeration compactifications and odometers.

References