# Zero entropy does not guarantee a smooth positive-volume model

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A zero-entropy system without a smooth positive-volume model](../../preprints/A-finite-entropy-system-without-a-smooth-positive-volume-model-September-25-2026/paper.pdf)

## Scope

The paper asks whether a measure-preserving system can be represented by a smooth diffeomorphism preserving positive smooth volume. The formalized supporting result constructs an ergodic invertible transformation of a standard nonatomic probability space with finite Kolmogorov–Sinai entropy that has no such model on any compact finite-dimensional manifold, including manifolds with smooth boundary. The comparison is measurable conjugacy after discarding null sets.

The linked statement gives finite entropy; the paper's stronger zero-entropy conclusion is outside this statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finite-entropy system without a smooth positive-volume model | [SmoothObstruction.lean](../ComparatorChallenges/SmoothObstruction.lean) |