Motivation

Stock exchanges, commodity markets and trading platforms are institutions for trade between parties who each know something the other does not. The simplest version is bilateral trade: one seller, one buyer, one indivisible good, and each side privately knows its own value. The question is whether any trading institution can make the two trade exactly when trade is efficient, with both taking part voluntarily and without a subsidy from outside. Myerson and Satterthwaite (1983) showed that, apart from trivial cases, none can. The result is one of the basic impossibility theorems of economic theory. It explains why bargaining under private information is inefficient, and it is the benchmark every later analysis of double auctions and market design compares against.

This mission formalizes Section 3.4 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015): the impossibility theorem, the pivot-mechanism argument that proves it, the second-best and profit-maximizing trading mechanisms, and the uniform example.

Timeline. Vickrey (1961) noted the tension between efficiency and budget balance in markets with private values. Chatterjee and Samuelson (1983) studied the sealed-offer double auction and its linear equilibrium for uniform values. Myerson and Satterthwaite (1983) proved the impossibility for general independent distributions with overlapping supports, and computed the second-best mechanism; for uniform values it coincides with the Chatterjee–Samuelson linear equilibrium. Börgers (2015) gives the pivot-mechanism proof formalized here.

Setting

A seller $S$ owns one indivisible good; a buyer $B$ may buy it. The seller's value $\theta_S$ has distribution $F_S$ with density $f_S > 0$ on $[\underline\theta_S, \overline\theta_S]$; the buyer's value $\theta_B$ has distribution $F_B$ with density $f_B > 0$ on $[\underline\theta_B, \overline\theta_B]$. The two intervals are nondegenerate and may differ, and the values are independent. The seller's utility is $t$ if she sells for $t$ and $\theta_S + t$ if she keeps the good and receives $t$; the buyer's is $\theta_B - t$ if he buys and pays $t$, and $-t$ otherwise.

A direct mechanism is a trading rule $q : \Theta \to \{0,1\}$ on $\Theta = [\underline\theta_S, \overline\theta_S] \times [\underline\theta_B, \overline\theta_B]$ and transfers $t_S$ (received by the seller) and $t_B$ (paid by the buyer). Conditioning on one agent's type gives the interim trade probabilities $Q_S, Q_B$, the interim transfers $T_S, T_B$, and the interim utilities $U_S(\theta_S) = T_S(\theta_S) + (1 - Q_S(\theta_S))\theta_S$ and $U_B(\theta_B) = Q_B(\theta_B)\theta_B - T_B(\theta_B)$. The mechanism is incentive-compatible if truthful reporting is a Bayesian equilibrium, individually rational if $U_S(\theta_S) \ge \theta_S$ and $U_B(\theta_B) \ge 0$ for all types, ex post budget balanced if $t_S(\theta) = t_B(\theta)$ for every $\theta$, and ex ante budget balanced if $\mathbb E[t_S] = \mathbb E[t_B]$. A first-best trading rule trades when $\theta_B > \theta_S$ and not when $\theta_B < \theta_S$, with any choice at ties. The seller's virtual cost is $\psi_S = \theta_S + F_S/f_S$ and the buyer's virtual valuation is $\psi_B = \theta_B - (1 - F_B)/f_B$; the distributions are regular if both are increasing.

Formalization targets

Goal: Proposition 3.12 (Myerson–Satterthwaite)

An incentive-compatible, individually rational and ex post budget balanced direct mechanism with a first-best trading rule exists if and only if

$$\underline\theta_B \ge \overline\theta_S \quad\text{or}\quad \underline\theta_S \ge \overline\theta_B .$$

Milestones

• Lemmas 3.9–3.11. The pivot mechanism is incentive-compatible and individually rational. Among all such mechanisms that implement a first-best rule, it maximizes $\mathbb E[t_B - t_S]$. That quantity is negative whenever $\underline\theta_B < \overline\theta_S$ and $\overline\theta_B > \underline\theta_S$.
• Proposition 3.13 (second best). With overlapping supports and regular distributions, the welfare-maximizing incentive-compatible, individually rational, ex ante budget balanced mechanisms are characterized by the trading rule

$$q(\theta) = 1 \iff \theta_B - \tfrac{\lambda}{1+\lambda}\tfrac{1 - F_B(\theta_B)}{f_B(\theta_B)} \ge \theta_S + \tfrac{\lambda}{1+\lambda}\tfrac{F_S(\theta_S)}{f_S(\theta_S)}$$

for some $\lambda > 0$, exact budget balance $\int q\,(\psi_B - \psi_S)\,f = \overline\theta_S - \int \psi_S f$, and the incentive-compatible payments with binding participation of $\overline\theta_S$ and $\underline\theta_B$.

• Proposition 3.14 (profit maximization). Profit $\mathbb E[t_B - t_S]$ is maximized by trading iff $\psi_B(\theta_B) > \psi_S(\theta_S)$, with the same payment formulas.
• Propositions 3.15–3.16 (uniform values on $[0,1]$). The second best trades iff $\theta_B - \theta_S > 1/4$; the profit maximizer trades iff $\theta_B - \theta_S > 1/2$.

Significance

The theorem locates the source of inefficiency in bilateral bargaining in private information itself, not in any particular bargaining protocol: no mechanism, however clever, achieves efficient voluntary trade without a subsidy. It is the reason efficiency in markets is studied as a limit (large double auctions approach efficiency as the number of traders grows), and why a trading platform's fee structure is analyzed as a second-best problem. The pivot-mechanism argument is the same one that proves the impossibility of first-best public-goods provision (Proposition 3.7), so the two formalizations share their structure.

All results of this section are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no mechanism-design library. The platform has the Chatterjee–Samuelson linear equilibrium as an open statement about one particular game; this mission states results about all mechanisms. A complete development yields a reusable one-dimensional envelope/payoff-equivalence library for two agents with differently oriented types (the seller's incentive constraint runs from high types down), and the Lagrangian optimality argument for a linear objective under a single linear constraint.

Difficulty

The obvious attempt to prove impossibility looks for a contradiction between incentive compatibility and budget balance state by state. That fails: incentive compatibility and participation are interim constraints, so any single state admits budget-balanced transfers consistent with them, and the contradiction exists only after integrating over the prior. Two points need care. The seller's orientation is reversed: her trade probability is decreasing and her participation constraint binds at the highest type. And the deficit of the pivot mechanism must be shown to have positive probability, which uses that the supports overlap in a set with nonempty interior. The optimal-mechanism results additionally need that the trading rule implied by a Lagrange multiplier satisfies the monotonicity constraint, which is where regularity enters, and that a multiplier exists which makes the budget constraint bind.

Formalization scope

A type vector is a pair θ : ℝ × ℝ with θ.1 the seller's and θ.2 the buyer's value. The prior is Lebesgue measure on $\Theta$ with density $f_S(\theta_S) f_B(\theta_B)$. Densities are measurable, strictly positive on the closed supports and integrate to one; nothing else, such as continuity, is assumed. The trading rule is real-valued with values in $\{0,1\}$ on $\Theta$ (deterministic, as in Definition 3.9). The measurability the book omits (Ch. 2 note 2) is built into the admissible class: $q$, $t_S$, $t_B$ are measurable with integrable transfers. "Increasing" is weak monotonicity, the book's convention.

Explicit formulas the statements carry: the first-best rule (3.61) with free tie rule, the pivot transfers of Definition 3.10, the rule (3.70) with parameter $\lambda > 0$, the exact budget equation of Proposition 3.13 (ii), the payment formulas $T_B(\theta_B) = \theta_B Q_B(\theta_B) - \int_{\underline\theta_B}^{\theta_B} Q_B$ and $T_S(\theta_S) = \overline\theta_S - (1 - Q_S(\theta_S))\theta_S - \int_{\theta_S}^{\overline\theta_S}(1 - Q_S)$, the profit rule $\psi_B > \psi_S$, and the thresholds $1/4$ and $1/2$.

The goal quantifies over every first-best trading rule and imposes budget balance as the ex post equality $t_S = t_B$. Dropping budget balance, weakening it to $t_S \le t_B$, or fixing one tie rule would give a different, and in the first case false, statement. The pointwise "if and only if … for all $\theta$" characterizations of Propositions 3.13–3.16 are stated with necessity almost everywhere, since an optimal trading rule is determined only up to null sets. For Proposition 3.14 necessity is also restricted to $\{\psi_B \ne \psi_S\}$: under weak regularity that tie set can have positive probability, and profit does not depend on the trading rule there.

Contributions welcome: proofs of the milestones, a two-agent payoff-equivalence lemma for the seller's reversed orientation, and a sorry-free construction of the pivot mechanism's integrability facts.

Selected references

• R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
• K. Chatterjee and W. Samuelson, Bargaining under incomplete information, Operations Research 31 (1983) 835–851. https://doi.org/10.1287/opre.31.5.835
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.4. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

Whether a community can finance a shared project out of voluntary contributions, when each member knows only her own benefit from it, is one of the founding questions of mechanism design. Bayesian mechanism design began with mechanisms for the provision of public goods: d'Aspremont and Gérard-Varet (1979) and Arrow (1979) showed that the efficient decision can be made Bayesian incentive compatible with a budget that balances in every state, provided agents cannot opt out. Once participation is voluntary, this is no longer possible, and Güth and Hellwig (1986) studied the best mechanism under that constraint. The same tension between efficiency, incentives, voluntary participation and budget balance drives the Myerson–Satterthwaite theorem for bilateral trade, which the next mission of this series formalizes.

This mission formalizes Section 3.3 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), which treats the public goods problem in the independent private values model with a continuum of types. The section proves an impossibility theorem for first best provision and then characterizes the best mechanisms that respect the budget: the welfare-maximizing (second best) mechanism and the profit-maximizing one, with a worked two-agent uniform example.

Setting

A community of agents $I = \{1, \dots, N\}$, $N \ge 2$, decides whether to produce an indivisible, nonexcludable public good, $g \in \{0,1\}$, at cost $c > 0$. Agent $i$ pays a transfer $t_i$ and obtains utility $\theta_i g - t_i$. Her type $\theta_i$ is private information, drawn independently across agents from a distribution $F_i$ with density $f_i$, strictly positive on the common support $[\underline\theta, \bar\theta]$, $0 \le \underline\theta < \bar\theta$. The type space is $\Theta = [\underline\theta, \bar\theta]^N$ and $f(\theta) = \prod_i f_i(\theta_i)$.

A direct mechanism is a decision rule $q : \Theta \to \{0,1\}$ and transfer rules $t_i : \Theta \to \mathbb R$. For agent $i$ reporting $\theta_i$, $Q_i(\theta_i)$ is the probability of production and $T_i(\theta_i)$ the expected transfer, taken over the other agents' types, and $U_i(\theta_i) = Q_i(\theta_i)\theta_i - T_i(\theta_i)$. The mechanism is incentive compatible (IC) if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i, \theta_i, \theta_i'$, and individually rational (IR) if $U_i(\theta_i) \ge 0$ for all $i, \theta_i$. It is ex post budget balanced if $\sum_i t_i(\theta) \ge c\,q(\theta)$ for every $\theta$, and ex ante budget balanced if this inequality holds after integrating both sides against $f$.

Welfare is $(\sum_i \theta_i)\, g - \sum_i t_i$. The first best decision rule is $q^*(\theta) = 1$ if $\sum_i \theta_i \ge c$ and $0$ otherwise; a first best mechanism uses $q^*$ and transfers that add up to exactly $c\,q^*(\theta)$ in every state. The pivot mechanism uses $q^*$ and

$$t_i(\theta) = \underline\theta\, q^*(\underline\theta,\theta_{-i}) + \big(q^*(\theta) - q^*(\underline\theta,\theta_{-i})\big)\Big(c - \sum_{j\ne i}\theta_j\Big).$$

The virtual valuation is $\psi_i(\theta_i) = \theta_i - (1-F_i(\theta_i))/f_i(\theta_i)$, and $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Proposition 3.7

$$\exists\ \text{an IC and IR first best mechanism} \iff N\underline\theta \ge c \ \text{ or }\ N\bar\theta \le c .$$

In the two cases on the right, producing is efficient for every type vector or for none; in every other case efficient provision cannot be financed voluntarily.

Milestones

1. Proposition 3.6: every ex ante budget balanced mechanism has an equivalent ex post budget balanced one.
2. Lemma 3.6: the pivot mechanism is IC and IR.
3. Lemma 3.7: among IC and IR mechanisms with decision rule $q^*$, the pivot mechanism has the largest expected budget surplus.
4. Lemma 3.8: if $N\underline\theta < c < N\bar\theta$, the pivot mechanism's expected budget surplus is negative.
5. Proposition 3.8 (second best): under regularity and $N\underline\theta < c < N\bar\theta$, an IC, IR, ex ante budget balanced mechanism maximizes expected welfare among such mechanisms iff for some $\lambda > 0$

$$q(\theta) = 1 \iff \sum_i \theta_i > c + \sum_i \frac{\lambda}{1+\lambda}\,\frac{1-F_i(\theta_i)}{f_i(\theta_i)},$$

the budget binds, $\int_\Theta q(\theta)\big[\sum_i \psi_i(\theta_i) - c\big] f(\theta)\,d\theta = 0$, and $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$. 6. Proposition 3.9 (profit maximization): under regularity, the profit-maximizing IC and IR mechanism produces iff $\sum_i \theta_i > c + \sum_i (1-F_i(\theta_i))/f_i(\theta_i)$, with the same formula for $T_i$. 7. Proposition 3.10 (Example 3.3: $N=2$, uniform types on $[0,1]$, $0<c<2$): the second best produces iff $\theta_1+\theta_2 > s$, where $s$ is the unique root in $[0,1]$ of $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ if $c < 2/3$, and $s = \tfrac12 + \tfrac34 c$ if $c \ge 2/3$. 8. Proposition 3.11 (same example): the profit maximizer produces iff $\theta_1+\theta_2 > 1 + \tfrac12 c$.

Significance

Proposition 3.7 says that with voluntary participation no mechanism both takes efficient production decisions and pays for them, outside the degenerate cases. It is the reason the rest of the section, and much of the applied literature on public goods, studies constrained optimum mechanisms: Proposition 3.8 describes what the best budget-respecting mechanism gives up (it undersupplies the good, producing only when valuations exceed a bound strictly above the cost), and Proposition 3.9 quantifies the further distortion under a monopoly supplier. The example makes the three thresholds explicit and comparable.

All results of the section are classical and proved in the book, several of them only sketched there (Proposition 3.9 is stated without proof; Proposition 3.8 invokes an infinite-dimensional Kuhn–Tucker theorem whose applicability is not checked). None of them is formalized in Lean. The mission produces a machine-checked account of the envelope and revenue-equivalence arguments with interim expectations over independent types, a checked pivot-mechanism deficit computation, and a checked Lagrangian characterization; the uniform example additionally certifies the book's arithmetic.

Difficulty

The naive argument for the goal fails at the first step: a mechanism that implements $q^*$ with a balanced budget in every state is not obviously comparable to one that is only IC and IR, because IC constrains interim expectations while budget balance is ex post. The impossibility needs a reduction of the whole class of IC, IR mechanisms with rule $q^*$ to a single extremal one, which requires the payoff equivalence formula for interim utilities and an exact integral identity for expected revenue in terms of virtual valuations. The strict deficit of the pivot mechanism then needs a case analysis over which agents are pivotal and a positive-probability argument. For Proposition 3.8, pointwise maximization of a Lagrangian is not enough: one must show the multiplier exists and is positive, that the maximizer satisfies the monotonicity constraint, and that uniqueness holds only up to null sets.

Formalization scope

Agents are Fin N with $N \ge 2$; types are vectors in Fin N → ℝ; the type distribution is the product of the marginal measures $f_i(x)\,dx$ on $[\underline\theta,\bar\theta]$, which encodes independence. $Q_i$ and $T_i$ integrate the decision and transfer rules against this distribution with agent $i$'s coordinate overwritten by her report. Decision rules are deterministic, with values in $\{0,1\}$ on $\Theta$, as in Definition 3.4. Ties in the first best rule produce, as in the book's note 2 to Chapter 3; the second best and profit-maximizing rules use strict inequalities, as printed.

The book omits measurability and the existence of conditional expectations; the class of direct mechanisms here requires $q$ and each $t_i$ to be Borel measurable, each $t_i$ integrable, and each conditional expectation of $t_i$ given one agent's type to exist. The characterizations in Propositions 3.8–3.11 are stated in two directions: the stated rule, for every $\theta$, is sufficient; necessity holds for almost every $\theta$, since changing $q$ on a null set of type vectors changes nothing that is optimized. The explicit formulas the mission commits to are: the pivot transfers above; the second best rule with multiplier $\lambda > 0$ and the binding budget identity; $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i$; the cubic $-\tfrac23 s^3 + s^2 - (1-\tfrac12 s^2)c = 0$ for $c < 2/3$; $s = \tfrac12 + \tfrac34 c$ for $c \ge 2/3$; and $s = 1 + \tfrac12 c$ for the profit maximizer.

A trivializing formalization of the goal takes "first best" to mean only the decision rule $q^*$; the pivot mechanism would then be a witness in every case, so first best here also requires transfers adding up to exactly $c\,q^*(\theta)$ in every state.

Reusable infrastructure includes interim expectations over independent product distributions, the payoff and revenue equivalence lemmas for IC mechanisms, and the virtual-valuation identity for expected revenue; these are shared with the auction and bilateral trade chapters of the series. Contributions to any milestone, and to general lemmas about product measures with densities on boxes, are welcome.

Selected references

• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.3. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• C. d'Aspremont and L.-A. Gérard-Varet, Incentives and incomplete information, Journal of Public Economics 11 (1979) 25–45. https://doi.org/10.1016/0047-2727(79)90043-4
• W. Güth and M. Hellwig, The private supply of a public good, Zeitschrift für Nationalökonomie, Supplement 5 (1986) 121–159.
• R. B. Myerson and M. A. Satterthwaite, Efficient mechanisms for bilateral trading, Journal of Economic Theory 29 (1983) 265–281. https://doi.org/10.1016/0022-0531(83)90048-0
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969.

Why revenue-maximizing auctions matter

A seller with one indivisible good and several potential buyers, each of whom privately knows how much the good is worth to them, has to choose a selling procedure: a posted price, an English auction, a sealed-bid auction with a reserve price, or something more elaborate. Which procedure raises the most expected revenue? Myerson's answer (Myerson 1981) is the foundation of optimal auction design. It underlies reserve-price setting in practice, the analysis of sponsored-search and ad-exchange auctions, and the modern algorithmic mechanism design literature, which treats Myerson's auction as the benchmark against which simple and approximately optimal auctions are measured.

This mission formalizes Section 3.2 of Tilman Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), the textbook treatment of Myerson's result in the independent private values model with Bayesian incentive compatibility. It is the second mission of a series covering the book.

Timeline. Vickrey (1961) showed that the second-price auction makes truthful bidding a dominant strategy and compared auction formats. Myerson (1981) characterized the revenue-maximizing mechanism for independent private values with possibly asymmetric distributions; Riley and Samuelson (1981) obtained the symmetric case and the optimal reserve price independently. The revelation principle in the Bayesian form used here goes back to Myerson (1979) and Dasgupta, Hammond and Maskin (1979).

Setting

There are $N \ge 2$ potential buyers $i \in I = \{1,\dots,N\}$. Buyer $i$ values the good at $\theta_i$; if he receives it and pays $t_i$ his utility is $\theta_i - t_i$, and otherwise $-t_i$. The seller's utility is $\sum_i t_i$. The valuations $\theta_1,\dots,\theta_N$ are independent; $\theta_i$ has cumulative distribution function $F_i$ and density $f_i$ with $f_i(\theta_i) > 0$ on the common support $[\underline\theta, \bar\theta]$, where $0 \le \underline\theta < \bar\theta$. The type space is $\Theta = [\underline\theta,\bar\theta]^N$ and the joint density is $f(\theta) = \prod_i f_i(\theta_i)$.

A direct mechanism asks buyers to report their types and consists of an allocation rule $q : \Theta \to \Delta$, where $\Delta = \{(q_1,\dots,q_N) : 0 \le q_i \le 1,\ \sum_i q_i \le 1\}$, and payment rules $t_i : \Theta \to \mathbb R$. Its interim quantities are the expected allocation probability, payment and utility of buyer $i$ conditional on his own type:

$$Q_i(\theta_i) = \int_{\Theta_{-i}} q_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad T_i(\theta_i) = \int_{\Theta_{-i}} t_i(\theta_i,\theta_{-i}) f_{-i}(\theta_{-i})\,d\theta_{-i},\quad U_i = \theta_i Q_i - T_i.$$

The mechanism is incentive-compatible if $\theta_i Q_i(\theta_i) - T_i(\theta_i) \ge \theta_i Q_i(\theta_i') - T_i(\theta_i')$ for all $i,\theta_i,\theta_i'$ (truth-telling is a Bayesian Nash equilibrium) and individually rational if $U_i(\theta_i) \ge 0$ for all $i,\theta_i$. The virtual valuation of buyer $i$ is

$$\psi_i(\theta_i) = \theta_i - \frac{1 - F_i(\theta_i)}{f_i(\theta_i)},$$

and the distribution $F_i$ is regular if $\psi_i$ is strictly increasing.

Formalization targets

Goal: Myerson's optimal auction (Proposition 3.4)

Under regularity, among all incentive-compatible and individually rational direct mechanisms, a mechanism maximizes the seller's expected revenue $\mathbb E[\sum_i t_i(\theta)]$ exactly when, for every buyer $i$,

$$q_i(\theta) = \begin{cases}1 & \text{if } \psi_i(\theta_i) > 0 \text{ and } \psi_i(\theta_i) > \psi_j(\theta_j) \text{ for all } j \ne i,\\ 0&\text{otherwise,}\end{cases}\qquad T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx,$$

the allocation identity holding for almost every $\theta$; and such a mechanism exists.

Milestones

1. Proposition 3.1, the revelation principle: every Bayesian Nash equilibrium of every mechanism is replicated by truth-telling in an incentive-compatible direct mechanism.
2. Lemmas 3.1–3.4: incentive compatibility makes $Q_i$ increasing and $U_i$ convex with $U_i' = Q_i$; payoff equivalence $U_i(\theta_i) = U_i(\underline\theta) + \int_{\underline\theta}^{\theta_i} Q_i$; revenue equivalence for $T_i$.
3. Proposition 3.2: incentive compatibility holds if and only if every $Q_i$ is increasing and the revenue-equivalence formula holds.
4. Proposition 3.3: under incentive compatibility, individual rationality is equivalent to $T_i(\underline\theta) \le \underline\theta Q_i(\underline\theta)$.
5. Lemma 3.5: an optimal mechanism has $T_i(\underline\theta) = \underline\theta Q_i(\underline\theta)$.
6. Eqs. (3.4)–(3.5): expected revenue equals expected virtual surplus $\sum_i \int_\Theta q_i(\theta)\psi_i(\theta_i) f(\theta)\,d\theta$.
7. Proposition 3.5: a mechanism maximizes expected welfare $\mathbb E[\sum_i q_i(\theta)\theta_i]$ among incentive-compatible, individually rational mechanisms if and only if it gives the good to the highest value (almost everywhere) and $T_i(\theta_i) \le \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i}Q_i$.

Significance

The theorem identifies the revenue-maximizing selling procedure among all procedures, not among a parametric family: by the revelation principle, no auction format, however elaborate, and no equilibrium of it can beat the mechanism of Proposition 3.4. Its consequences include the optimality of first- and second-price auctions with reserve price $\psi^{-1}(0)$ when buyers are symmetric, the revenue equivalence of standard auction formats, the fact that an asymmetric optimal auction may sell to a buyer without the highest value, and the monopoly inefficiency that the optimal seller sometimes withholds the good. The envelope characterization of Bayesian incentive compatibility (Proposition 3.2) is the tool reused throughout the rest of the book, in public goods provision, bilateral trade and dynamic screening.

The result is classical and fully proved in the literature. What is missing is a machine-checked version at this generality: asymmetric distributions, an arbitrary lower support end $\underline\theta \ge 0$, Bayesian (interim) rather than dominant-strategy constraints, and optimality over all incentive-compatible and individually rational mechanisms. Existing formalizations on the platform treat the i.i.d. case with values on $[0,\bar v]$.

Difficulty

The obvious argument maximizes the virtual surplus $\sum_i q_i(\theta)\psi_i(\theta_i)$ pointwise and declares victory, but this ignores that the seller's feasible set is constrained by monotonicity of every $Q_i$; the pointwise maximizer is feasible only because regularity makes $\psi_i$ increasing, and that has to be proved for the interim probabilities, which integrate over the other buyers' types. The revenue identity links interim payments, which integrate over the other buyers' types, to an integral over the whole type space weighted by the virtual valuation, and it is only valid for mechanisms whose lowest types' payments are pinned down. The necessity direction requires showing that ties and zero virtual values are null events, which rests on strict monotonicity of every $\psi_i$ and on the absolute continuity of the type distribution. Finally, the envelope step requires convexity and almost-everywhere differentiability of $U_i$, with care at the endpoints of the type interval.

Formalization scope

Buyers form a finite type with at least two elements. The prior is the measure on $\mathbb R^N$ with density $\prod_i f_i(\theta_i)$ on $\Theta$ and no mass outside it; each $f_i$ is measurable, strictly positive on $[\underline\theta,\bar\theta]$ and integrates to $1$; $F_i(\theta_i) = \int_{\underline\theta}^{\theta_i} f_i$. Allocation and payment rules are total functions whose values on $\Theta$ are constrained, and $Q_i$, $T_i$ are prior expectations with the $i$-th coordinate fixed. "Increasing" is weak monotonicity, as in the book; regularity is strict monotonicity of $\psi_i$ on $[\underline\theta,\bar\theta]$ (Assumption 3.1).

The following conventions are committed to:

• Measurability. The book omits measurability throughout. The comparison class for optimality consists of mechanisms with measurable $q_i, t_i$, integrable $t_i$, and integrable sections $\theta_{-i}\mapsto t_i(\theta_i,\theta_{-i})$. Without these hypotheses the Lean integrals would be $0$ and revenue comparisons would be meaningless.
• Almost-everywhere characterizations. Propositions 3.4 and 3.5 are printed with "for all $\theta \in \Theta$". Changing $q$ on a null set of type vectors changes neither incentives nor revenue nor welfare, so the "only if" directions hold only almost everywhere; they are stated for almost every $\theta$, and the existence of a mechanism satisfying the allocation rule at every $\theta$ is stated separately. The payment conditions hold for every $\theta_i$.
• Explicit formulas. The goal states Myerson's allocation rule and the payment formula $T_i(\theta_i) = \theta_i Q_i(\theta_i) - \int_{\underline\theta}^{\theta_i} Q_i(x)\,dx$ explicitly. Proposition 3.5 states the efficient rule $q_i(\theta) = 1$ iff $\theta_i > \theta_j$ for all $j \ne i$, and the payment inequality. A statement asserting only that some optimal mechanism exists, or only that the optimal auction is efficient, would not be this theorem.
• Revelation principle. A general mechanism has arbitrary measurable message sets and an outcome function giving allocation probabilities in $\Delta$ and expected transfers; equilibria are in pure type-contingent strategies. A version in which the mechanism is already direct would be trivial and is not the statement.
• Interim constraints. Incentive compatibility and individual rationality are Bayesian and interim, not dominant-strategy or ex post; the latter are the subject of a later mission.
• Endpoints in Lemma 3.2. Differentiability of $U_i$ and $U_i' = Q_i$ are stated at interior points of $[\underline\theta,\bar\theta]$.

The envelope and payoff-equivalence lemmas, and the revenue identity, are reused in later missions of this series, so proofs of the milestones are welcome independently of the goal.

Selected references

• Tilman Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, §3.2, pp. 31–45. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• John G. Riley and William F. Samuelson, Optimal Auctions, American Economic Review 71(3), 381–392, 1981. https://www.jstor.org/stable/1802786
• William Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. https://doi.org/10.2307/1912346
• Partha Dasgupta, Peter Hammond and Eric Maskin, The Implementation of Social Choice Rules: Some General Results on Incentive Compatibility, Review of Economic Studies 46(2), 185–216, 1979. https://doi.org/10.2307/2297045

Motivation

A seller with one good and one buyer whose valuation she does not know faces the simplest problem of mechanism design: choose a selling procedure, anticipating that the buyer will act in his own interest given what he knows. The textbook answer, "post the monopoly price", is usually derived by optimizing over prices alone. The question that opens Börgers' An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015, doi:10.1093/acprof:oso/9780199734023.001.0001) is whether the seller could do better with anything else: negotiation, lotteries, menus of price–probability pairs, or any extensive game she can commit to.

Chapter 2 answers this for one buyer, and in doing so introduces the tools the rest of the book, and most of auction theory, reuse: the revelation principle, the envelope characterization of incentive compatibility, payoff and revenue equivalence, and the virtual valuation. The book's exposition of §2.2 follows Manelli and Vincent (2007), and the nonlinear pricing model of §2.3 is due to Mussa and Rosen (1978, doi:10.1016/0022-0531(78)90085-6); both attributions are the book's own (§2.5, p.29).

Setting

The buyer's type $\theta$ is his valuation for the good. His utility is $\theta-t$ if he receives the good and pays $t$, and $-t$ if he only pays $t$. The seller's belief about $\theta$ is a cumulative distribution function $F$ with density $f$ on an interval $[\underline\theta,\bar\theta]$, $0\le\underline\theta<\bar\theta$, with $f(\theta)>0$ throughout and $F(\theta)=\int_{\underline\theta}^{\theta}f(x)\,dx$.

A direct mechanism is a pair $q:[\underline\theta,\bar\theta]\to[0,1]$, $t:[\underline\theta,\bar\theta]\to\mathbb R$: the buyer reports a type $\theta'$, receives the good with probability $q(\theta')$ and pays $t(\theta')$. Write $u(\theta)=\theta q(\theta)-t(\theta)$. The mechanism is incentive-compatible if $u(\theta)\ge\theta q(\theta')-t(\theta')$ for all $\theta,\theta'$, and individually rational if $u(\theta)\ge 0$ for all $\theta$. The seller's expected revenue is $\int_{\underline\theta}^{\bar\theta}t(\theta)f(\theta)\,d\theta$.

For the extreme-point argument, $\mathcal F$ denotes the space of functions on $[\underline\theta,\bar\theta]$ with the $L^1$ norm, and $M\subset\mathcal F$ the set of increasing functions with values in $[0,1]$. A point $x$ of a convex set $C$ is an extreme point if for every $y\neq 0$ at least one of $x+y$, $x-y$ lies outside $C$.

In the nonlinear pricing model of §2.3 the good is divisible, quantity $q\ge 0$ costs the seller $cq$ with $c>0$, and the buyer's utility is $\theta\nu(q)-t$, with $\nu(0)=0$, $\nu'>0$, $\nu''<0$, $\bar\theta\nu'(0)>c$ and $\lim_{q\to\infty}\bar\theta\nu'(q)<c$. The seller maximizes expected profit $\int(t-cq)f$. The distribution $F$ is regular if the virtual valuation $\theta-(1-F(\theta))/f(\theta)$ is increasing.

Formalization targets

Goal: Proposition 2.5, a posted price is optimal

If $p^*\in\arg\max_{p\in[\underline\theta,\bar\theta]}p(1-F(p))$, then the mechanism

$$q(\theta)=\begin{cases}1&\theta>p^*\\0&\theta<p^*\end{cases},\qquad t(\theta)=\begin{cases}p^*&\theta>p^*\\0&\theta<p^*\end{cases}$$

maximizes expected revenue among all incentive-compatible, individually rational direct mechanisms. The comparison class contains every randomized rule $q$ with values in $[0,1]$; the statement fixes no distribution and no constant.

Milestones on the way

1. Proposition 2.1: every mechanism and optimal buyer strategy can be replaced by a truthful direct mechanism with the same outcomes.
2. Lemmas 2.1–2.4: incentive compatibility forces $q$ increasing, $u$ increasing and convex with $u'=q$, and

$$u(\theta)=u(\underline\theta)+\int_{\underline\theta}^{\theta}q(x)\,dx,\qquad t(\theta)=t(\underline\theta)+\big(\theta q(\theta)-\underline\theta q(\underline\theta)\big)-\int_{\underline\theta}^{\theta}q(x)\,dx.$$

3. Propositions 2.2–2.3 and Lemma 2.5: these conditions characterize incentive compatibility; individual rationality reduces to $u(\underline\theta)\ge0$; at the optimum $t(\underline\theta)=\underline\theta q(\underline\theta)$.
4. Lemma 2.6, Proposition 2.4, Lemma 2.7: $M$ is compact and convex, a linear function continuous on a compact convex set attains its maximum at an extreme point, and the extreme points of $M$ are the $\{0,1\}$-valued functions.
5. Proposition 2.6: under regularity, $q(\theta)=0$ when $\nu'(0)\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)\le c$, otherwise $\nu'(q(\theta))\big(\theta-\tfrac{1-F(\theta)}{f(\theta)}\big)=c$, with $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$, maximizes expected profit.

Significance

Proposition 2.5 says that the elementary monopoly price is not a restriction of the seller's options but the solution of the unrestricted design problem, including every lottery and every indirect procedure. Its one-buyer argument is the template for Myerson's optimal auction (Chapter 3 of the book), whose revenue formula is the multi-buyer form of Lemma 2.4. Proposition 2.6 exhibits the two standard features of screening, no distortion at the top and downward distortion below, which recur in regulation, insurance and contract theory.

All results of the chapter are classical and proved in the book. None of them is formalized on Prove2Me, and Mathlib has neither the revelation principle, the envelope lemma for incentive-compatible mechanisms, nor a maximum principle for linear functions on compact convex sets (Mathlib has the Krein–Milman lemma, IsCompact.extremePoints_nonempty, but not Bauer's maximum principle). The mission therefore produces the first machine-checked foundation for the one-agent screening model on which chapters 3, 4 and 11 of the book build.

Difficulty

The obvious argument for the goal compares the posted price with other posted prices; that comparison is one line and is not the theorem. The content is the comparison with randomized mechanisms: an arbitrary increasing $q$ with values in $[0,1]$ may do better than every deterministic threshold rule unless one shows that expected revenue is linear in $q$ and that its maximum over the infinite-dimensional set $M$ is attained at an extreme point. That step needs compactness of $M$ in $L^1$ and a maximum principle on compact convex sets in a normed space, neither of which is finite-dimensional linear programming. The envelope step (Lemma 2.3) needs absolute continuity of a convex function on a closed interval, including its endpoints, where $u$ need not be differentiable. For Proposition 2.6 the pointwise maximizer of the virtual surplus must be shown to be monotone and to satisfy incentive compatibility, which is where regularity enters.

Formalization scope

Types are real numbers; every function of the type is a total function $\mathbb R\to\mathbb R$ and every condition quantifies over $[\underline\theta,\bar\theta]$ only. "Increasing" means weakly increasing (the book's note 3). The distribution is a structure carrying the density $f$, positive and integrable on $[\underline\theta,\bar\theta]$ with total mass $1$, and $F$ tied to it by $F(\theta)=\int_{\underline\theta}^{\theta}f$. No measurability or integrability hypothesis is placed on mechanisms: incentive compatibility makes $q$ monotone and $t$ bounded and measurable, so every expected revenue is a genuine integral.

The explicit formulas are part of the statements: the posted-price mechanism of Proposition 2.5 with $p^*\in\arg\max p(1-F(p))$; the payment formulas of Lemmas 2.3–2.4 and Proposition 2.2; $t(\underline\theta)=\underline\theta q(\underline\theta)$ in Lemma 2.5; and in Proposition 2.6 the two-case rule for $q$ and the payment $t(\theta)=\theta\nu(q(\theta))-\int_{\underline\theta}^{\theta}\nu(q(x))\,dx$. The goal fixes $q(p^*)=1$, $t(p^*)=p^*$ for existence and quantifies over every incentive-compatible, individually rational completion at the tie.

The space $\mathcal F$ is $L^1([\underline\theta,\bar\theta])$ of almost-everywhere classes, because the book's $L^1$ "norm" on bounded functions vanishes on null functions; $M$ is the set of classes with an increasing $[0,1]$-valued representative, and Lemma 2.7 is an almost-everywhere statement, as the book's notes 4–6 already indicate. Proposition 2.4 is stated for a nonempty compact convex set in a real normed space and a linear map continuous on that set. The revelation principle models a general mechanism as the buyer's reduced strategy set, an arbitrary type, with a purchase probability and an expected payment for each strategy.

A goal that compared the posted price only with other posted prices, or only with deterministic mechanisms, would be trivial and is excluded: the competitors range over all incentive-compatible, individually rational direct mechanisms with $q$ valued in $[0,1]$.

Reusable beyond this mission: the one-agent envelope and revenue-equivalence lemmas (needed again in Chapters 3, 4 and 11), compactness of monotone functions in $L^1$, and the maximum principle for linear functions on compact convex sets. Contributions to any of these are welcome.

Selected references

• T. Börgers (with D. Krähmer and R. Strausz), An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015. doi:10.1093/acprof:oso/9780199734023.001.0001
• M. Mussa and S. Rosen, "Monopoly and product quality", Journal of Economic Theory 18(2), 1978. doi:10.1016/0022-0531(78)90085-6
• E. A. Ok, Real Analysis with Economic Applications, Princeton University Press, 2007 (Extreme Point Theorem, p.658), cited by the book at p.16.

Motivation

Assumptions of Physics by Gabriele Carcassi and Christine A. Aidala (book, v3.0, 2025) is a programme to derive the mathematical structures of physical theories from explicit physical requirements. Part II, "Physical Mathematics", begins (Chapter 1) by making precise what it means for a statement to be experimentally verifiable, and shows that a single physical requirement (only countably many tests can be run in an indefinite amount of time) is enough to force the familiar structures of point-set topology onto the space of outcomes of any experiment. This mission formalizes that chapter. It is the first mission of a series on the book; all declarations live in the namespace AssumptionsOfPhysics so that later missions can build on them.

Setting

A logical context is represented by its set $\Omega$ of possible truth assignments, and a statement (up to logical equivalence) by its truth set $s\subseteq\Omega$. Negation, conjunction and disjunction are complement, intersection and union; the certainty is $\Omega$ and the impossibility is $\emptyset$; "$s_1$ is narrower than $s_2$" means $s_1\subseteq s_2$, and $s_1,s_2$ are compatible when $s_1\cap s_2\neq\emptyset$.

An experimental domain $\mathcal D$ is a family of statements that contains $\Omega$ and $\emptyset$, is closed under finite conjunction and countable disjunction, and has a countable basis $B\subseteq\mathcal D$: every element of $\mathcal D$ is obtained from $B$ by finite conjunctions and countable disjunctions. Its theoretical domain $\bar{\mathcal D}$ is the closure of $\mathcal D$ under negation, finite conjunction and countable disjunction. A possibility is a non-impossible $x\in\bar{\mathcal D}$ that, for every $s\in\bar{\mathcal D}$, is either narrower than $s$ or incompatible with it; $X$ denotes the set of possibilities. The verifiable set of a statement $s$ is $U(s)=\{x\in X: x\cap s\neq\emptyset\}$, and the natural topology on $X$ is the topology generated by $\{U(s): s\in\mathcal D\}$. A domain is decidable if it is closed under negation.

Formalization targets

Goal (Propositions 1.57, 1.61, 1.65)

$$\mathcal T_X = \{U(s) : s\in\mathcal D\},\qquad (X,\mathcal T_X)\ \text{is second-countable and } T_0 .$$

Milestones

• Proposition 1.37: $\bar{\mathcal D}$ is closed under countable conjunction.
• Proposition 1.46: any basis of $\mathcal D$ generates $\bar{\mathcal D}$ by negation and countable operations.
• Proposition 1.48: the possibilities are exactly the non-impossible minterms of a basis.
• Theorem 1.52: $|X|\le 2^{\aleph_0}$.
• Proposition 1.53: $X$ finite $\iff$ $\mathcal D$ finite $\iff$ $\mathcal D$ has a finite basis.
• Proposition 1.56: $s=\bigvee_{x\in U(s)}x$ for $s\in\mathcal D$.
• Propositions 1.57, 1.60, 1.61, 1.65: the verifiable sets are exactly the open sets; $U(B)\cup\{X\}$ is a sub-basis; second countability; $T_0$.
• Proposition 1.66: $T_1$ $\iff$ every possibility is approximately verifiable.
• Proposition 1.74 and Theorem 1.76: equivalent characterizations of decidable domains, and decidability $\iff$ discreteness of the natural topology.

Significance

The chapter's results identify the open sets of a topology with verifiable statements and its points with complete experimental answers (possibilities). Second countability and the $T_0$ axiom are thereby derived rather than assumed, and the cardinality bound $|X|\le 2^{\aleph_0}$ limits which mathematical objects can carry experimental meaning. Later chapters of the book (domain combination, properties and quantities, ensemble spaces) rely on these facts. The results are proved informally in the book; no machine-checked formalization of them is known to the drafters. A formalization fixes the precise hypotheses under which they hold (for instance, whether a basis must be countable in Propositions 1.46, 1.48 and 1.60) and provides a reusable library for the rest of the series.

Difficulty

The individual statements are elementary, but several of the book's proofs are informal about two points that a formal proof must handle. First, the possibilities must be shown to cover the space of assignments and to be atoms of $\bar{\mathcal D}$; the book argues through minterms of a countable basis, which needs a "disjunctive normal form" for countably generated families. Second, the natural topology is defined via arbitrary unions while experimental domains are only closed under countable disjunction; showing that every open set is still of the form $U(s)$ (Proposition 1.57) requires a second-countability / Lindelöf-type argument rather than direct closure.

Formalization scope

Statements are subsets s : Set Ω of an arbitrary type Ω (possibly empty); the experimental domain is the structure ExperimentalDomain Ω, whose field stmts is the family $\mathcal D$. Generation by finite conjunction and countable disjunction (FinConjCountDisj) includes the empty conjunction $\Omega$ and the empty disjunction $\emptyset$; generation with negation (NegFinConjCountDisj) includes $\Omega$. Possibilities form the type D.Possibility, which carries the natural topology as an instance; topological notions (SecondCountableTopology, T0Space, T1Space, DiscreteTopology) are Mathlib's. The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in $\mathcal D$ is what all results of the chapter use. Statements involving "a basis" quantify over every basis (countable or not), as in the source. Contributions of reusable lemmas, in particular a disjunctive-normal-form lemma for countably generated families of sets, are welcome.

Selected references

• G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 1 "Verifiable statements and experimental domains", pp. 101–146.

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.

It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.

Setting

Mine A holds $x_0 \ge 0$ units of gold and mine B holds $y_0 \ge 0$. At time $t$ a proportion $\varphi_1(t) \in [0,1]$ of the machine's effort goes to A and $\varphi_2(t) = 1 - \varphi_1(t)$ to B (Eq. (7.3)). With $x(t), y(t)$ the gold remaining, $p(t)$ the probability that the machine still works and $f(t)$ the expected gold mined, the process is defined by Eq. (7.2):

$$\frac{dx}{dt} = -\varphi_1 r_1 x,\qquad \frac{dy}{dt} = -\varphi_2 r_2 y,\qquad \frac{dp}{dt} = -p\,(\varphi_1 q_1 + \varphi_2 q_2),\qquad \frac{df}{dt} = p\,(\varphi_1 r_1 x + \varphi_2 r_2 y),$$

with $x(0) = x_0$, $y(0) = y_0$, $p(0) = 1$, $f(0) = 0$. The mining rates $r_1, r_2$ and the failure rates $q_1, q_2$ are positive. The objective is the expected total gold $f(\infty) = \int_0^\infty f'(t)\,dt$.

In the three-choice problem (§ 12) a third decision $C$ removes gold from A at rate $r_3$ and from B at rate $r_4$, and fails at rate $q_3$. A control is a triple $\varphi_1, \varphi_2, \varphi_3 \ge 0$ with $\varphi_1 + \varphi_2 + \varphi_3 = 1$ (Eq. (12.2)). For a horizon $T$, the switching functions $K_1, K_2, K_3$ of Eq. (12.5) are computed along a control. For instance,

$$K_1(t) = -q_1\int_t^T f'(s)\,ds + r_1\,p(T)\,x(T) - r_1\int_t^T p'(s)\,x(s)\,ds.$$

They measure the first-order gain from shifting effort towards each decision at time $t$. The linear forms

$$C_1 = q_1 r_2 y - q_2 r_1 x,\qquad C_2 = q_1 r_4 y - (q_3 r_1 - q_1 r_3)x,\qquad C_3 = (q_3 r_2 - q_2 r_4) y - q_2 r_3 x$$

and the quantity $D = q_1 r_2 r_3 + q_2 r_1 r_4 - q_3 r_1 r_2$ (Eqs. (13.2)–(13.3)) organize the analysis.

Formalization targets

Goal: Chapter VIII, Theorem 1

For the two-choice process, the maximum of $f(\infty)$ is attained by the policy

$$\varphi_1 = 1 \text{ for } q_1 r_2 y < q_2 r_1 x,\qquad \varphi_2 = 1 \text{ for } q_1 r_2 y > q_2 r_1 x,\qquad \varphi_1 = \tfrac{r_2}{r_1+r_2},\ \varphi_2 = \tfrac{r_1}{r_1+r_2} \text{ for } q_1 r_2 y = q_2 r_1 x.$$

The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes $f(\infty)$ over all measurable controls with values in $[0,1]$.

Milestones

1. Eq. (10.1): $f_A(\infty) = r_1 x_0/(q_1 + r_1)$ and $f_B(\infty) = r_2 y_0/(q_2 + r_2)$ for the pure policies.
2. Lemmas 1–3 (§ 13): for a control that maximizes $f(T)$, almost everywhere, $K_i > K_j$ forces $\varphi_i = 1$ or $\varphi_j = 0$; a strictly largest $K_i$ forces $\varphi_i = 1$; a strictly beaten $K_i$ forces $\varphi_i = 0$.
3. Lemma 4 (§ 14): if $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant and $D \ne 0$, no optimal control mixes $A$, $B$ and $C$ on an interval.
4. Lemma 5 (§ 14): a mixture of exactly two decisions on an interval keeps the state on $C_1 = 0$, $C_2 = 0$ or $C_3 = 0$ respectively, with the proportions that hold $y/x$ fixed.
5. § 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$.
6. "Theorem 8" (§ 16, the chapter's third theorem): if $D < 0$ (with $r_3 > r_4$ and $x_0, y_0 > 0$), the three-choice problem is solved by the two-choice rule of Theorem 1, and every optimal control has $\varphi_3 = 0$ almost everywhere.

Significance

Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope $y/x$, and on the line $q_1 r_2 y = q_2 r_1 x$ it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: $D < 0$ means that $C$ removes gold at a higher failure cost than an equivalent mixture of $A$ and $B$.

On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.

Difficulty

The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and $B$ is preferred near the $y$-axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let $\varphi$ be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into "$C_k = 0$ on the interval".

Formalization scope

• Process by closed forms. No differential equations are formalized. With $\Phi_i(t) = \int_0^t \varphi_i$, the definitions are $x = x_0 e^{-r_1\Phi_1 - r_3\Phi_3}$, $y = y_0 e^{-r_2\Phi_2 - r_4\Phi_3}$, $p = e^{-\sum_i q_i\Phi_i}$, $f(T) = \int_0^T f'$. These are the unique absolutely continuous solutions of (7.2) and (12.1). The two-choice process is the three-choice one with $\varphi_3 = 0$.
• Controls are open-loop and measurable, with $\varphi_i \ge 0$ and $\sum_i \varphi_i = 1$. Decisions are indexed 0, 1, 2 for $A, B, C$.
• $f(\infty)$ is a lower Lebesgue integral with values in $[0,\infty]$. It has no junk value, and optimality is compared in $[0,\infty]$.
• Theorem 1's feedback rule is encoded as a predicate on open-loop controls: the rule holds along the control's own trajectory for almost every $t \ge 0$. The goal also asserts that such a control exists, which rules out the trivializing reading in which no control satisfies the rule and the optimality claim is vacuous.
• Horizon of Lemmas 1–5. § 12 considers only $T = \infty$, but the variation (12.4) and the switching functions (12.5) are written for a general $T$. Each lemma is formalized for both: every finite horizon $T$, with $K_i$ built from that horizon, and $T = \infty$, with $K_i$ given by (12.5) at $T = \infty$ (boundary term $0$).
• Implicit ranges. All rates $q_1, q_2, q_3, r_1, \dots, r_4$ are taken positive, and $x_0, y_0 \ge 0$. Lemmas 4–5 and "Theorem 8" take $x_0, y_0 > 0$, the open quadrant the book analyses. Lemma 4 carries the book's assumption that $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant ($q_1 r_3 < q_3 r_1$, $q_2 r_4 < q_3 r_2$). "Theorem 8" carries the standing assumption $r_3 > r_4$ of § 15.
• Misprint corrected. The value of the pure $C$-policy in the proof of Lemma 6 (§ 15, Eq. (1), p. 237) is printed $r_3 x_0/(q_2 + r_3) + r_4 y_0/(q_3 + r_4)$. The first denominator must be $q_3 + r_3$: for $x_0 = 1$, $y_0 = 0$, $q_2 = 1$, $q_3 = 2$, $r_3 = 1$ the process yields $1/3$, not $1/2$. The corrected identity is stated.
• Numbering. The third theorem of the chapter is printed "Theorem 8" and is cited that way.
• Left out. Theorem 2 ($D > 0$) specifies its solution only through Fig. 7 and an unspecified line $L$. Lemmas 6–8, 11 and the two Lemmas 12 describe regions of figures. The finite-horizon analysis of § 11 has no numbered result, and neither does the nonlinear utility of § 18.

Useful infrastructure: the derivative formulas (13.1) for the $K_i$, a first-variation lemma for $f(T)$ under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter VIII, pp. 222–244. https://doi.org/10.2307/j.ctv1nxcw0f
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
• J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x