Updated: 2026-09-07
Formalized. The selected surface covers Appendix (A-1) and Theorems 1–4 of the stationary priority-pricing model. Theorem 3 uses the source’s stationary feasible-flow domain and its PTD schedule-and-assignment notion.
Haim Mendelson and Seungjin Whang, Optimal Incentive-Compatible Priority Pricing for the M/M/1 Queue, Operations Research 38(5), 1990, pp. 870–883. The selected results concern stationary priority queueing, marginal-externality pricing, homogeneous and time-dependent priority pricing, and cheating penalties.
| Result | Comparison with source |
|---|---|
| Appendix (A-1) | Exact. |
| Theorem 1 | Exact for interior domain. The selected class has positive optimal arrival rate. Condition. |
| Theorem 2 | Exact for strict domain. Every class has positive arrival rate. Condition. |
| Theorem 3 | Exact for strict domain. Every class has positive arrival rate. Condition. |
| Theorem 4 | Exact for strict domain. Every class has positive arrival rate. Condition. |
None for the selected current targets. The archival zero-flow formulations of the strict conclusions are not claimed as strict results; the source clarification explains the relevant adjacent-flow factor.
None.
The PTD argument separates the expected direct charge of a reported priority from the customer’s own service-time law, then compares total expected costs through a single penalty difference. This keeps incentive compatibility tied to the schedule itself rather than to a preselected reported class.
A boundary extension could state weak best-response and weak penalty conclusions at zero-flow priority levels. It is not needed for the selected strict interior targets.
The source clarification memo gives the positive-flow interior reading for Theorem 1 and the strict-comparison reading for Theorems 2–4.
The strict priority comparisons are interior statements. At an unused adjacent priority level, the displayed comparison factor can vanish; this does not affect the checked full-positive stationary result.
The paper-facing interface has five transparent result targets with exact proof endpoints: Appendix (A-1) and Theorems 1–4. The PTD optimality definition is represented directly as source semantic context for Theorem 3.
The source model supplies stationary Poisson arrivals, positive exponential service means, nonpreemptive priority, nonnegative flow, and strict offered load stability. Theorem-specific positive-flow conditions are documented in the source clarification memo.
The source map records the stationary queueing formula, marginal externality price, homogeneous and PTD prices, and cheating penalty against their source passages.
The reusable layer supplies stationary marked-Poisson inputs, selected-arrival service laws, nonpreemptive-priority work accounting, and finite mean-wait algebra. The pricing schedules and numbered theorem statements remain paper-specific.
The dependency DAG follows the source order from the queueing model and welfare objective through Theorem 1, the homogeneous route, and the PTD route to Theorems 2–4. The PTD equilibrium criterion and Theorem 3 are shown as formalized nodes. The rendered DAG was visually inspected for readable labels, arrowheads, reading order, and node or edge overlap.
The selected source statements, semantic prerequisites, and complete paper build have passed their recorded checks. Final adversarial review and strict closeout are complete; see the accepted record.
Checked definitions include stationary class input, priority queueing time, the net-value objective, marginal externality, homogeneous and time-dependent prices, expected total cost under a declared priority, the PTD equilibrium criterion, and the cheating penalty.
The source-to-Spec ledger records the current direct statement review. The paper and library prerequisite ledgers record the source-semantic conditions used by those targets.
The source map retains five selected result routes and the source definitions that provide their semantic context. The result table in Section 4 and the source clarification memo record the only material target qualifications.