Operations Research

Motivation

Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.

Timeline, as far as this mission is concerned:

• 1952: Wardrop states the static user-equilibrium criterion (equal and minimal travel times on used routes).
• 1979–1980: Smith and Dafermos formulate static user equilibrium as a finite-dimensional variational inequality.
• 1989: Friesz, Luque, Tobin and Wie treat dynamic route choice with a fixed departure schedule as an optimal-control problem.
• 1993: Friesz et al. (this paper) formulate simultaneous route and departure-time equilibrium and prove its equivalence with a variational inequality on $(L^2[0,T])^{|P|}$ (Theorem 2, p. 187).

Setting

A traffic network has a finite set $P$ of paths. Each path $p$ connects exactly one origin–destination (OD) pair $kl$; $P_{kl}$ denotes the paths of pair $kl$. Travellers depart during the horizon $[0,T]$, $T>0$, which carries Lebesgue measure $\nu$; "$\forall_\nu(t)$" means "for $\nu$-almost every $t\in[0,T]$".

A vector of departure-time densities $h=(h_p)_{p\in P}$ assigns to each path a square-integrable, almost everywhere nonnegative function $h_p$ on $[0,T]$: $h_p(t)$ is the rate at which travellers depart at time $t$ on path $p$. The set of such vectors is $H_+$. Each OD pair has a fixed travel demand $Q_{kl}$, and the feasible set is

$$\Lambda=\Big\{h\in H_+ : \sum_{p\in P_{kl}}\int_0^T h_p(t)\,d\nu(t)=Q_{kl}\ \text{for every OD pair } kl\Big\}.\qquad(38)$$

A cost operator gives the effective delay $C_p(t,h)\ge 0$ of departing at time $t$ on path $p$ when the densities are $h$: travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,

$$\mu_p(h)=\operatorname{ess\,inf}\{C_p(t,h):t\in[0,T]\}=\sup\{x\in\mathbb R:\ \nu\{t: C_p(t,h)<x\}=0\},$$

and the lowest achievable cost for pair $kl$ is $\mu_{kl}(h)=\min_{p\in P_{kl}}\mu_p(h)$.

Definition 3. For $h\in\Lambda$ and a nonnegative vector $\mu=(\mu_{kl})$, the pair $(h,\mu)$ is an SRD equilibrium if for every OD pair $kl$ and every $p\in P_{kl}$:

$$h_p(t)>0\ \Rightarrow\ C_p(t,h)=\mu_{kl}\quad\forall_\nu(t),\qquad C_p(t,h)\ge\mu_{kl}\quad\forall_\nu(t).$$

No positive-measure set of travellers can lower its cost by switching route or departure time.

Formalization targets

Goal: Theorem 2 (PIE VIP)

For $h^*$ with nonnegative, square-integrable costs $C_p(\cdot,h^*)$:

$$\big(\exists\,\mu^*:\ (h^*,\mu^*)\ \text{SRD equilibrium}\big)\ \Longrightarrow\ h^*\in\Lambda\ \text{and}\ \sum_{p\in P}\int_0^T C_p(t,h^*)\,[h_p(t)-h^*_p(t)]\,d\nu(t)\ge 0\ \ \forall h\in\Lambda,\qquad(39)$$

and conversely, if $h^*\in\Lambda$ solves (39), then $(h^*,\mu(h^*))$ with $\mu^*_{kl}=\mu_{kl}(h^*)$ is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential $\mu^*$.

Milestones

1. Lemma 2: a measurable function positive on a set of positive measure exceeds some $\varepsilon_0>0$ on a set of positive measure.
2. The pointwise inequality (42) at an equilibrium, and the necessity half of Theorem 2.
3. Condition (17) holds by construction for $\mu^*=\mu(h^*)$.
4. The positive-measure sets (44)–(46) and (47) produced by a failure of (16).
5. Feasibility (50) of the mass-shifted vector (48)–(49), the value bound (54), and the sufficiency half of Theorem 2.

Significance

The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima $\mu_{kl}(h^*)$, so the multiplier $\mu^*$ need not be found separately.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in $L^2$" arguments, which recur in continuous-time equilibrium models.

Difficulty

Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity $\int_0^T[h_p-h^*_p]\,d\nu=0$, which is false; only the sum over $P_{kl}$ vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets $S_p(\varepsilon,\delta)$ and $T_q(\varepsilon)$, a nonatomicity argument that a pointwise proof would miss.

Formalization scope

Densities are plain functions $\mathbb R\to\mathbb R$ with a square-integrability condition with respect to $\nu=$ Lebesgue measure restricted to $[0,T]$, not $L^2$ equivalence classes; every pointwise condition is $\nu$-almost everywhere, and values outside $[0,T]$ are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when $C$ is altered on a null set and makes sufficiency false. $\mu_{kl}$ is a real infimum over $P_{kl}$; for a pair with no paths it is an unused default value.

The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain $\mathbb R_+$ of (13)) and square-integrability are assumed only at $h^*$, which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is $0$, so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from $p=q$ to $p\ne q$ (p. 188) is taken as the hypothesis $p\ne q$.

A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of $L^2$ functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3):325–362, 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. J. Smith, The existence, uniqueness and stability of traffic equilibria, Transportation Research B 13(4):295–304, 1979. https://doi.org/10.1016/0191-2615(79)90022-5
• S. Dafermos, Traffic equilibrium and variational inequalities, Transportation Science 14(1):42–54, 1980. https://doi.org/10.1287/trsc.14.1.42
• T. L. Friesz, J. Luque, R. L. Tobin and B. W. Wie, Dynamic network traffic assignment considered as a continuous time optimal control problem, Operations Research 37(6):893–901, 1989. https://doi.org/10.1287/opre.37.6.893
• P. R. Halmos, Measure Theory, Van Nostrand, 1950 (Proposition 41.2, nonatomicity of Lebesgue measure).

Motivation

Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound $C^k_1$. Whether this procedure converges at all is the question of this mission.

Timeline:

• 1991: Pereira and Pinto publish SDDP, with no convergence proof.
• 1999: Chen and Powell prove almost-sure convergence for CUPPS; Linowsky and Philpott (2005) extend the argument to SDDP, AND and ReSa. Both proofs rely on an unstated independence assumption between sampled outcomes and convergent subsequences of iterates.
• 2008: Philpott and Guan (Oper. Res. Lett. 36(4), 450–455) give a proof based on the finiteness of the set of distinct cut coefficients, for a class they call DOASA (Dynamic Outer Approximation Sampling Algorithms).
• Later work (Shapiro 2011; Girardeau, Leclère and Philpott 2015) extends convergence to convex nonlinear and continuous settings.

Setting

There are $T\ge2$ stages. Stage $t$ has a decision $x_t\ge0$ in $\mathbb R^{n_t}$, costs $c_t$, a matrix $A_t$ and, for $t\le T-1$, a matrix $B_t$ coupling $x_t$ to the next stage. At stage $1$ the constraint is $A_1x_1=b_1$. For $2\le t\le T$ the right-hand side is random: $A_tx_t=\omega_t-B_{t-1}x_{t-1}$, where $\omega_t$ takes values $\omega_{t1},\dots,\omega_{tq_t}$ with probabilities $p_{ti}>0$, independently across stages. The expected cost-to-go is defined backwards from $\mathcal Q_{T+1}\equiv0$:

$$Q_t(x_{t-1},\omega_{ti})=\min\{c_t^\top x_t+\mathcal Q_{t+1}(x_t):A_tx_t=\omega_{ti}-B_{t-1}x_{t-1},\ x_t\ge0\},\qquad \mathcal Q_t=\sum_i p_{ti}Q_t(\cdot,\omega_{ti}),$$

and $Q_1=\min\{c_1^\top x_1+\mathcal Q_2(x_1):A_1x_1=b_1,x_1\ge0\}$ is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.

The approximate problem [AP$_t^k$] replaces $\mathcal Q_{t+1}$ by $\max_j\{\alpha_{t+1,j}-(\beta^j_{t+1})^\top x_t\}$ over the cuts generated before iteration $k$; its value is $C^k_t$. A scenario fixes one outcome per stage $2,\dots,T-1$. Each DOASA iteration (i) samples one forward scenario $\omega^k$ and solves [AP$_t^k$] along it, giving states $x^k_t$; (ii) for $t=T,\dots,2$ runs the Cut Calculation Algorithm (CCA): it solves [AP$_t^k$] at $x^k_{t-1}$ for the outcomes in a backward sample $\Omega^k_t$, stores optimal extreme-point dual solutions $(\pi,\rho)$ in a collection $\mathcal D_t$, picks for every outcome the best stored dual, and averages them into a new cut on $\theta_t$. DOASA-N instead traverses a fixed list of $N$ scenarios in every iteration.

Formalization targets

Goal: Theorem 4 under the joint sampling property J

If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration $K$ after which the cuts no longer change, the policy $\bar x$ they induce is optimal for [LP1], and

$$C^K_1=Q_1 .$$

Milestones

• Monotonicity (p. 4): $C^{k+1}_t\ge C^k_t$ and $C^{k+1}_1\ge C^k_1$.
• Lower bound (p. 4): every cut is valid, so $C^k_t\le Q_t$ and $C^k_1\le Q_1$.
• Lemma 1 (p. 6): the set $\mathcal G^k_t$ of distinct generated cuts is bounded in size and eventually constant.
• Lemma 2 (p. 10): DOASA-N stops changing after finitely many iterations, with $\lim_kC^k_1\le Q_1$.
• Lemma 3 (p. 10): DOASA-N over all scenarios, with backward sampling infinitely often per scenario, converges almost surely to an optimal policy.

Significance

The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.

The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.

Difficulty

The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors $\rho$ grow in dimension with $k$, so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.

Formalization scope

Stages are numbered $1,\dots,T$ with variable dimensions per stage. B t is the paper's $B_t$, the matrix multiplying $x_t$ in stage $t+1$. Value functions are real infima, used only on reachable states. Iterations are numbered from $0$ in Lean. Explicit choices, each recorded in the item statements:

• The J correction. The paper states Theorem 4 under FPSP and BPSP. These do not suffice. In a three-stage instance whose last-stage backward sample is $\{c\}$ after forward outcome $a$ and $\{d\}$ after $b$, alternating, both properties hold but the cuts stabilize at a suboptimal policy with $C^k_1$ below $Q_1$. The goal is stated under J, which implies FPSP and BPSP and holds for the schemes the paper names. Lemma 3's BPSP is read per scenario of DOASA-N.
• Initial cut. The paper's trivial cut $\theta_{t+1}\ge-\infty$ makes [AP$_t^1$] unbounded; it is replaced by a finite cut $\theta_{t+1}\ge L_t$ assumed valid on reachable states. Stage $T$ uses the exact cut $\theta_{T+1}\ge0$.
• (A4) is required on reachable states only.
• The LP solver is a deterministic oracle on cut sets returning optimal solutions of [AP$_t$], so repeated cuts do not change forward solutions.
• Duals. Collected duals are optimal extreme points of the dual region; best duals are chosen with arbitrary tie-breaks. No cut is added while the dual collection is empty. Dual multipliers $\rho$ are sequences padded with zeros.
• Runs are relations covering DOASA and DOASA-N (batched forward scenarios). The conclusions hold for every run consistent with the samples, inside the almost-sure quantifier.

A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.

A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.

Selected references

• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4) (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013 (cited from the authors' manuscript v24, 2008-02-25)
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• Z.-L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, J. Optim. Theory Appl. 102 (1999) 497–524. https://doi.org/10.1023/A:1022641805263
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209 (2011) 63–72. https://doi.org/10.1016/j.ejor.2010.08.007
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1) (2015) 130–145. https://doi.org/10.1287/moor.2014.0664

Motivation

The vehicle routing problem with time windows (VRPTW) asks for minimum-cost routes from a central depot that serve every customer exactly once, respecting vehicle capacity and a time interval in which each customer's service must begin. It models school bus routing, parcel and retail distribution, and dial-a-ride services. Desrochers, Desrosiers and Solomon (Oper. Res. 40 (1992) 342–354) gave an optimization algorithm for the VRPTW that solved benchmark instances with up to 100 customers to optimality, a size far beyond earlier exact methods. Their method, which solves the linear relaxation of a set partitioning model by column generation with routes priced out by a resource-constrained shortest path dynamic program, is the template that later exact vehicle routing algorithms ("branch-and-price") follow.

The mathematical core of the method is a certificate: once the pricing subproblem reports that no route has negative marginal cost (reduced cost), the current linear programming solution is optimal over all routes the subproblem can generate, its value bounds every VRPTW solution from below, and an integral solution covering each customer exactly once is VRPTW-optimal. This mission formalizes that certificate and the lemmas of the paper it rests on.

Setting

The nodes are a depot $d$ and customers $N\setminus\{d\}$. An arc set $A$ carries, for each arc $(i,j)$, a cost $c_{ij}$ and a duration $t_{ij}$; each node has a demand $q_i$ and a time window $[a_i,b_i]$; vehicles have capacity $Q$.

A path $(d, i_1, \dots, i_K, d)$ uses arcs of $A$ and passes through the depot only at its ends. It is resource-feasible when there are service start times $T_0 = 0, T_1, \dots, T_{K+1}$ with $T_k + t_{i_k i_{k+1}} \le T_{k+1}$ (waiting is allowed) and $a_{i_k}\le T_k\le b_{i_k}$, and its load $\sum_{k=1}^{K} q_{i_k}$ is at most $Q$. Its cost is $c_r = \sum_{k=0}^{K} c_{i_k i_{k+1}}$, and $\gamma_{ir}$ is the number of visits of $r$ to customer $i$. The paper uses three solution spaces:

1. feasible routes $R$: resource-feasible paths visiting each customer at most once;
2. second-model paths: resource-feasible paths where customers may repeat (the state-space relaxation that tracks load and time but not the set of visited customers);
3. third-model paths: second-model paths with no 2-cycle $(i, j, i)$.

A VRPTW solution is a set of feasible routes covering each customer exactly once; its cost is the sum of the route costs.

The set covering type model (Sec. 4) over a column set $\mathcal R$ is

$$\min \sum_r c_r x_r \quad\text{s.t.}\quad \sum_r \gamma_{ir}x_r \ge 1\ (i \ne d),\quad \sum_r x_r - X_d = 0,\quad \sum_r c_r x_r - X_c = 0,$$

with $x_r\in\{0,1\}$ and $X_d, X_c\ge 0$ integer. Its LP relaxation replaces $x_r\in\{0,1\}$ by $x_r\ge 0$ and drops integrality. For dual values $\pi_i$, $\pi_d$, $\pi_c$ of the three rows, the marginal cost of a column and of an arc are

$$\bar c_r = c_r - \sum_{i\ne d}\pi_i\gamma_{ir} - \pi_d - \pi_c c_r,\qquad \bar c_{ij} = (1-\pi_c)c_{ij} - \pi_i\quad(\pi_i := \pi_d \text{ at } i = d).$$

Formalization targets

Goal: the column generation certificate

Let $R_0$ be a finite set of third-model paths, $\bar z = (\bar x, \bar X_d, \bar X_c)$ an optimal solution of the LP relaxation restricted to $R_0$, and $(\pi,\pi_d,\pi_c)$ an optimal solution of its dual. If every third-model path has nonnegative marginal cost, $\sum_{k=0}^{K}\bar c_{i_k i_{k+1}} \ge 0$, then

$$\bar z \text{ is optimal for the LP relaxation over all third-model paths},$$

and, when arc costs are nonnegative, $\sum_r c_r \bar x_r \le \text{cost}(S)$ for every VRPTW solution $S$; if moreover $\bar x$ is integral and covers each customer exactly once, its support is an optimal VRPTW solution.

Milestones

1. Feasible routes $\subseteq$ third-model paths $\subseteq$ second-model paths (Sec. 3, p. 346).
2. $\bar c_r = \sum_{k=0}^{K}\bar c_{i_k i_{k+1}}$ for every path (Sec. 4.1, p. 347).
3. Nonnegative column marginal costs over all third-model paths make the restricted optimum optimal (Sec. 4, p. 346).
4. Every VRPTW solution is a feasible LP point of equal cost (Sec. 2, p. 344).
5. An integral, exactly covering LP point is a VRPTW solution of equal cost (Sec. 5, p. 348).
6. Under the strict triangle inequality, LP optima over routes do not overcover (Sec. 5, p. 348).
7. The four time window reduction conditions preserve the set of paths (Sec. 6.1, p. 349).
8. The Figure 1 example has 11, 22 and 12 solutions in the three models (pp. 345–346).

Significance

The certificate is the correctness statement of column generation for vehicle routing: it says when the algorithm may stop, what the value it stops with means, and when the branch-and-bound tree can be skipped. The same argument, with a different subproblem, underlies branch-and-price for crew scheduling, cutting stock and many other set partitioning formulations. Milestone 2 is the observation that turns pricing into a shortest path problem on the original network, and milestone 7 is the preprocessing used before every dynamic program over time windows.

The paper's results are classical and their proofs are short in prose. None of them, nor any VRPTW column generation statement, has a machine-checked proof on the platform; the closest existing items concern split deliveries (Desaulniers 2010) or general finite LP duality. The mission produces a reusable formal model of resource-constrained paths, the set covering LP and its restricted dual, on which later branch-and-price papers can build.

Difficulty

The goal combines three ingredients that do not fit together automatically. First, LP duality for the restricted problem: the hypothesis gives an optimal dual, but optimality over all columns needs equality of the restricted primal and dual values, which is strong duality for a finite LP with equality rows and sign-constrained auxiliary variables. Second, the column set of the full LP is infinite in general: a nonelementary path can repeat customers, so the comparison must go through the finitely many columns a given feasible point uses. Third, the pricing hypothesis is about arc sums along node sequences while the LP is about column costs and visit counts; matching them needs the depot to appear exactly at the two ends of a path.

The tempting shortcut of quantifying the pricing hypothesis over the current columns only gives dual feasibility for the restricted LP, which says nothing about columns not yet generated. The lower bound also fails for arbitrary real costs, because row (4) with $X_c \ge 0$ excludes negative-cost solutions from the LP while the VRPTW still contains them.

Formalization scope

Nodes are Fin (n+1) with the depot 0. A path is the list of its customers; its node sequence is 0 :: p ++ [0], so a path visits at least one customer and meets the depot only at its ends. The arc set is an arbitrary relation; costs, durations, demands and windows are arbitrary reals, and every sign or triangle condition a statement needs appears in its own hypotheses. The committed readings:

• service times are indexed by position (a second-model path may visit a node twice), with $T_0 = 0$;
• the depot's window also applies at the return ($0 \le k \le K+1$, where the page prints $0\le k\le K$);
• the capacity constraint is load $\le Q$ (the page says "less than"; the recurrences and Figure 1 use $\le$);
• a 2-cycle is a pattern of the customer list, so $(d, i, d)$ is not one;
• the LP relaxation keeps $X_d, X_c \ge 0$, relaxes $x_r\in\{0,1\}$ to $x_r\ge 0$ with no upper bound, and is the root LP without branching rows; its dual is that of the restricted LP, with $\pi_i, \pi_d, \pi_c \ge 0$;
• LP points are finitely supported functions on lists (Finsupp); VRPTW solutions are Finsets of routes;
• clauses 2–3 of the goal and milestone 4 assume nonnegative arc costs (the paper's costs are distances);
• milestone 6 adds complete arcs, positive costs, a triangle inequality on durations and nonnegative demands; milestone 7 applies the conditions at customers only; milestone 8 lists $(d,2,1,2,1,d)$ where the page prints $(d,2,1,2,d)$ twice.

The goal is not to be trivialized: the pricing hypothesis ranges over all third-model paths, not the current columns; equality of primal and dual values is not assumed; the full column set is not $R_0$; and "covered exactly once" is not presupposed to mean elementary columns, which must be derived from integrality.

Contributions welcome: proofs of the milestones, a reusable finite LP strong duality interface for Finsupp-indexed columns, and lemmas about arc sums over node sequences.

Selected references

• M. Desrochers, J. Desrosiers, M. Solomon, A new optimization algorithm for the vehicle routing problem with time windows, Operations Research 40(2), 1992, 342–354. https://doi.org/10.1287/opre.40.2.342
• N. Christofides, A. Mingozzi, P. Toth, State-space relaxation procedures for the computation of bounds to routing problems, Networks 11(2), 1981, 145–164. https://doi.org/10.1002/net.3230110207
• D. J. Houck, J.-C. Picard, M. Queyranne, R. R. Vemuganti, The travelling salesman problem as a constrained shortest path problem: theory and computational experience, Opsearch 17, 1980, 93–109.
• G. Desaulniers, Branch-and-price-and-cut for the split-delivery vehicle routing problem with time windows, Operations Research 58(1), 2010, 179–192. https://doi.org/10.1287/opre.1090.0713

Motivation

Generating points uniformly distributed over a bounded region $S\subseteq\mathbb R^n$ is a basic subroutine in Monte Carlo integration, in estimating the volume of a region, in randomized search for optimization, and in identifying redundant constraints of mathematical programs. When $S$ is given only implicitly, for instance by a system of inequalities, the classical methods break down in high dimension: transformation methods need a tractable description of $S$, and rejection from an enclosing box or ball accepts a fraction of proposals that decays exponentially with $n$.

Smith (Oper. Res. 32(6), 1984) studied a family of Markov chain methods, mixing algorithms, that avoid rejection altogether. The best known member is the Random Directions Algorithm, now called hit-and-run: from the current point, pick a direction uniformly at random and move to a uniformly random point of $S$ on the line through the current point in that direction. Boneh and Golan (1979) proposed it for constraint identification and conjectured, without proof, that it generates uniform points; Smith (1980, 1984) proved asymptotic uniformity, and Section 3 of the 1984 paper gives an explicit geometric convergence rate. This mission targets that rate, Theorem 3.

Later work, in particular Lovász (Math. Program. 86, 1999) and Lovász and Vempala (SIAM J. Comput. 35, 2006), proved polynomial mixing bounds for hit-and-run on convex bodies. Smith's bound is exponential in $n$, but it holds for every open bounded region, convex or not, and from every starting point.

Setting

Write $V$ for $n$-dimensional Lebesgue measure (content) on $\mathbb R^n$ and $\|\cdot\|$ for the Euclidean norm. Let $S\subseteq\mathbb R^n$ be open, bounded and nonempty.

• The uniform distribution over $S$ is $\lambda(A)=V(A\cap S)/V(S)$.
• For $x\in S$ and a unit vector $d$, the line set is $L=S\cap\{x+td:t\in\mathbb R\}$, and its length is $\ell(x,d)=\mathrm{Leb}_1\{t: x+td\in S\}$. For convex $S$ this is the chord length; in general $L$ may consist of many segments.
• One step of the Random Directions Algorithm from $x\in S$: draw $d$ uniformly on the unit sphere $\{d:\|d\|=1\}$, then draw $X_{i+1}$ uniformly on $L$. The transition kernel is

$$P(A\mid x)=\int \frac{\mathrm{Leb}_1\{t:x+td\in S\cap A\}}{\ell(x,d)}\,\sigma(\mathrm dd),$$

with $\sigma$ the normalized surface measure of the sphere, and $P^m(A\mid x)=P(X_m\in A\mid X_0=x)$ is its $m$-step iterate.

• $R^\star$ is the radius of the smallest ball containing $S$, $V_n(r)$ the volume of a ball of radius $r$, and

$$\gamma=\frac{V(S)}{V_n(R^\star)}\in(0,1]$$

the fraction of its smallest enclosing ball that $S$ fills.

• $S_n(r)=nV_n(1)r^{n-1}$ is the surface area of a sphere of radius $r$, and $d=\operatorname{diam}S$.

Formalization targets

Goal: Theorem 3 (p. 1304)

For $n\ge2$, every $x\in S$, every measurable $A\subseteq S$ and every $m\ge1$,

$$\bigl|P(X_m\in A\mid X_0=x)-\lambda(A)\bigr|<\Bigl(1-\frac{\gamma}{n\,2^{n-1}}\Bigr)^{m-1}.$$

The constant is the paper's. The bound is uniform in the starting point and in $A$, and it depends on $S$ only through $n$ and $\gamma$.

Milestones (the steps of the paper's proof, in order)

1. Lemma 1 for this algorithm: $\lambda$ is stationary, $\lambda(A)=\int_S P(A\mid x)\,\lambda(\mathrm dx)$.
2. Doob's Case (b) bound: for a chain with stationary law $\pi$ and a minorization $P(A\mid x)\ge\delta\,\varphi(A\cap C)$ on a closed set $C$ that carries $\pi$, $|P^m(A\mid x)-\pi(A)|\le(1-\delta\varphi(C))^{m-1}$.
3. Density formula: $P(A\mid x)=\int_A f(y\mid x)\,\mathrm dy$ with $f(y\mid x)=2/\bigl(S_n(\|y-x\|)\,\ell(x,y)\bigr)$.
4. Density lower bound: $f(y\mid x)>\delta=2/(d\,S_n(d))$ for all distinct $x,y\in S$ when $n\ge2$.
5. Constant comparison: $\delta\,V(S)\ge\gamma/(n2^{n-1})$.

Significance

The result. Theorems 1 and 2 of the paper (the companion mission) establish only that the chain converges to $\lambda$. Theorem 3 makes this quantitative: the deviation from uniformity decays geometrically, at a rate computable from the dimension and the shape ratio $\gamma$ alone. It shows which features of a region govern convergence, it gives a stopping rule with a guarantee, and it holds for non-convex regions, which the later polynomial-time analyses of hit-and-run do not cover. The paper notes the bound is of practical use only in low dimension; its value lies in being explicit and fully general.

Formalizing it. The theorem is proved in the paper, but parts of the proof are heuristic: the density is derived by a limit over small cubes, and the step from $\delta$ to $\gamma$ uses a claim about circumscribed spheres that is false as stated (see below). A machine-checked proof would produce, as reusable components, a general-state-space Doeblin bound (no such theorem currently exists on the platform; the existing Doeblin results are finite-state), a measure-theoretic definition of hit-and-run as a Markov kernel, and the polar-coordinates computation of its density. None of these has, to our knowledge, been formalized.

Difficulty

The obvious argument is: the density is bounded below on $S$, so Doeblin's condition holds, so the chain converges geometrically. Each step hides work. The density is not given by the algorithm but must be derived: the algorithm draws a direction and a scalar, and the change of variables from (direction, signed distance) to the endpoint is two-to-one and carries the Jacobian $\|y-x\|^{n-1}$, which is where $S_n$ and the factor 2 come from. The Doeblin step needs a stationary law and the fact that the chain started in $S$ never leaves $S$. For non-convex $S$, the paper's "diameter along the ray" must be replaced by the measure of the line set, and the maximal chord does not bound the distance $\|y-x\|$; the diameter of $S$ is needed instead. Finally, the paper's assertion that the ball of radius $d/2$ circumscribes $S$ fails already for an equilateral triangle, so the final comparison must go through the smallest enclosing ball's radius $R^\star\ge d/2$.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure. The region is a set S with IsOpen S and Bornology.IsBounded S; boundedness is the paper's standing assumption ("bounded regions").
• The transition law is a Mathlib ProbabilityTheory.Kernel built operationally from the algorithm: the uniform law on the line set, integrated against the normalized surface measure of the unit sphere (Mathlib's Measure.toSphere, divided by its total mass $nV_n(1)$). Off $S$ the kernel is the identity, which the chain started in $S$ never uses. The $m$-step law is the published MarkovChainCLT.iterKernel.
• $\lambda$ is Lebesgue measure restricted to $S$ divided by $V(S)$. $\gamma$ uses the infimum of radii of closed balls containing $S$; the ball is not a free parameter. $\delta=2/(d\,S_n(d))$ is defined from $d=\operatorname{diam}S$, not assumed.
• Deviations from the printed statement. (i) The goal assumes $n\ge2$: for $n=1$ the strict inequality is false (on an interval $X_1$ is already uniform and $\gamma=1$, so both sides vanish for $m\ge2$). (ii) The density uses the line-set length $\ell(x,y)$ instead of "the diameter of $S$ along the ray", which coincides for convex $S$. (iii) The paper's $d=\max_{x,y}d(x,y)$ is taken as $\operatorname{diam}S$. (iv) The Doob step is stated with a kernel-form minorization rather than a lower bound on the density of the absolutely continuous part, which it is implied by, and with $C$ a closed set carrying the stationary law, which is what $C=S$ means inside $\mathbb R^n$. (v) The final comparison is stated as $\delta V(S)\ge\gamma/(n2^{n-1})$, the true inequality behind the paper's false circumscribed-sphere claim. No statement weakens the paper's constant.
• Ruled out. The kernel is not defined through the density formula (which would make milestone 3 definitional and remove the algorithm from the goal), and neither stationarity nor a minorization is a hypothesis of the goal: Theorem 3 assumes only conditions on $n$, $S$, $x$, $A$ and $m$.
• Contributions welcome: the general Doeblin bound, the polar-coordinates density computation (useful for any line-sampling algorithm), and proofs that the kernel is Markov on $S$ and reversible with respect to $\lambda$.

Selected references

• R. L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6):1296–1308, 1984. https://doi.org/10.1287/opre.32.6.1296
• A. Boneh and A. Golan, Constraints' redundancy and feasible region boundedness by random feasible point generator (RFPG), Third European Congress on Operations Research (EURO III), Amsterdam, 1979.
• J. L. Doob, Stochastic Processes, Wiley, 1953 (Case (b), p. 197).
• L. Lovász, Hit-and-run mixes fast, Mathematical Programming 86:443–461, 1999. https://doi.org/10.1007/s101070050099
• L. Lovász and S. Vempala, Hit-and-run from a corner, SIAM Journal on Computing 35(4):985–1005, 2006. https://doi.org/10.1137/S009753970544727X

Motivation

Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).

For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).

Setting

Let $S$ be the state region and $V$ its finite, nonzero content measure. In Smith's geometric setting, $S$ is a bounded $k$-dimensional measurable region in $\mathbb R^n$, and $V$ is $k$-dimensional content; at $k=0$, content is counting measure. A Markov transition kernel $P$ assigns to every current point $x\in S$ a probability $P(x,A)$ of entering a measurable set $A\subseteq S$ on the next move. For the associated chain $(X_0,X_1,\ldots)$, the $m$-step transition probability is $P^m(x,A)=\mathbb P(X_m\in A\mid X_0=x)$.

The uniform law is $\lambda(A)=V(A)/V(S)$. Smith's Assumption (a) gives a measurable transition density $f(y\mid x)$ relative to $V$:

$$P(x,A)=\int_A f(y\mid x)\,V(dy).$$

For a symmetric mixing algorithm, the paper states that this density satisfies $f(y\mid x)=f(x\mid y)$ for all $x,y\in S$. Assumption (b) says $f(y\mid x)>0$ for all such pairs. These are pointwise conditions, including states of zero $V$-measure. A nonempty measurable set $A$ is closed if $P(x,A)=1$ for every $x\in A$. The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).

Formalization targets

Stationarity and indecomposability

Lemma 1 asserts that $\lambda$ is stationary: $\lambda(A)=\int_S P(x,A)\,\lambda(dx)$ for every measurable $A$. Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).

Convergence from every starting point

The mission goal is Smith's Theorem 2. For every $x\in S$ and every measurable $A\subseteq S$,

$$\lim_{m\to\infty}P^m(x,A)=\lambda(A).$$

This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every $n\ge2$, the $n$-step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).

Significance

Theorem 2 makes the uniform law the limiting distribution of the sample at time $m$, for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).

These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.

Difficulty

The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of $P^m(x,A)$. The distinction matters especially at starting points in $V$-null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).

Formalization scope

Lean uses a measurable type $\alpha$ as the whole region $S$, a finite measure $V$ with $V(S)\ne0$, a Markov kernel $P$, and an extended-nonnegative density $f:\alpha\to\alpha\to\mathbb R_{\ge0}^{\infty}$. The density is jointly measurable and is linked to $P$ by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.

The uniform law is normalized by $V(S)$. Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The $m$-step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every $x$, rather than $\lambda$-almost every $x$, and uses setwise convergence on each measurable $A$. No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching $f$ from $P$ would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.

Selected references

• Robert L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6), 1296–1308, 1984. DOI: 10.1287/opre.32.6.1296.

Motivation

A seller with one indivisible object must decide whether to keep it or transfer it to one of several bidders whose values she does not observe. The allocation and the payment rule affect what bidders choose to report. Myerson's 1981 paper identifies a revenue-maximizing rule when bidders' private value estimates are independent, their densities are positive, and their valuations may be revised after learning other bidders' information. It covers value distributions for which the usual virtual-value rule is not monotone, by replacing each bidder's virtual value with an ironed priority level.

The question matters to auction design because a pointwise revenue-maximizing assignment can reward a bidder for understating a value. The seller must maximize expected utility subject to both incentive compatibility and each bidder's ability to decline participation. The paper's main theorem gives a specific allocation and payment pair that meets those constraints and attains the maximum. The result is proved in the source; this mission asks for a machine-checked formalization of it.

Setting

There is a finite nonempty set $N$ of bidders and one seller. Bidder $i$ has a value estimate $t_i$ in a finite interval $[a_i,b_i]$, where $a_i<b_i$; endpoints may be negative and may differ between bidders. The continuous density $f_i$ is strictly positive on that interval and has total integral one. The bidders' estimates are independent, so a profile $t=(t_i)_{i\in N}$ has density $f(t)=\prod_i f_i(t_i)$ on $T=\prod_i[a_i,b_i]$. Write $F_i(s)=\int_{a_i}^{s}f_i(u)\,du$ for the distribution function. The seller's known value for keeping the object is $t_0$.

A revision effect $e_j(t_j)$ describes the change in everyone else's valuation after bidder $j$'s estimate becomes known. Bidder $i$'s revised value is $v_i(t)=t_i+\sum_{j\ne i}e_j(t_j)$, while the seller's is $v_0(t)=t_0+\sum_j e_j(t_j)$. A direct mechanism assigns each profile an allocation probability $p_i(t)$ and expected payment $x_i(t)$ for each bidder. Payments may be negative and need not vanish when a bidder loses. Its feasibility conditions say that allocation probabilities are nonnegative and sum to at most one, each bidder's interim expected utility is nonnegative at every possible value, and truthful reporting yields at least as much interim utility as any other report. The seller maximizes her expected utility over all feasible mechanisms.

The virtual value is $c_i(s)=s-e_i(s)-(1-F_i(s))/f_i(s)$. In the general case it need not increase with $s$. Myerson transforms $c_i$ through the quantile $q=F_i(s)$: $h_i(q)=c_i(F_i^{-1}(q))$, $H_i(q)=\int_0^q h_i(r)\,dr$, and $G_i$ is the convex envelope of $H_i$ on $[0,1]$. The slope $g_i$ of $G_i$, extended across kinks, gives the ironed priority $\bar c_i(s)=g_i(F_i(s))$. At profile $t$, the winning set $M(t)$ contains exactly those bidders whose priority is maximal and at least $t_0$.

Formalization targets

The goal is Myerson's §6 theorem. The proposed rule shares the object equally among bidders in $M(t)$, or keeps it when $M(t)$ is empty, and charges each bidder the envelope payment:

$$\bar p_i(t)=\begin{cases}|M(t)|^{-1},&i\in M(t),\\0,&i\notin M(t),\end{cases} \qquad \bar x_i(t)=\bar p_i(t)v_i(t)-\int_{a_i}^{t_i}\bar p_i(t_{-i},s)\,ds.$$

The target asserts that $(\bar p,\bar x)$ is feasible and that every feasible $(p,x)$ has seller utility no greater than that of $(\bar p,\bar x)$. The milestone list follows the paper's reduction: Lemma 2 characterizes feasible direct mechanisms by a monotone interim allocation rule and an envelope identity; equation (4.12) rewrites seller utility using virtual values; Lemma 3 turns maximization of virtual surplus into optimality. Equations (6.9)–(6.13) compare virtual and ironed priorities and establish the optimality and monotonicity of the proposed allocation.

Significance

The theorem specifies both who receives the object and how payments are computed, including irregular distributions and bidder-specific supports. The ironed priorities preserve incentives while retaining the seller's maximal expected utility. Equation (4.12) also gives the revenue-equivalence consequence: once the allocation rule and each lowest-type interim utility are fixed, expected seller utility is fixed.

A formal proof would connect several reusable results: product distributions with bidder-specific densities, interim incentive constraints, an envelope characterization, virtual-surplus accounting, and one-dimensional convex ironing. The source theorem and milestones are currently statements to be proved in this development, not existing machine-checked results. Related Börgers auction statements on Prove2Me use a common nonnegative support, at least two bidders, zero revision effects, and zero seller value; they do not provide this general theorem.

Difficulty

Maximizing virtual surplus at each profile is straightforward only if each bidder's virtual value rises with her report. When it falls, the resulting win probability can also fall, violating the incentive constraint. Replacing virtual values by slopes of a convex envelope restores monotonicity, but then the proof must account exactly for the difference between the original and ironed objectives, including flat portions of the envelope. Payments must satisfy the interim envelope identity for every type, while the seller's objective includes both transfers and her value for retaining the object.

Formalization scope

The Lean model uses a finite nonempty bidder type, real-valued reports and payments, one object, independent continuous positive densities normalized on each finite support, and continuous revision effects. The latter regularity is implicit in the paper's assertion that $c_i$ is continuous. No mean-zero condition on revision effects is imposed: the paper explicitly says its equation (2.9) is unnecessary. One bidder, negative support endpoints, unequal supports, and arbitrary seller value remain allowed.

The profile law is Lebesgue measure restricted to $T$ and weighted by the product density. Integrating a function after replacing coordinate $i$ represents the $T_{-i}$ integral, because bidder $i$'s marginal density has mass one. Mechanisms are total functions, but allocation and incentive conditions quantify over supported profiles and reports. Feasibility explicitly requires integrability of allocations, payments, and their report sections so no undefined Bochner expectation can acquire Lean's default value zero. The convex envelope is the two-point infimum of equation (6.3); its defining set is nonempty and bounded below on $[0,1]$. The slope uses the right derivative below quantile one and the left derivative at one. The theorem requires feasibility of the proposed pair as well as its utility bound, ruling out an empty or unconstrained maximization claim.

The Stieltjes expressions in (6.9), (6.12), and (6.13) are combined into equivalent ordinary-integral comparisons over the profile law. A complete proof needs the one-dimensional envelope theorem, product-measure integration and Fubini results, differentiation of the convex envelope, and a careful endpoint treatment. The definitions of interim utilities and ironing can be reused for related auction models; contributions that establish these analytic components or the listed source lemmas are in scope.

Selected references

• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. DOI: 10.1287/moor.6.1.58.

Motivation

Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.

The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).

Setting

A circuit is a finite sequence of triples $C=((a_i,b_i,c_i),\ i=1,\dots,k)$ with $k\ge1$. Each $a_i$ is one of the operations false, true, and, or. A triple with $a_i\in\{\text{false},\text{true}\}$ is an input; a triple with $a_i\in\{\text{and},\text{or}\}$ is a gate, and a gate reads two earlier triples, $1\le b_i,c_i<i$. The value of an input is its constant; the value of a gate is the Boolean operation $a_i$ applied to the values of triples $b_i$ and $c_i$. The value of $C$ is the value of triple $k$.

A finite Markov decision process has a finite state set $S$, an initial state $s_0$, and at each state $s$ a nonempty finite set $D_s$ of decisions. Taking decision $i$ at state $s$ at time $t$ costs $c(s,i,t)$ and moves to $s'$ with probability $p(s,s',i,t)$. A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state and time. For a horizon $T$ the expected cost of $\delta$ is

$$J_T(\delta)=\mathbb E_\delta\Bigl[\sum_{t=0}^{T}c\bigl(s_t,\delta(s_t,t),t\bigr)\Bigr],$$

and the optimal expected cost is $J_T^\ast=\inf_\delta J_T(\delta)$ over all policies.

From a circuit $C$ the proof of Theorem 1 builds a stationary process $M_C$: one state per triple plus an absorbing state $q$. An input state has one decision, moving to $q$, at cost $1$ if the input is false and $0$ if it is true. An or gate has two free decisions, $0$ moving to $b_i$ and $1$ moving to $c_i$. An and gate has one decision, moving to $b_i$ or $c_i$ with probability $1/2$ each. All other costs are zero. The initial state is triple $k$ and the horizon is $T=k$.

In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.

Formalization targets

Goal: correctness of the reduction

$$J_k^\ast(M_C)\le 0\quad\Longleftrightarrow\quad \text{the value of } C \text{ is true},$$

for every circuit $C$ with $k\ge1$ triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of $C$ was true" on p. 445.

Milestones

1. Every policy has $J_k(\delta)\ge0$ ("it cannot be less").
2. For any finite process with nonnegative costs, $J_T(\delta)=0$ iff no positive cost is incurred on any trajectory of positive probability ("the states with positive costs are impossible to reach").
3. If some policy has $J_k(\delta)=0$, then $C$ is true.
4. If $C$ is true, some policy has $J_k(\delta)=0$.

Further statement

The discounted analogue, which the paper asserts in one sentence: for $\beta\in(0,1)$, the optimal expected discounted cost $\inf_\delta\sum_{t\ge0}\beta^t\,\mathbb E_\delta[c(s_t,\delta(s_t,t))]$ of $M_C$ is at most $0$ iff $C$ is true (discounted_reduction).

Significance

Combined with the log-space computability of $M_C$ from $C$, the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.

The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.

Difficulty

The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.

Formalization scope

Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.

Conventions committed to:

• Triples are indexed by Fin k (paper index $i$ is Lean index $i-1$); $k\ge1$ via [NeZero k]. The fields $b_i,c_i$ of an input are unused (the paper sets them to $0$, not a triple index). Triple $k$ need not be a gate.
• States of $M_C$ are Option (Fin k), with none the state $q$; decisions are Fin 2 at or gates and Fin 1 elsewhere.
• The and-gate row is $\tfrac12\mathbf 1[s'=b_i]+\tfrac12\mathbf 1[s'=c_i]$, so that $b_i=c_i$ (allowed by the paper) gives a probability vector.
• Rows of the transition kernel are probability vectors and every $D_s$ is nonempty (implicit in the paper, explicit here).
• The expected cost is a finite sum over trajectories, with the §2 horizon convention $\sum_{t=0}^{T}$ and $T=k$. The optimum is a real infimum over all policies $\delta(s,t)$, not over stationary ones.
• The discounted cost is $\sum_t\beta^t$ times the expected time-$t$ cost, which equals the expectation of the discounted series for bounded nonnegative costs.

A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.

Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time $T$) that are reusable for any finite-horizon process.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3) (1987) 441–450. https://doi.org/10.1287/moor.12.3.441
• R. E. Ladner, The Circuit Value Problem is Log Space Complete for P, SIGACT News 7(1) (1975) 18–20. https://doi.org/10.1145/990518.990519
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of $1-1/e$ for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).

The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.

Setting

There are $n$ boys, represented by rows, and $n$ girls, represented by columns. A bipartite graph $G\subseteq[n]\times[n]$ records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of $G$. This assumption supplies an offline benchmark of $n$ matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.

Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order $n,n-1,\ldots,1$. A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance $p(A)$ is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).

The paper's hard family begins with the complete upper-triangular graph $T_n$, where row $i$ is adjacent to column $j$ exactly when $i\le j$. Its columns arrive from largest to smallest. Relabeling the rows by a permutation $\pi$ gives an instance $T_\pi$ that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write $V_{T_n}(n,\varnothing)$ for RANDOM's expected number of matches on $T_n$, beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).

Formalization targets

Main theorem

For every $\varepsilon>0$, there is one threshold $N$ such that, for every $n\ge N$ and every randomized online algorithm $A$ on $n$ rows and columns, a graph $G$ with a perfect matching satisfies

$$\mathbb E_A[|M(G)|]\le (1-e^{-1}+\varepsilon)n.$$

The threshold is uniform over algorithms. The graph may depend on $A$. This is the quantified upper-bound reading of Theorem 2's $p(A)\le n(1-1/e)+o(n)$ (Karp, Vazirani, and Vazirani, 1990, Theorem 2).

Milestone statements

Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted $T_n$ with RANDOM's expected size on $T_n$. Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit

$$\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.$$

Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).

Significance

Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from $n$ is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.

Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.

Difficulty

For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the $o(n)$ claim in Lemma 16.

Formalization scope

Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order $n,\ldots,1$ is represented by zero-based order $n-1,\ldots,0$; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.

RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For $n=0$, the matching and RANDOM value are zero; the main theorem is eventual in $n$ and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's $o(n)$ in Theorem 2 is stated as $\forall\varepsilon>0,\exists N,\forall n\ge N$ with $N$ before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.

Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.

Selected references

• Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, pp. 352–358, 1990. DOI: 10.1145/100216.100262.

Motivation

Many decision problems in control, finance and engineering must hold against an uncertain parameter $\delta$ whose distribution is unknown, while samples of $\delta$ (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the $N$ observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen $\delta$ violate it?

The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on $N$ and the dimension $d$, and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than $d$ samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.

Timeline:

• 2005–2006, Calafiore and Campi: a convex scenario program in $\mathbb R^d$ has at most $d$ support constraints; first sample-size bounds.
• 2008, Campi and Garatti: the exact bound $\mathbb P^N\{V(x^*_N)>\epsilon\}\le\sum_{i=0}^{d-1}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$, with equality for fully-supported problems.
• 2018, Campi and Garatti: the wait-and-judge bound, Theorem 1 below, with the 2008 bound as a corollary.

Setting

The decision variable is $x\in\mathbb R^d$. A problem consists of a cost vector $c\in\mathbb R^d$, a convex domain $\mathcal X\subseteq\mathbb R^d$, convex constraint sets $\mathcal X_\delta\subseteq\mathbb R^d$ indexed by $\delta$ in a probability space $(\Delta,\mathcal F,\mathbb P)$, and convex tie-break functions $t_1,\dots,t_p$. Given an i.i.d. sample $\delta^{(1)},\dots,\delta^{(N)}$ with $N>d$, the scenario program is

$$\min_{x\in\mathcal X}\ c^{\mathsf T}x\quad\text{subject to}\quad x\in\bigcap_{i=1}^N\mathcal X_{\delta^{(i)}}.$$

Ties are broken by minimising $t_1$ among the minimisers, then $t_2$, and so on; the resulting solution is $x^*_N$.

• The violation of a point is $V(x)=\mathbb P\{\delta\in\Delta: x\notin\mathcal X_\delta\}$.
• A constraint is a support constraint if removing it changes the solution; $s^*_N$ is their number.
• Assumption 1: for every $m$ and every sample of size $m$, the program with those $m$ constraints has a unique tie-broken solution.
• Assumption 2 (non-degeneracy): for every $m$, with probability one, keeping only the support constraints does not change the solution.

The variational problem (10) is: for a function $\epsilon:\{0,\dots,d\}\to[0,1]$,

$$\gamma^*=\inf_{\xi\in C^d[0,1]}\xi(1)\quad\text{s.t.}\quad\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}\xi(t)\ge\binom Nk t^{N-k}\,\mathbf 1_{[0,1-\epsilon(k))}(t),\ \ t\in[0,1],\ k=0,\dots,d.$$

Formalization targets

Goal: Theorem 1 (p. 10)

For every $[0,1]$-valued $\epsilon(k)$, under Assumptions 1 and 2,

$$\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}\ \le\ \gamma^*.$$

The level $\epsilon$ is evaluated at the observed number of support constraints. The goal fixes no particular $\epsilon$, which keeps it stable under any later choice of levels.

Milestones (the proof of Theorem 1, Sect. 5.1)

1. $s^*_m\le d$ for every sample (quoted from [7]).
2. (14): $\mathbb P^N\{V(x^*_N)>\epsilon(k)\wedge s^*_N=k\}=\binom Nk\,\mathbb P^N\{A\}$, where $A$ adds "the first $k$ constraints are of support".
3. $A=B$ up to a null set, where $B$ concerns the program on the first $k$ samples.
4. (16): $\mathbb P^N\{A\}=\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$, with $F_k(v)=\mathbb P^k\{V(x^*_k)\le v\wedge s^*_k=k\}$.
5. (17): $\mathbb P^N\{V(x^*_N)>\epsilon(s^*_N)\}=\sum_{k=0}^d\binom Nk\int_{(\epsilon(k),1]}(1-v)^{N-k}\,\mathrm dF_k(v)$.
6. (18): $\sum_{k=0}^{\min\{m,d\}}\binom mk\int_{[0,1]}(1-v)^{m-k}\,\mathrm dF_k(v)=1$ for every $m$.
7. Weak duality between the truncated moment problem (20) and its dual (21), giving (22).
8. (23): $\frac1{k!}\frac{\mathrm d^k}{\mathrm dt^k}t^m=\binom mk t^{m-k}$ for $m\ge k$, and $0$ otherwise.
9. (24): the infimum of $p(1)$ over polynomials feasible for (10) equals $\gamma^*$.

Companions

• Theorem 2 (p. 11): for $\beta\in(0,1)$ and $\epsilon(k)=1-t(k)$, with $t(k)$ the unique root in $(0,1)$ of $\frac{\beta}{N+1}\sum_{m=k}^N\binom mk t^{m-k}-\binom Nk t^{N-k}=0$, the probability is at most $\beta$.
• The root lemma of Sect. 5.3, including its sign and divergence claims.
• $\gamma^*\le\sum_{i<d}\binom Ni\epsilon^i(1-\epsilon)^{N-i}$ for constant $\epsilon$ (Sect. 5.2).
• Corollary 1, the 2008 bound.

Significance

Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of $\epsilon(k)$, a user who finds $k\ll d$ support constraints obtains a level $\epsilon(k)$ comparable to that of a $k$-dimensional problem, which is far below the a-priori level for dimension $d$. The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.

The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:

• a formal account of scenario programs with lexicographic tie-break and of support constraints in the "changes the solution" sense;
• the exchangeability argument (14) on product measures;
• the representation (17) of a tail probability through generalized distribution functions;
• a weak-duality argument for a generalized moment problem. The 2008 bound itself is posed on the platform as an open problem under other hypotheses; Corollary 1 states it under this paper's assumptions.

Difficulty

The obvious approach bounds the probability for each value of $s^*_N$ separately by a binomial tail, then sums. This fails: the event $s^*_N=k$ is not known in advance, and summing the individual bounds over $k$ loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the $(d+1)$-tuple $(F_0,\dots,F_d)$. It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in $d+1$ measures, and solves it by duality.

Two steps carry most of the work. One is the almost-sure identity $A=B$, which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in $C^d[0,1]$. The bound $s^*_N\le d$ itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.

Formalization scope

• Spaces. The decision space is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from $0$. $\mathbb P$ is a probability measure and $\mathbb P^N$ is the product measure.
• Tie-break. The tie-broken solution is the lexicographic minimiser of $(c^{\mathsf T}x,t_1(x),\dots,t_p(x))$ and depends only on the feasible set, which is what makes the exchangeability step valid. A support constraint is one whose removal changes this solution; this is not the platform's earlier "removal lowers the cost" notion.
• Assumptions. Assumption 1 is required for every sample, Assumption 2 almost surely.
• Measurability. The paper takes measurability for granted (footnote 1). Here it is two explicit hypotheses: the relation $\{(x,\delta):x\in\mathcal X_\delta\}$ is measurable, and every solution map $\omega\mapsto x^*_m(\omega)$ is measurable. No event is assumed measurable directly.
• $F_k$. $F_k$ is the finite measure on $\mathbb R$ given by the law of $V(x^*_k)$ on the event $\{s^*_k=k\}$; it is not normalised.
• Problem (10). $C^d[0,1]$ is ContDiffOn ℝ d on $[0,1]$, with derivatives taken within $[0,1]$. $\gamma^*$ is a real infimum over a set that is nonempty ($\xi(t)=t^N$) and bounded below by $0$.
• Probabilities are compared with real quantities through ENNReal.ofReal.
• Theorem 2 is stated for every $\epsilon$ whose values $1-\epsilon(k)$ are roots of (11) in $(0,1)$, which by its first part is the paper's $\epsilon$.
• Added hypothesis. The constant-$\epsilon$ companion assumes $d\ge1$: at $d=0$, $\epsilon=0$ its inequality is false.

Ruled-out trivializations:

• The solution is never a free function of the sample.
• The goal does not mention $F_k$, moments or polynomials.
• Assumption 1 is not weakened to almost surely.
• $N>d$ is kept on Theorems 1, 2 and Corollary 1.
• The indicators keep the paper's open and closed ends: $[0,1-\epsilon(k))$ in (10), $(\epsilon(k),1]$ in (16)–(21).

Contributions welcome:

• the support-constraint bound under lexicographic tie-break, which is reusable for any convex scenario result;
• the exchangeability lemma on Measure.pi;
• the duality and density lemmas, which are pure analysis.

Selected references

• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming 167 (2018). https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102 (2005). https://doi.org/10.1007/s10107-003-0499-y
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51 (2006). https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19 (2008). https://doi.org/10.1137/07069821X