Timing, Entry, and Revenue in Clock-Based Platform Markets
Thomas Pitz, Vinicius Ferraz
econ.TH
Apr 12, 2026 · v4
TL;DR
Formal dominance, comparative-statics, and payment-inequality results are machine-verified in Lean 4, with sources in a public GitHub repository.
Abstract
On platforms where time-to-contract is itself payoff-relevant–Aalsmeer's flower auctions, ride-hailing dispatch, on-demand-labor matching–the textbook revenue equivalence between Dutch and first-price formats holds the trading outcome fixed. Once participation is endogenous and both sides bear waiting costs, the trading format directly shapes who enters, market thickness, volume, and platform revenue. The platform's ranking of the descending clock against immediate and batched posted-price benchmarks is decided by two estimable primitives on each side of the market: an earnings gap and a timing gap. A bidirectional four-case classification identifies when the descending clock dominates at every level of waiting costs, only above a floor, only below a ceiling, or not at all; the last case is unconditional – when the descending clock charges no more per trade and contracts no faster than the posted-price benchmark, it cannot win. No format admits a universal ranking. The local verdict propagates through endogenous entry, and cross-side complementarity amplifies shared local advantages into joint dominance. A conditional revenue theorem converts entry and volume gains into a platform-revenue ranking. In calibrated parameterizations the revenue-ranking switching boundary lies near $p_0/\bar v\approx 1$, inside the empirical range for ride-hailing platforms. A measurement protocol provides explicit nonparametric estimators for the six reduced-form objects and a test statistic for the dominance condition, and a Lean 4 formalization audits the algebraic and order-theoretic content. In markets where goods or services cannot wait, the speed of the trading mechanism is a primitive of market design.
Problem
On platforms where time-to-contract affects payoffs, such as flower auctions and ride-hailing, standard Dutch/first-price revenue equivalence ignores endogenous two-sided entry and waiting costs. The question is when a descending clock beats immediate or batched posted-price formats in entry, volume, and platform revenue.
Approach
A timing–entry–volume framework evaluates outcomes as (match, price, time) triples, with endogenous driver and rider participation and a Poisson-meeting microfoundation. Dominance is characterized by earnings and timing gaps on each side, giving a four-case classification. The framework includes a measurement protocol with nonparametric estimators. The algebraic and order-theoretic results are formalized in Lean 4.
Results
No format is universally best. The Dutch clock dominates batch clearing for all positive waiting costs under acceptance-rate matching. In calibrations, the revenue-ranking switching boundary lies near p0/v̄ ≈ 1. The Lean formalization showed that a corrected dominance theorem needs only the weaker payment inequality, not the original equality assumption.
