Continuous decoding and aperiodicity
Abstract
Continuous decoding and aperiodicity.
Definition 1.1 (Construction).
Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialSubshift.decode
Formalization. D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialSubshift.decode (✓ std3).
Source. Repository-derived.
Commentary.
The compact tiling reader is injective, so its inverse on the factorial subshift is continuous. A positive period would preserve every recognizable boundary set. Choosing a level whose shortest block exceeds that period translates a boundary into a strict block interior, a contradiction. The natural-number orbit is injective, so the base is infinite.
Theorem 1.2 (Result).
Lean statement: D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialSubshift.factorial_no_positive_period
Proof. Machine-checked in Lean as D5/S1/Dynamics/Symbolic/PermutativeLifts/FactorialSubshift.factorial_no_positive_period (✓ std3). ∎
Source. Repository-derived.
Commentary.
The compact tiling reader is injective, so its inverse on the factorial subshift is continuous. A positive period would preserve every recognizable boundary set. Choosing a level whose shortest block exceeds that period translates a boundary into a strict block interior, a contradiction. The natural-number orbit is injective, so the base is infinite.