Papers With

← All papers
First page of Exact Finite-Length Theory of Uniform Car Parking: Spatial Laws, Absorption, and Aggregation

Exact Finite-Length Theory of Uniform Car Parking: Spatial Laws, Absorption, and Aggregation

Ganesh P Kumar

cs.RO Aug 24, 2026 · v1 cs.DS cs.SC math.PR math.RA
formalization mathlib probability combinatorics
Read PDF arXiv abstract
TL;DR
A companion Lean 4/Mathlib development (73 modules, 555 declarations) machine-checks the structural core: the joint-density form, jamming-cell combinatorics, free-length affineness, and count bounds.
Abstract
The uniform car-parking process is the one-dimensional random sequential adsorption of unit cars on a segment of finite length $s$: cars arrive at uniformly random positions and park wherever they fit, until no gap admits another. This paper develops the exact finite-$s$ theory. The joint density of the parked positions is resolved into jamming cells, on each of which it is a rational function, and evaluated by a subset recursion in $O(2^n n)$ operations; the marginal and gap order statistics are obtained as hyperlogarithms whose weight is fixed by the number of coordinates integrated out; and the absorption count and the aggregate quantities are treated through the integral equation descending from Rényi.
Problem

The uniform car-parking process (one-dimensional random sequential adsorption of unit cars on a segment of length s) lacked an exact finite-length theory of the joint law of parked positions, gap statistics, and the absorption count.

Approach

The joint density of the order statistics is written as a sum over arrival orders of products of reciprocal free lengths. It is decomposed into jamming cells indexed by bitstrings, on each of which it is a rational function, and evaluated by a subset recursion in O(2^n n) operations. Marginals are obtained as hyperlogarithms, and the absorption count is treated through Rényi's integral equation. Structural claims are machine-checked in Lean 4 against Mathlib, with external theorems carried as explicit hypotheses and axiom footprints audited.

Fig 2: cell partition and Schlegel diagram
Results

The paper gives closed-form cell counts and feasibility criteria, a weight bound of n-1 on the hyperlogarithmic marginals, moment recursions and support of the absorption count, asymptotic limit laws, and jamming-graph invariants. About 555 Lean declarations verify the core combinatorial and measure-theoretic results, and the exact forms are cross-validated by Monte Carlo simulation.

Fig 3: The UCP joint density at n=2 , s=13/2 ; dotted lines are the cell walls \{G_{i}=1\}