The OR Formalization Drive

Why the timing of a markdown matters

A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.

The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.

Prices, demand, and admissible switches

Let $n\ge1$ be the initial stock and $t\ge0$ the time to go. The seller first charges price $p_1$ and may change once to a lower price $p_2$. Demands at the two prices are independent Poisson counts with positive rates $\lambda_1$ and $\lambda_2$. A lower price produces more arrivals, so $p_2<p_1$ and $\lambda_1<\lambda_2$. Feng and Gallego also assume that lowering the price increases the revenue rate: $p_1\lambda_1<p_2\lambda_2$. There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.

Write $N_1(s)$ for the observed sales count at the initial price by time $s$. If the price changes at deterministic time $s\in[0,t]$, let $J(n,t;s)$ be the expected total revenue. The count after the change is independent of $N_1(s)$, and their sum has Poisson mean $\lambda_1s+\lambda_2(t-s)$. The optimal value $J(n,t)$ allows the switch time $\tau$ to depend on the counts observed so far. An admissible $\tau$ lies between zero and $t$, is a stopping time for the history of $N_1$, and occurs before stock is exhausted almost surely. At $s=0$, $J(n,t;0)$ is the revenue from charging $p_2$ immediately. The paper defines these quantities in §3, pp. 1377–1379.

Formalization targets

The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence $x_1<x_2<\cdots$ of inventory-dependent thresholds. When $t\le x_n$, switching immediately earns the optimal value; when $t>x_n$, a correction $F(n,t)$ is added:

$$J(n,t)=\begin{cases} J(n,t;0),&t\le x_n,\\ J(n,t;0)+F(n,t),&t>x_n. \end{cases}$$

The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with $F(0,t)=0$. For $n\ge1$, set $L(n,t)=G(n,t)+\lambda_1F(n-1,t)$, where $G$ is the Poisson-tail expression from §4.1. The threshold $x_n$ is the first nonnegative zero of $L(n,\cdot)$. A function $H(n,\cdot)$ satisfies $\partial_tH=-\lambda_1H+L$ for positive time and $H(n,x_n)=0$; $F$ is zero below $x_n$ and equals $H$ at and above it. If $y_n$ is the first zero of $G(n,\cdot)$, the theorem also gives $x_1=y_1$ and $x_n<y_n$ for $n>1$.

Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of $G$ in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.

What the result provides

The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.

The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.

Where the mathematics is difficult

The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory $n$ depends on the correction at stock $n-1$. Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of $G$, the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.

The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.

Formalization scope

Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.

The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.

For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.

Selected references

• Y. Feng and G. Gallego, Optimal Starting Times for End-of-Season Sales and Optimal Stopping Times for Promotional Fares, Management Science 41(8), 1995, pp. 1371–1391. DOI: 10.1287/mnsc.41.8.1371.

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

Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time $t$ leaves it at time $\tau(t)$. The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.

Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.

Timeline:

• 1969. Vickrey's bottleneck model introduces deterministic queueing at a single bottleneck (Vickrey 1969).
• 1986. Ben-Akiva and De Palma show (Trans. Sci. 20 (1986)), for uniform entry rates and deterministic queueing delays, that it is not possible to "arrive earlier by departing later".
• 1993. Friesz et al. prove (Theorem 1, p. 185) that for every linear arc delay $D = \alpha x + \beta$ the exit time is strictly increasing, extending the 1986 result to all continuous entry-rate patterns (remark, p. 186).

Setting

Consider one arc. Vehicles enter it at the entry rate $u(t) \ge 0$, a continuous function of time $t \ge 0$; the first vehicle enters at time $0$. For an exit-time function $\tau$, the arc volume at time $t \ge 0$ is the inflow mass of the vehicles that entered during $[0,t]$ and have not left by time $t$:

$$x(t) = \int_{\{s \in [0,t]\,:\,\tau(s) > t\}} u(s)\,ds .$$

The linear delay function (18) of the paper is

$$D(t) = \alpha\, x(t) + \beta, \qquad \alpha, \beta > 0,$$

a fixed free-flow travel time $\beta$ plus a queueing time determined by the service rate $1/\alpha$. The exit time is entry time plus delay, so $\tau$ is pinned by the exit-time equation

$$\tau(t) = t + \alpha\, x(t) + \beta \qquad (t \ge 0).$$

The equation is implicit: $\tau$ appears on the right through the volume. The proof partitions time at $t_0 = 0$, $t_{n+1} = \tau(t_n)$; in particular $t_1 = \tau(0) = \beta$ is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.

Formalization targets

Goal: Theorem 1 (p. 185)

For $\alpha, \beta > 0$ and a nonnegative continuous entry rate $u$, every $\tau$ satisfying the exit-time equation is strictly increasing on $[0, \infty)$:

$$0 \le s < t \implies \tau(s) < \tau(t),$$

and hence injective there, so $\tau^{-1}$ exists.

Milestones

1. Lemma 1 (19): for a differentiable invertible $f$, $[f^{-1}]'(z) = 1/f'[f^{-1}(z)]$.
2. First interval (21)–(24): $t_1 = \beta$; on $[0, t_1]$, $x(t) = \int_0^t u$, $\tau(t) = t + \alpha\int_0^t u + \beta$, and $\tau' = 1 + \alpha u > 0$.
3. Second interval (25)–(28): on $[t_1, t_2]$, $\tau(t) = t + \alpha\int_{\tau^{-1}(t)}^t u + \beta$ and $\tau'(t) = \alpha u(t) + 1/(1 + \alpha u[\tau^{-1}(t)]) > \alpha u(t)$.
4. Induction (29)–(34): the same representation and $\tau'(t) > \alpha u(t)$ on every $[t_{n+1}, t_{n+2}]$, with $\tau$ strictly increasing there.
5. Covering: $t_{n+1} - t_n \ge \beta$ and $\mathbb R_+ = \bigcup_{n \ge 0}[t_n, t_{n+1}]$.

A supporting, non-milestone item states that the exit-time equation has a solution for every admissible $u$.

Significance

The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.

Difficulty

The obvious argument differentiates $\tau(t) = t + \alpha x(t) + \beta$ and bounds the outflow rate. But the volume can only be written as $\int_{\tau^{-1}(t)}^t u$ once $\tau$ is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on $[t_n, t_{n+1}]$ the volume depends only on $\tau$ restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions $t_n$, where $\tau$ is generally not differentiable, and show that the junctions do not accumulate.

Formalization scope

Time is real; the entry rate is a function $u : \mathbb R \to \mathbb R$ with $u(t) \ge 0$ and $u$ continuous on $[0, \infty)$. Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on $[0,\infty)$ only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval $[t_n, t_{n+1}]$. The paper's separate pieces $\tau_k$ are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis $f'[f^{-1}(z)] \ne 0$, without which it is false.

The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through $\tau^{-1}$ or assumed $\tau$ monotone would assume the conclusion and is ruled out.

The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation 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
• M. Ben-Akiva and A. de Palma, Some circumstances in which vehicles will reach their destinations earlier by starting later: revisited, Transportation Science 20(1):52–55, 1986. https://doi.org/10.1287/trsc.20.1.52
• M. Ben-Akiva, A. de Palma and P. Kanaroglou, Dynamic model of peak period traffic congestion with elastic arrival rates, Transportation Science 20(3):164–181, 1986. https://doi.org/10.1287/trsc.20.3.164
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–261, 1969. https://www.jstor.org/stable/1823678

Motivation

A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).

This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule $S_n$ for the first $n$ tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).

For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of $S_n$ has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).

The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.

Difficulty

Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

• Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
• Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
• Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$. Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$. A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$, either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$. Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$, and the total discrepancy of $S$ is

$$\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .$$

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$.

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$, is there a schedule with $\mathrm{cost}(S)\le k$?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$, can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$, write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$. A schedule is ordered if, on each side of $M$, shorter tasks lie nearer to $M$. The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

$$\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}$$

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

1. Even-odd partition is in NP; the instance $x_1=1$, $x_{2i}=x_{2i-1}+y_i$, $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
2. The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$), LEMMA 3 ($|A(S)|=|B(S)|$), LEMMA 4 ($m_0(S)=M$), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ($\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

$$k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .$$

3. At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$; equality forces the ordered, gap-free form in item 2.
4. The reduction: the instance D with $l_0=x_1-1$, $l_i=x_i$, $l_{2n+1}=2$, $M_j=M=\sum_{i\le 2n}l_i/2$, $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$, the $i$-th pair of lengths in the $i$-th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$, so they must be restated for every $M$. Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$, exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$, and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$. Together these force the two sides to have equal total length. A proof that only cites the large-$M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$.

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$, double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

• Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$, and integer data are cast to $\mathbb R$. Restricting to integer starting times would be a different problem and is not what is stated.
• Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
• Tasks are indexed by Fin N from $0$. In the special case $T_i$ is index $i$, and the paper's $T_{2i-1},T_{2i}$ ($1\le i\le n$) are the indices $2k+1,2k+2$ for $k=i-1$.
• Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
• The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
• Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
• N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf