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 |