Compact Quasi-Metric Spaces Are Expand-Contract Plastic
Thomas Duzer
math.FA
Oct 9, 2026 · v1
TL;DR
The two rigidity theorems and most counterexamples are machine-checked in Lean 4 over Mathlib, with files archived on Zenodo.
Abstract
On a totally bounded metric space every non-contractive self-map is an isometry. For quasi-metric spaces, taken $T_1$ throughout ($d(x,y) = 0$ implies $x = y$), this fails: Zavarzina gave a hereditarily precompact counterexample and asked whether bijectivity restores rigidity; a recent example, the toll spiral, shows that it does not. We prove that compactness does: every compact quasi-metric space is expand-contract plastic, that is, each of its bijective non-contractive self-maps is an isometry. Countable compactness suffices, as does compactness of the conjugate topology. Bijectivity cannot be dropped: a compact, hereditarily precompact quasi-metric on the natural numbers makes the shift non-contractive and not an isometry. For arbitrary non-contractive self-maps we prove rigidity when the space is hereditarily precompact and its conjugate topology is sequentially compact, in particular when it is hereditarily precompact and Yoneda complete; neither hypothesis can be dropped. In both theorems the $T_1$ axiom can be weakened to $R_0$ ($d(x,y) = 0$ implies $d(y,x) = 0$), with hereditary precompactness read sequentially (every sequence has a left K-Cauchy subsequence), but not to $T_0$. We construct a $T_0$ space with all the remaining hypotheses of both theorems, Yoneda complete and compact both in its own topology and in the conjugate one, carrying a bijective non-contractive self-map that is not an isometry. Under $R_0$ the two-sided case reduces to the metric theorem, both topologies being sequentially compact exactly when the symmetrized distance is compact; the one-sided theorems do not reduce to it, and plasticity does not pass to the symmetrization even for compact spaces. The two theorems are machine-checked in Lean, and so are the counterexamples, apart from a few statements listed at the end.
Problem
Zavarzina asked whether bijective non-contractive self-maps of precompact quasi-metric spaces must be isometries. The toll spiral shows that they need not be, which leaves open which hypotheses restore this rigidity.
Approach
Using recurrence arguments for orbits under sequential compactness, the authors prove that compact (or countably compact, or conjugate-compact) quasi-metric spaces are expand-contract plastic. They also show that all non-contractive maps are isometries under hereditary precompactness together with sequential compactness of the conjugate topology. Counterexamples show that each hypothesis is needed, including a T0 construction. The main theorems and counterexamples are formalized in Lean 4 with Mathlib.
Results
Every compact quasi-metric space is expand-contract plastic, and the theorems extend from T1 to R0 but not to T0. The Lean files LowerLimits.lean, UpperLimits.lean and ShiftExample.lean check the main results using only the standard axioms. A few lemmas are not mechanized and are listed explicitly.
| compact topology | bijective non-contractive maps | all non-contractive maps |
|---|
| τ_d only | isometries | not always |
| τ_{d^{-1}} only | isometries | not always |
| both (d_s compact) | isometries | isometries |
Which topology is compact versus which maps are forced to be isometries