The Structure of a Non-Isometric Non-Contractive Bijection of a Hereditarily Precompact Quasi-Metric Space
Thomas Duzer
math.GM
Oct 21, 2026 · v2
TL;DR
The structure theorems and three spiral examples on quasi-metric dynamics are machine-checked in Lean 4 over Mathlib, with files archived on Zenodo.
Abstract
On a hereditarily precompact quasi-metric space, every non-contractive bijection $F$ is asymptotically an isometry along its backward orbits: for all $a$ and $\varepsilon>0$, $0\le d(Fx,Fy)-d(x,y)<\varepsilon$ for $x$ far in the past of $a$ and all $y$. Zavarzina asked whether every such bijection of a precompact space is an isometry; the author's toll spiral (arXiv:2610.13973) answered no. Each such $F$ has a register, a quasi-pseudo-metric $λ^-\le d$ for which $F$ is an isometry, with round-trip distances totally bounded on orbits; after completion, $F$ acts on each orbit as a rotation of a compact monothetic group, its rigid shadow. The defect $d-λ^-$ from $x$ to $y$ is at most the fee of $x$ (the supremum of its defects to earlier iterates) and at least the excess of $x$'s fee over $y$'s now or at any earlier time, less their round-trip register distance; the fee never decreases forward along orbits and tends to zero backward. In this sense, every such $F$ is a toll over its rigid shadow. The fees bound the defect but do not determine it: three spirals show it can depend on $y$, vanish at a distant $y$ even when $x$ has a positive fee, and be positive toward later iterates of $x$. The toll-spiral paper asked whether every such map is conjugate to a tolled extension, a fixed toll zone over an isometric shadow, possibly with infinitely many zones. If only descents are charged, the answer is no, even up to bi-Lipschitz conjugacy; on each infinite orbit, a map is such an extension over its register exactly when its ascents carry no defect. Fees may vanish at any rate, but for zone tolls (two-valued, shift-monotone, subadditive along their routes) they reach zero at a finite depth. The general results hold on quasi-pseudo-metric spaces where every sequence has a left K-Cauchy subsequence; all but the statements listed at the end are machine-checked in Lean.
Problem
The paper addresses the structure of bijective non-contractive maps on hereditarily precompact quasi-metric spaces, which need not be isometries. It also answers the toll-spiral paper's Question 7.6: is every such map conjugate to a tolled extension, a fixed toll zone over an isometric shadow?
Approach
The distance is decomposed as d = λ⁻ + D₀, where the register λ⁻ (the limit of backward-iterate distances) is an F-invariant quasi-pseudo-metric and D₀ is the defect. A fee function c is defined as the supremum of defects to backward returns, and two-sided bounds (the 'band') on the defect are proved in terms of fees. Three explicit spiral examples on Z, built from an irrational rotation plus a toll, show which features are not forced. The results are formalized in Lean 4 over Mathlib, building on earlier verification files.
Results
Every such map is a toll over a rigid shadow, a rotation of a compact monothetic group on each orbit. Fees are nondecreasing forward along orbits and vanish in the deep past. For zone tolls, fees reach zero at a finite depth. If only descents are charged, the answer to the classification question is negative, even up to bi-Lipschitz conjugacy. All results except a few listed statements are machine-checked in Lean.