Bijective Non-Contractive Maps of Hereditarily Precompact Quasi-Metric Spaces Need Not Be Isometries
Thomas Duzer
math.GN
Sep 17, 2026 · v1
math.FA
TL;DR
The core counterexample construction, including quasi-metric axioms, hereditary precompactness, and the circle instance, is formalized sorry-free in Lean 4 over Mathlib.
Abstract
Zavarzina asked whether every bijective non-contractive self-map of a precompact quasi-metric space is an isometry. We answer the question in the negative, in a stronger form: on a hereditarily precompact quasi-metric space (a tolled extension of the irrational rotation over Z), the shift is a bijective non-contractive map that is not an isometry. The construction generalizes: for every metric space Y, every bijective isometry $σ$ of Y, and every point whose $σ$-orbit is aperiodic and totally bounded, the tolled Z-extension is such a counterexample; instances include the irrational rotation and the p-adic odometer. The conjugate space is not precompact, so the two-sided hypothesis of Zavarzina's positive result is sharp, and the space is not expand-contract plastic. The core results, including the general scheme and the circle instance, are machine-checked in Lean 4 over mathlib, sorry-free (no unproved steps), under a pinned toolchain. A structural section proves a monochromy theorem: for every strict pair on a hereditarily precompact space, one endpoint's backward self-returns have self-defect at least a quarter of the pair's defect, uniformly on a chain-closed displacement set. Boundary results delimit what remains open: one-sided compactness together with separation.
Problem
Zavarzina asked whether every bijective non-contractive self-map of a precompact quasi-metric space must be an isometry. The question is the asymmetric analogue of expand-contract plasticity for totally bounded metric spaces.
Approach
The authors build a 'toll spiral': a tolled Z-extension of a metric space with a bijective isometry and an aperiodic point whose orbit is totally bounded. The quasi-metric adds a constant toll c on descending pairs whose source index is nonnegative, and the shift n→n+1 serves as the map. The results of Section 3 are formalized in a single Lean 4 file, TollSpiral.lean, over a pinned Mathlib. The formalization has an abstract core layer and a family layer, and covers the irrational rotation as the circle instance. A structural section proves an invariant limit register and a monochromy theorem on paper.
Results
The shift is a bijective non-contractive non-isometry on a hereditarily precompact quasi-metric space, which answers the question negatively. Because the conjugate space is not precompact, the two-sided hypothesis of Zavarzina's positive theorem is sharp, and the space is not expand-contract plastic. The Lean artifact, archived on Zenodo, compiles sorry-free and warning-free and checks hereditary precompactness in both sequential and net form.
