Comments: There are many new corrections with respect to v1 - v3. Also new pictures are included. Now the paper has a helpful companion: arXiv:2511.20724. Roughly it is a part of the version v2 of the present paper. It contains a variant of Hall's harem theorem with controlled sizes of cycles, where all computability issues are ruled out. The corresponding proof is similar and slightly simpler
We prove a computable version of the Hall Harem Theorem where the matching realizes a unary function with controlled sizes of cycles. We apply it to non-amenable computable coarse spaces. As a result, we obtain a computable version of the geometric von Neumann conjecture.