Multiplication on Infinite Legal Digit Streams

Abstract

Multiplication on Infinite Legal Digit Streams.

Theorem 1.1 (The multiplier obstruction).

Lean statement: D5/S1/Digit/Infinite/MultiplierObstruction.multiplier_obstruction

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

Source. Repository-derived.

Commentary.

For every natural number m at least two, no continuous self-map of the legal streams sends the digit row of n to the digit row of m times n for every natural number n.

References

• Truth anchor: D5/S1/Digit/Infinite/MultiplierObstruction.multiplier_obstruction
• Dependency: D5/S1/Digit/GoldenZeckendorfLanguage
• Dependency: D5/S1/Digit/Infinite/SignedSeriesFibres
• Dependency: D5/S1/Digit/Raw