cs.ROAug 24, 2026
SaveExact Finite-Length Theory of Uniform Car Parking: Spatial Laws, Absorption, and Aggregation
Abstract
The uniform car-parking process is the one-dimensional random sequential adsorption of unit cars on a segment of finite length : cars arrive at uniformly random positions and park wherever they fit, until no gap admits another. This paper develops the exact finite- 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 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.
Figures & tables
| # | Result | Section | Evidence |
|---|---|---|---|
| 1 | The joint density of the positions is the temporal-order sum , one rational function on each region | 5.1 | machine-checked |
| 2 | Every free length is affine in the gaps, with coefficients in | 5.1 | machine-checked |
| 3 | The regions are indexed by jamming bitstrings, with a closed-form feasibility criterion and count | 5.2 | machine-checked |
| 4 | On a region the density is a single rational function, with poles only on free-length hyperplanes | 5.2 | machine-checked |
| 5 | The parking arrangement is linearly reducible, so every marginal is a hyperlogarithm of weight at most | 5.1 | machine-checked |
| 6 | The gap map carries : it is affine with unit Jacobian | 5.4 | machine-checked |
| Question | Section | Obstacle, and the step that would remove it |
|---|---|---|
| Real-rootedness of the count generating polynomial , hence log-concavity and unimodality of | 6 | Real-rootedness is not preserved by the continuous mixture over the split position, and the splitting family has non-constant degree, so the common-interlacer route is unavailable. The remaining candidate is to establish real-rootedness of the symmetric self-convolution by a tree-structured aggregation. |
| The likelihood-ratio order in the segment length | 6 | The same mixture: the order is preserved by independent sums and not by mixtures. Real-rootedness would give it, so this problem is subsumed by the row above. |
| Whether the density can be evaluated in polynomial time, and whether the associated counting problems are -hard | 5.2 | Open in both directions. A collapse of the subset recursion to intervals would need the free lengths to be interval-determined, and they are not. Settling either direction needs new work: a polynomial algorithm exploiting the geometry of the free lengths, or a gadget reproducing the temporal-order sum from a known hard problem. |
| The asymptotic two-point gap density inside the present framework | 7 | Its kernel is an exponential period, outside the algebra of multiple polylogarithms in which the finite-length theory sits. The step is to work in that transcendence class directly, targeting the double-Laplace form of the kernel rather than a polylogarithmic one. |
| Section | Aspect of the attachment chain |
|---|---|
| order statistics | the density on the hard-core polytope ; jammed conditioning, partial step- marginal |
| absorption time | the absorption level / time and its law |
| aggregate / count | the law and moments of , via the strong-Markov split-convolution (R'enyi IE) |
| point process / RGG | the absorbed configuration as a point process and random geometric graph |
| asymptotics | the large- limit — stabilisation, scoped to saturation (§5) |
| probabilistic object | algebraic object |
|---|---|
| one arriving car | grafting in , depth |
| temporal order (position against arrival time) | a word in (ladder tree in ) |
| temporal-order density | the character on that word (comultiplicative for deconcatenation) |
| sorting sum over temporal orders | the shuffle (symmetrize over ) |
| order-stat joint density | |
| marginalize one coordinate | one coaction , weight |
| aggregate subsection | continues | tool laid here |
|---|---|---|
| representations | the split-convolution dictionary | the Volterra / Dyson–Schwinger dichotomy (§1–2) + Hopf ( 4.3 ) |
| additivity | Rényi’s mean equation | the second-kind Volterra resolvent (§1) |
| special-cases | the moment cascade | the Dyson–Schwinger / Faà di Bruno structure (§2) |
| order statistics (integral-equation route) | the rank marginals and the joint density | the Volterra hierarchy + linear reducibility (§1, §4) |
| boundary | the correlation cascade | correlation densities (§3) + transcendence classes (§4) |
Fig 1: The joint density across two jamming walls: continuous, not differentiable
Fig 2: cell partition and Schlegel diagram
Fig 3: The UCP joint density at , ; dotted lines are the cell walls
| general | : | in the literature? | |
|---|---|---|---|
| 1. # cells | no prior source found (the jamming-cell partition) | ||
| 2. qualitatively distinct | (reflection of the segment; the density is rational on every cell, of weight ) | reflection is classical; the partition is not | |
| 3. min terms / cell | : every temporal order is feasible at an interior point | no prior source found | |
| 4. max terms / cell | exactly reciprocal-products: | prior art (the order-sum form ) |
| attachment words | cells (bitstrings) | collapse | gaps computed | -pieces / gap | integrals / gap | max / cell·piece | |
|---|---|---|---|---|---|---|---|
| n=3 | 90 | 15 | (→ refl.) | 11 | 588 | 24 | |
| n=4 | 384 | 16 | (refl.) | 5 | ≈3600 | 288 |
| gap | piece | cells meeting the slice | largest term count |
|---|---|---|---|
| 5 | 39,840 | ||
| 1 | 149 | ||
| 11 | 50,210 | ||
| 5 | 60,253 | ||
| 5 | 55,324 | ||
| 1 | 471 |
Fig 4: Marginals of the joint density at , : the first position and the interior gap , with the half-integer breakpoints marked
| operation | cost | note |
|---|---|---|
| analytic class of | weight-0 rational | sorting adds no transcendentality; polylogs appear only on marginalization |
| representation | permuted copies of (each arrival terms) | halved by the reflection |
| point evaluation | each via Held–Karp subset DP [R8]; the is intrinsic to sorting a non-exchangeable vector | |
| support / pieces | ordered jammed simplex, pieces | Theorem C of 5.2 |
| marginal to | integrate coords | 5.3 |
| gap feature | UCP | Tonks (equilibrium) | Poisson (no hard core) | Mat'ern I/II |
|---|---|---|---|---|
| gap law | size-biased ; non-exchangeable | uniform on simplex; exchangeable | i.i.d. exponential spacings | thinned-Poisson spacings |
| Theorem D ( ) | distinct terms | one term (collapses) | i.i.d. product form | thinned, stationary |
| boundary vs interior | boundary gaps larger ( vs at ) | identical (exchangeable) | identical (stationary) | stationary |
| max gap | w.p. 1 (jamming certificate) | can exceed 1 (equilibrium admits sub-jammed) | unbounded | governed by exclusion |
| min gap | , can be (near contact) | enforced | ||
| gap density shape | log-convex per cell | log-affine (uniform) | log-linear (exponential) | , |
| symbol | meaning |
|---|---|
| the conditional order-statistic density, a probability density | |
| the all-unjammed region , every gap at least ; the modal set for |
Fig 5: UCP joint CDF on the Tonks simplex
Fig 6: Quantile function of X_(1): the inverse is Lambert W
| Property | Global operation | Per-cell assembly? | Cost | Verdict |
|---|---|---|---|---|
| Normalization | sum of integrals | yes (additive) | per-cell integral | easy |
| Moments | sum of integrals | yes (additive) | per-cell integral, weight | easy |
| Marginal density / CDF | integrate out, then over -pieces | yes per -piece | weight- polylog | moderate |
| Joint CDF | integrate over cell box | no (box cuts across cells) | cell box pieces, weight | harder |
| Covariances / association | pair-marginal integrals | yes (additive) | weight- | moderate |
| Quantile | invert the marginal CDF | no (inverse has no per-cell form) | transcendental root-find | hard |
| parent structure | joint order-statistic density | cost |
|---|---|---|
| i.i.d. | elementary product form (David–Nagaraja Ch. 2) | |
| independent non-identical (i.n.i.d.) | a permanent | #P-hard exactly; by Ryser |
| UCP spatial order statistics | structured (a set-function permanent , above) | subset DP ; closed form on the all-unjammed cell; complexity of the general case open |
| general dependent parents (David–Nagaraja Ch. 6) | the dependency theorem , no permanent shortcut | intractable; the temporal (arrival) law |
| route | computes | cost |
|---|---|---|
| Widom arrival sum (naive) | exact finite- density | |
| Held–Karp / Ryser subset DP | exact finite- density | |
| all-unjammed cell (closed form) | point evaluation | |
| Widom kinetic time-integral | density ( -kernel) |
| statement | content | Lean |
|---|---|---|
| free length is a subset sum | over the jammed set , additive, with no interaction between gaps | UCP.freeLength_subset_sum |
| cost of the subset recursion | the memoised recursion performs exactly operations | UCP.Cost.tableCost_eq |
| it costs less than the order sum | whenever | UCP.Cost.tableCost_lt_naive |
| knowing all proper subsets suffices | two weights agreeing on every give the same value | UCP.heldKarp_congr_of_forall_ssubset |
| missing one proper subset does not | if some is never queried, two weights agree on all queries yet differ in value | UCP.heldKarp_not_determined_of_missing |
| a partial-history oracle does not help | an oracle giving the density of the first arrivals supplies the weight only on sets of size , leaving the rest to be queried | UCP.high_levels_remaining |
| feature | UCP (this work) | Tonks (equilibrium) | Mat'ern I | Mat'ern II |
|---|---|---|---|---|
| construction | sequential uniform attachment | concurrent Gibbs draw | Poisson delete any close pair | Poisson keep earliest of close pair |
| conditioning | fixed segment and count | fixed | fixed intensity | fixed intensity |
| joint density on | (size-biased ) | uniform | thinned Poisson (not a fixed- density) | thinned Poisson |
| gaps | non-exchangeable , size-biased | exchangeable (i.i.d. given sum) | stationary, dependent | stationary, dependent |
| order-stat correlation | positive , decays in | positive, exchangeable | short-range | short-range |
| log-shape of density | log-convex per cell , global fail | log-affine (constant) | , (no fixed- density) | , |
Fig 7: The two masses on the band . They cross at , where both equal , so the maximising block is and the mode is not unique.
| route | obstacle |
|---|---|
| Laplace or Sturm–Liouville reformulation | the transform relocates the mixture rather than removing it |
| common interlacer | the family has non-constant degree ( 6.0.4 ) |
| Hodge index on the convolution Gram matrix | the Gram matrix is not Lorentzian |
| Lorentzian polynomials and the Hodge-theoretic route of Adiprasito, Huh and Katz | that machinery delivers log-concavity for the invariants of a matroid or, more generally, for a Lorentzian polynomial. The coefficients are not known to be either: no matroid is known whose invariants they are, and deciding whether is Lorentzian needs the Hessian signature of its homogenisation, which we cannot check without a closed form for |
| determinantal representation | the integral of a determinant is not a determinant, and the pencils have -dependent size |
| Alexandrov–Fenchel or Brunn–Minkowski | the region carrying exactly cars is a non-convex union of cells whose dimension grows with |
| property | UCP, | Tonks, |
|---|---|---|
| real-rootedness | open ( 6.0.4 ) | holds: a unit-interval graph is claw-free, so its independence polynomial is real-rooted (Chudnovsky and Seymour 2007), and the continuum statement follows by a limit |
| log-concavity | open ( 6.0.4 ) | holds, by Newton’s inequalities |
| unimodality | open ( 6.0.4 ) | holds, from log-concavity |
| mode bound | proved ( 6.0.3 ) | holds, the proof using only the support |
| plateaux | occur ( 6.0.3 ) | occur: when , that is at |
| symbol | meaning |
|---|---|
| Rényi parking constant | |
| variance rate, , (Dvoretzky–Robbins / Blaisdell–Solomon) | |
| a stabilizing score at for point set (Penrose–Yukich); is reserved for scores, and the population -quantile of §A2′ is written | |
| radius of stabilization (here -tailed: super-exponential decorrelation) | |
| RSA field / configuration | the random set of parked-car positions on — a point process (“field” in the geometric-probability sense, not an algebraic field) |
| MDA | max-domain of attraction; the three classes are named in words (Gumbel, Weibull, Fréchet), the Gumbel law alone carrying the symbol |
| aspect | partial (subcritical, ) | jammed (saturated) | established in |
|---|---|---|---|
| gap support | unbounded (large voids) | , hard-capped | — |
| gap / void tail | exponential , rate | finite endpoint, contact-divergent | §A5, Lemma V |
| max-gap EVT | Gumbel | Weibull | §A5, Corollary G′ |
| jamming graph | linear forest, geometric components | single path (connected) | 8.1 |
| unbounded scores ( ) | heavy-tailed, CLT can fail | bounded, CLT holds | §A1, Theorem G |
| bounded-score CLT | rate | rate | §A1, Theorem G |
| result | sparse | partial | saturated |
|---|---|---|---|
| A1 bulk CLT | Gaussian (weak dep) | Gaussian, bounded (Thm G); -stable super-tail | Gaussian, all |
| A2/A2′ quantile CLT | — | (§A2′) | median |
| A3 concentration | tighter (more blocks) | sub-Gaussian, bounded ( open — §A3) | sub-Gaussian |
| A4 Berry–Esseen | — | (stabilisation BE, open) | proven |
| A5 max-gap EVT | Gumbel | Gumbel | Weibull ( flip) |
| A7 emp. law | Pyke bridge | func. CLT (§A7) |
| case | statement | status |
|---|---|---|
| (saturated) | , | proven — Penrose–Yukich stabilisation of the bounded gap score |
| (partial, ) | same CLT, ensemble-specific rate | proven for bounded (Theorem G); unbounded jammed-only (heavy tail from large voids) |
Fig 8: A1 CLT: example vs non-example
| case | statement | status |
|---|---|---|
| (saturated) | , | conditional theorem — given (i) the count CLT, (ii) shielding-independence of the half-counts, (iii) a Bahadur–Kiefer remainder; core (linearisation + exact reflection-centring) proven |
| (partial, ) all central quantiles | CLT, | proven (§A2′) — Bahadur 1966/Kiefer 1967 (density-general linearisation) Penrose 2001 count CLT (any density) §G5′ half-count independence. No Rényi split needed; median is . Closes the general case |
Fig 9: A2 median: central vs extreme rank
| case | statement | status |
|---|---|---|
| (saturated) | , bounded | conditional theorem — Freedman on the split-tree martingale, modulo the bounded-remainder lemma of §A3 (Dvoretzky–Robbins 1964); martingale + Freedman step proven |
| (partial, ) | bounded-score normality carries; explicit constant does not | CLT carries (Theorem G, bounded ); the Azuma constant is jammed (split-tree Rényi split). A fixed-density tail needs a stabilisation concentration inequality, not yet instantiated |
Fig 10: concentration vs non-concentration
Fig 11: higher cumulants extensive; standardized cumulants vanish
| case | statement | status |
|---|---|---|
| (saturated) | proven, given Bolthausen’s martingale Berry–Esseen (1982), which gives ; then . The rate theorem is cited, not proved here, and no rate theory of this kind is formalised. Sharp conditional (Grama–Haeusler -QV) | |
| (partial, ) | analogous rate | jammed-as-proved — the split-tree martingale BE is jammed; a fixed-density rate needs the stabilisation Berry–Esseen (Lachièze-Rey–Schulte–Yukich 2019), open for RSA |
Fig 12: A4 Berry–Esseen: bounded vs unbounded
| case | statement | status |
|---|---|---|
| (saturated) | ; in the Weibull MDA (endpoint , shape ), | conditional theorem — given , Chen–Stein Exp ; derived from the kinetic gap equation ( , §A5(iii)); Picard-branch uniqueness is the residual conjecture |
| (partial, ) | in the Gumbel MDA — the EVT class flips | conditional theorem — Corollary G′ (Lemma V exponential void tail, rate ; Chen–Stein), given the asymptotic independence of near-maximal gaps that the Chen–Stein term needs |
Fig 13: A5 Weibull vs Gumbel
Fig 14: Q–Q plots: jammed max-gap is Weibull (via Exp), partial max-gap is Gumbel
| case | statement | status |
|---|---|---|
| (saturated) | Glivenko–Cantelli to closed-form ; functional CLT in | proven — fdd (delta-method stabilisation CLT) tightness (§A7 proof: two-interval fourth-moment bound via Billingsley Thm 13.5, Rényi split, Penrose 2001 stabilisation, Saulis–Statulevičius cumulants); the residual is a split-tree-internal lemma, and the closed form of remains open |
| (partial, ) | spacing process classical Pyke bridge at low , departing toward the jammed finite-range kernel as | kernel computed (not a functional theorem) — density-driven interpolation; the process stays Gaussian, no class flip |
| i.i.d. uniform spacings (Pyke) | jammed RSA gaps (here) | |
|---|---|---|
| scale | — rescale by | — hard-core floor, no rescaling |
| limit law | (exponential, unbounded ) | on , bounded : exactly ( at jamming) |
| density | (§A5(iii)): contact spike, finite | |
| dependence | independent-spacing Brownian bridge | finite-range (super-exp decorrelation) — stabilization covariance |
| max | Gumbel, centering | Weibull , endpoint (§A5) |
| Theorem | Example (holds) | Non-example (fails) | Hypothesis violated |
|---|---|---|---|
| A1 CLT | (bounded) | (unbounded) | boundedness ⇒ Lindeberg fails; heavy tail, skew |
| A2 median CLT | central rank | extreme rank | central/bulk rank ⇒ Bahadur linearization needs positive local density |
| A3 concentration | bounded | (unbounded) | boundedness ⇒ sub-Gaussian tail replaced by heavy tail |
| A4 Berry–Esseen | bounded ( ) | (unbounded) | boundedness ⇒ no CLT, so no rate |
| A5 Weibull max-gap | jammed-RSA (bounded support) | Poisson-process max spacing (unbounded) | bounded support (hard-core) ⇒ Gumbel, not Weibull |
| symbol | meaning |
|---|---|
| ; | segment length; number of parked cars ( ) |
| the gaps, ; internal gaps are | |
| jamming bit (gap is jammed); the 5.1 cell index | |
| internal sub-word edge-indicator of | |
| jamming graph; , | |
| edge count # jammed internal intervals |
Fig 15: jamming graph geometry
| reach-depth | |||||
|---|---|---|---|---|---|
| 1 | 1.000 | 0 | 1.000 | — (single vertex) | — |
| 2 | 1.000 | 0.40308 ∗ | 1.596 | 0.40308 ∗ | 0.000 |
| 3 | 1.000 | 1.300 | 1.700 | 0.370 | 0.004 |
| 4 | 0.996 | 2.676 | 1.324 | 0.681 | 0.409 |
| 5 | 0.589 | 3.981 | 1.019 | 0.981 | 0.964 |
| 6 | 0.021 | 5.000 | 1.000 | 1.000 | 1.000 |
| conn sat | |||
|---|---|---|---|
| 2 | 0.4031 | 0.000 | |
| 3 | 0.370 | 0.004 | |
| 4 | 0.681 | 0.409 | 1.66 |
| 5 | 0.981 | 0.964 | 1.02 |
| 6 | 1.000 | 1.000 | (equality) |
| 2 | 0.596 | 0.404 | 0 | 0.404 |
| 3 | 0.257 | 0.620 | 0.123 | 0.867 |
| 4 | 0.054 | 0.555 | 0.392 | 1.338 |
| 5 | 0.002 | 0.405 | 0.594 | 1.592 |
| 6 | 0 | 0.333 | 0.667 | 1.667 |
Fig 16: jamming graph theorems
Fig 17: jamming-graph spectrum delta-comb
Fig 18: saturated adjacent-gap correlation
Fig 19: J-function inhibition
| aggregate quantity | Hopf object | integral equation | §, status |
|---|---|---|---|
| additive | primitive element | linear Volterra (2nd kind, unit delay) | §2, proved |
| count PGF | group-like element | quadratic Volterra (Dyson–Schwinger) | §3, proved |
| max-gap CDF | group-like element | quadratic Volterra | §3, proved |
| factorial moments | Faà-di-Bruno coordinates | finite linear cascade | §3, proved |
| single order statistic | marginalised character | triangular linear Volterra hierarchy | §4, proved |
| finite -variable joint density | graded component of the character | hyperlogarithm (linear reducibility) | §4, proved |
Fig 20: per-count modes
Fig 21: order-statistic marginals
Fig 22: order-statistic monotonicity in the count
Fig 23: max-gap distribution
| (tangent) | (simulated) | (tangent) | (simulated) | |||
|---|---|---|---|---|---|---|
| count | ||||||
Fig 24: pair density heatmap
Fig 25: three-point density
Fig 26: connected k-gap correlation ladder
| interval | weight | |||
|---|---|---|---|---|
| 0 | ||||
| 0 | ||||
| weight-1 (log) | weight-1 (log) | weight-1 (log) | 1 | |
| weight-2 (dilog) | weight-2 (dilog) | weight-2 (dilog) | 2 |
Fig 27: M1 and variance-rate convergence to their asymptotic constants
| (DSE march) | (order-statistic MC, s.e.) | |
|---|---|---|
| (DSE) | histogram (process MC, s.e.) | |
|---|---|---|
| Rényi | residual at | ||||
|---|---|---|---|---|---|
Fig 28: mean and variance against their asymptotics
Fig 29: the standardised third cumulant
Fig 30: Dependency graph of the machine-checked results. Roots (shaded) are the process measure and the free-length affineness; dashed clusters are conditional on the hypotheses listed below.
| result cluster | discharged (proved from / ) | assumed (explicit hypothesis) | why assumed |
|---|---|---|---|
| process measure | , PM-norm , total mass one, arrival kernel, first-arrival disintegration | — | — |
| order-statistic density | positional density, -symmetrisation, , reducibility | — | — |
| log-convexity | per-cell and on the density itself; exact global-failure counterexample | — | — |
| complexity | unjammed closed form, jammed subset-sum reduction, counting identity, the Held–Karp subset-recursion identity, refutation of the /FP claim | — | — |
| jamming graph | linear-forest structure, , , , independence / matching / domination, deletion law | — | — |
| weight ladder | the parking arrangement is reducible; the weight algebra | Aomoto–Goncharov period theorem, and a marginal-equals-integral identification | the period theorem is deep analysis absent from Mathlib; the marginal identification is separate work |
We explore the question of how to learn an optimal search strategy within the example of a parking problem where parking opportunities arrive according to an unknown inhomogeneous Poisson process. The optimal policy is a threshold-type stopping rule characterized by an indifference position. We propose an algorithm that learns this threshold by estimating the integrated jump intensity rather than the intensity function itself. We show that our algorithm achieves a logarithmic regret growth, uniformly over a broad class of environments. Moreover, we prove a logarithmic minimax regret lower bound, establishing the growth optimality of the proposed approach.
High-Density Automated Valet Parking with Relocation-Free Sequential Operations
In this paper, we present DROP, high-Density Relocation-free sequential OPerations in automated valet parking. DROP addresses the challenges in high-density parking & vehicle retrieval without relocations. Each challenge is handled by jointly providing area-efficient layouts and relocation-free parking & exit sequences, considering accessibility with relocation-free sequential operations. To generate such sequences, relocation-free constraints are formulated as explicit logical conditions expressed in boolean variables. Recursive search strategies are employed to derive the logical conditions and enumerate relocation-free sequences under sequential constraints. We demonstrate the effectiveness of our framework through extensive simulations, showing its potential to significantly improve area utilization with relocation-free constraints. We also examine its viability on an application problem with prescribed operational order. The results from all experiments are available at: https://drop-park.github.io.
Limit Theorems and Optimal Policies for Flock Flight through Poisson Forests
Inspired by birds flying through cluttered environments, Karaman and Frazzoli showed that high-speed flight through an ergodic random forest exhibits an ultimate speed limit: above a critical speed, almost surely no infinite collision-free trajectory exists for a single bird. This paper formulates a corresponding bulk-transport problem for many birds. We construct an explicit directed corridor network in a Poisson disk forest and impose a common temporal headway at its waypoints. The maximum current equals a minimum vertex-cut capacity and is achieved by repeated flight along vertex-disjoint paths. The same schedule maximizes completed traversals at every finite horizon, with constant forward speed and no internal waiting. For a forest belt of fixed depth, exact transverse superadditivity yields an almost-sure deterministic current-density limit. A uniform shape theorem for an asymmetric planar dual identifies the current when depth and width grow together. For diverging depth bounded by a constant times width, this current equals the width-first, depth-second limit and is independent of the positive aspect ratio. When diagonal corridors are available, bulk current is positive at sufficiently low obstacle intensity and zero at sufficiently high intensity. For stochastic demand, an upstream admission queue is stable at every rate below the finite-network capacity.