Mechanism Design

Motivation

Display advertising is sold one impression at a time, mostly through second-price auctions with reserve prices. A reserve tailored to each buyer and to the features of the impression can raise the seller's revenue considerably, but the right reserve depends on the buyers' valuations, which the seller does not know and must learn from past auctions. The buyers participate in the same exchange day after day and know that their bids feed the seller's learning, so a patient buyer may bid untruthfully today to obtain lower reserves tomorrow. Learning reserve prices from strategic buyers is therefore a joint problem of statistics and incentives.

Golrezaei, Javanmard and Mirrokni (arXiv:2002.11137, Operations Research 69(1), 2021) study this problem in a contextual model and propose the policy CORP (Contextual Robust Pricing). Earlier work on learning against strategic buyers considered a single buyer facing posted prices, without contexts: Amin, Rostamizadeh and Syed (NeurIPS 2013) introduced the discounted strategic buyer, and contextual and revenue-optimization variants followed (Amin, Rostamizadeh and Syed, NeurIPS 2014; Mohri and Muñoz Medina, NeurIPS 2015). Personalized reserves in second-price auctions were studied by Paes Leme, Pál and Vassilvitskii (2016). The present paper treats many buyers, personalized reserves, contexts in $\mathbb R^d$ and censored observations (the seller sees who won, not the valuations).

Setting

In every period $t=1,2,\dots$ the seller observes a feature vector $x_t\in\mathbb R^d$, drawn i.i.d. from a law $\mathcal D$ supported in the unit ball. Each of $N$ buyers has the valuation

$$v_{it}=\langle x_t,\beta_i\rangle+z_{it},$$

where $\beta_i\in\mathbb R^d$ is an unknown preference vector with $\|\beta_i\|\le B_p$ and the noises $z_{it}$ are i.i.d. with a known density $f$ on $[-B_n,B_n]$, mean zero, and distribution function $F$. Assumption 1 asks $F$ and $1-F$ to be log-concave on $[-B_n,B_n]$.

Each period runs a lazy second-price auction with personalized reserves $r_{it}$: the highest bidder $i^\star$ gets the item if $b_{i^\star t}\ge r_{i^\star t}$ and pays $\max\{r_{i^\star t},\max_{j\neq i^\star}b_{jt}\}$; nobody else pays. The benchmark knows the $\beta_i$ and sets $r^\star_i(x)=\arg\max_y y\,(1-F(y-\langle x,\beta_i\rangle))$ (4); its expected revenue against truthful buyers is $\mathrm{rev}^\star_t$ (5).

CORP works in episodes $E_k=\{\ell_k,\dots,\ell_{k+1}-1\}$ with $\ell_k=2^{k-1}$. At the start of episode $k$ it computes, for each buyer, a maximum-likelihood estimate $\hat\beta_{ik}$ over $\|\beta\|\le B_p$ from the censored outcomes of episode $k-1$ (8)–(9). In each period of episode $k$, with probability $1/\ell_k$ it explores: one uniformly chosen buyer is offered the item at a price uniform on $[0,B_p+B_n]$. Otherwise it exploits with reserves $r_{it}=\arg\max_y y\,(1-F(y-\langle x_t,\hat\beta_{ik}\rangle))$ (10).

Buyer $i$'s bid may depend on his own history of valuations, bids, allocations and payments, on $x_t$, on $v_{it}$ and on private randomness. His utility is $\sum_t\gamma^t\,\mathbb E[v_{it}q_{it}-p_{it}]$ with a discount factor $\gamma\in(0,1)$, and buyers are utility-maximizing. The regret after $T$ periods is $\sum_{t=1}^T(\mathrm{rev}^\star_t-\mathrm{rev}_t)$, worst case over $\beta$ and $\mathcal D$ (7).

Formalization targets

Goal: Theorem 4.1 (p. 23)

There is $C$, depending only on $B_p,B_n,M,f,c_{\min},c_{\max}$, such that for all $N,d\ge1$, $T\ge2$, $\gamma\in(0,1)$, all admissible $\mathcal D,\beta$ and all utility-maximizing buyers,

$$\mathrm{Regret}(T)\le C\,N d\Big(\log(Td)\log T+\frac{\log^2T}{\log^2(1/\gamma)}\Big).$$

Milestones, in the order the proof uses them

• Proposition 3.1 (p. 15): the reserves (4) are revenue-optimal against truthful buyers.
• Lemma 1 (p. 56): the conditional revenue $W_{it}$ is flat at $r^\star_{it}$ and has a bounded second derivative.
• Lemma 2 (p. 56): $|r^\star_{it}-r_{it}|\le|\langle x_t,\beta_i-\hat\beta_{ik}\rangle|$.
• Lemma 3 (p. 57): the second-highest bid and the competing bid move by at most the shading and overbidding.
• Proposition 9.2 (p. 53): per episode, a utility-maximizing buyer lies $O(\log(\ell/\delta)+\log(\ell N)/\log(1/\gamma))$ times, and his total shading and overbidding are $O(\log(\ell N)/\log(1/\gamma))$, with high probability.
• Corollary 18.2 (p. 88): the vector Freedman inequality.

Significance

If true, Theorem 4.1 says that a seller can learn personalized, contextual reserves from censored data at a cost logarithmic in $T$ and linear in $Nd$, even when buyers manipulate their bids. The strategic term vanishes as buyers become impatient. The episodic delay between a bid and its effect on reserves, together with the random exploration prices, is what makes untruthful bidding unprofitable. The lemmas are of independent use. Proposition 3.1 and Lemma 2 concern the monopoly price under log-concave noise. Lemma 3 is a deterministic fact about second-price auctions. Corollary 18.2 is a vector concentration inequality.

Status. None of these results is machine-checked anywhere known to us. The paper's printed proof has gaps. Proposition 9.1 (p. 52), which bounds the estimation error of the MLE by the number of lies, fails as printed. With uniform noise a single lie per episode keeps the estimate a constant distance from $\beta_i$. Its supporting Lemma 5 uses a constant $u_F$ that is infinite for every compactly supported $F$ (p. 71). Its curvature bound (89) also fails when a likelihood term leaves the support of $f$. Lemma 6 (p. 76) conditions on an event the exploration lottery itself moves. A proof of Theorem 4.1, or a counterexample to it, would settle the question. The goal is stated as the paper states it, and is neither asserted nor denied here.

Difficulty

The natural route is the paper's. First bound the estimation error of the censored MLE in terms of the number of lies. Then bound the number of lies by comparing a lie's discounted future gain with its immediate loss under the exploration lottery. Finally sum over episodes.

The first step is where it breaks. With noise supported on $[-B_n,B_n]$, an observation whose threshold falls outside the support carries no curvature. Its likelihood term is constant or $+\infty$, so the minimizer of (9) is in general a set, not a point. A minimizer at the wrong end of that set can keep the reserve below the benchmark for many episodes, even with truthful buyers. Any proof must say which minimizer CORP takes, or show that all of them work. The second step must handle buyers who react to one another through their histories; the paper's proof holds the other buyers' bids fixed. The concentration steps need a vector martingale inequality and a covariance concentration bound, neither of which is in Mathlib.

Formalization scope

Lean represents features as EuclideanSpace ℝ (Fin d) and buyers as Fin N. Periods are indexed from $0$ internally (Lean's $n$ is the paper's $t=n+1$), and episodes likewise (Lean's $e$ is the paper's $k=e+1$, so $\ell_k=2^e$). Period $1$ always explores. The per-period randomness consists of the features, the noises, the exploration coin, the chosen buyer, the exploration price and the buyers' seeds. It is independent across periods, under Measure.infinitePi, and the play is defined by recursion over periods. The likelihood (9) takes values in $[0,+\infty]$ with $-\log 0=+\infty$; a real-valued Real.log would make impossible observations free and change the estimator. The estimator (8) and the reserve rule (10) are arbitrary measurable selections of the argmin and argmax, quantified universally. No tie-break or uniqueness is added. The same reserve rule defines the benchmark (4).

Standing assumptions and added hypotheses.

• The noise density is continuous on $[-B_n,B_n]$, with mass one and mean zero, and Assumption 1 holds.
• $\|x\|\le1$ almost surely, and $c_{\min}/d\,\|u\|^2<\mathbb E\langle x,u\rangle^2\le c_{\max}/d\,\|u\|^2$; the proof uses these eigenvalue bounds (pp. 57, 72–73).
• Bids are at most $M$ (p. 14) and pairwise distinct almost surely (p. 20).
• Strategies and selections are measurable, $N,d\ge1$ and $T\ge2$.
• Utility-maximizing is pinned as the inequality the proof uses on p. 77: no buyer gains by switching to truthful bidding from the start of any episode on. Every best-response profile satisfies it, and the all-truthful profile does too.
• Exploration is a posted price to the chosen buyer.
• Lemma 1 adds $f\in C^1(\mathbb R)$, which its proof uses.
• Lemma 2 adds that both indices exceed $-B_n$; without that, the argmax is unbounded.
• Lemma 3's (45) adds that another buyer wins; as printed it fails when nobody wins.
• Corollary 18.2 adds $u_0=0$.

Ruled out. The constant $C$ comes before every instance, horizon, selection and strategy, so a bound depending on $T$ or on the instance does not count. The policy is CORP as defined, not any reserve-setting rule. The rationality hypothesis is satisfiable.

Infrastructure. A complete development needs the following.

• Measurability of the recursive play.
• The monopoly price under log-concavity (Proposition 3.1, Lemma 2).
• Censored-likelihood estimation with compactly supported noise.
• A vector Freedman inequality (Corollary 18.2, reusable).
• Covariance concentration for bounded vectors.

Contributions on any milestone are welcome. So is a formal counterexample to the goal in the model as stated, for example with one truthful buyer, uniform noise and the smallest minimizer of (9).

Out of scope. CORP-II and SCORP (Theorems 5.1–5.3, Propositions 11.1–11.2) and the extensions of Appendix 8 are not part of this mission. Proposition 9.1, Lemma 5, Lemma 6 and Theorem 18.1 are not posed (see Significance).

Selected references

• N. Golrezaei, A. Javanmard, V. Mirrokni, Dynamic Incentive-Aware Learning: Robust Pricing in Contextual Auctions, Operations Research 69(1), 2021; read as arXiv:2002.11137v1. https://arxiv.org/abs/2002.11137
• K. Amin, A. Rostamizadeh, U. Syed, Learning Prices for Repeated Auctions with Strategic Buyers, NeurIPS 2013. https://papers.nips.cc/paper/2013/hash/1e6e0a04d20f50967c64dac2d639a577-Abstract.html
• R. Paes Leme, M. Pál, S. Vassilvitskii, A Field Guide to Personalized Reserve Prices, WWW 2016. https://doi.org/10.1145/2872427.2883071
• J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16, 2011. https://doi.org/10.1214/ECP.v16-1624
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

Motivation

Firms that customize products, especially in business-to-business and service markets, need to learn what each customer wants before designing for that customer. Liang Guo's paper The Voice of Customers in Customization (SSRN 3994319; published in Management Science, DOI 10.1287/mnsc.2021.04025) compares two ways a seller can learn a customer's preference. Under A-Learning the customer describes its preference and the seller designs the product. Under O-Learning the customer proposes the design itself and the seller decides whether to accept it. The customer's preference is private, and the price is bargained after the product has been made, so a customer has a reason to misrepresent itself in either case: a customer believed to value quality less is charged less.

This mission formalizes the paper's characterization of when O-Learning reveals preferences without distortion: each customer type requests exactly the design it would request if its preference were public. The paper calls this the cheap-signaling equilibrium. A companion mission in this series formalizes the analogous result for A-Learning (Proposition 1), and another shows that O-Learning has no separating equilibrium at all below the threshold found here.

Setting

A seller faces buyers whose quality preference is $\theta\in\{\theta_H,\theta_L\}$ with $\theta_H>\theta_L>0$. Each buyer knows its own $\theta$. The seller holds the prior that a fraction $\alpha\in(0,1)$ of buyers has $\theta_H$. A product has a quality $q\ge 0$. Producing it costs $kq^2$ and selling it costs $sq^2$, with $k,s>0$. The selling cost is incurred before the price is set. In the price stage either party makes a take-it-or-leave-it offer: the seller with probability $\gamma\in(0,1)$, charging $\hat\theta q$ where $\hat\theta$ is its belief about the buyer, and the buyer with probability $1-\gamma$, offering $kq^2$.

The O-Learning game has three stages.

1. Each buyer submits a quality request $q(\theta)\ge 0$.
2. The seller, holding a posterior belief $\hat\theta(q)$, accepts or rejects the request. It accepts if and only if its expected profit is nonnegative:

$$\gamma(\hat\theta q-kq^2)-sq^2\ge 0.$$

3. The price is set as above. A rejected request ends the game with payoff $0$ to both parties.

A buyer of true preference $\theta$ whose request $q$ is accepted under belief $\hat\theta$ expects

$$\mu(q,\theta,\hat\theta)=\gamma\max\{\theta q-\hat\theta q,0\}+(1-\gamma)\max\{\theta q-kq^2,0\}.\tag{9}$$

A separating equilibrium consists of distinct requests $q_H\ne q_L$ and a belief function $\hat\theta(\cdot)$ satisfying three conditions. Beliefs are consistent on the equilibrium path: $\hat\theta(q_H)=\theta_H$ and $\hat\theta(q_L)=\theta_L$. Beliefs off the path are arbitrary. No type gains by deviating to any other request $q\ge 0$.

If the preference were public, the buyer would choose $q$ to maximize $\mu(q,\theta,\theta)$ subject to acceptance. The solution is the first-best request

$$q^*(\theta)=\min\Big\{\frac{\gamma\theta}{s+\gamma k},\ \frac{\theta}{2k}\Big\}.$$

The thresholds are

$$\Lambda_{H1}=\frac{\gamma(s+k)}{(1-\gamma)s},\qquad \Lambda_{H2}=\frac{1+\gamma}{1-\gamma},\qquad \Lambda_L=\frac{s}{\gamma k},\qquad \Lambda=\max\{\min\{\Lambda_{H1},\Lambda_{H2}\},\Lambda_L\}.$$

Formalization targets

Goal: Proposition 3 (p. 17)

The requests $q^O_H=q^*(\theta_H)$, $q^O_L=q^*(\theta_L)$ form a separating equilibrium for some belief function if and only if

$$\frac{\theta_H}{\theta_L}\ge\Lambda.$$

When this holds, the equilibrium is supported by the out-of-equilibrium belief $\hat\theta(q)=\theta_L$ if $\gamma\le s/k$, and by $\hat\theta(q)=\theta_H$ if $\gamma\ge s/k$.

Milestones

In attack order:

1. Seller acceptance (§3.3, p. 16). For $q\ge 0$, the seller accepts a request iff $q\le\gamma\hat\theta/(s+\gamma k)$.
2. The first-best request solves (10) (§3.3, p. 16). $q^*(\theta)$ is the unique maximizer of $\mu(q,\theta,\theta)$ over the acceptable requests.
3. The case form of $q^*$ (Appendix, Proof of Proposition 3, p. 28). $q^*(\theta)=\gamma\theta/(s+\gamma k)$ if $\gamma\le s/k$, and $q^*(\theta)=\theta/(2k)$ if $\gamma\ge s/k$.
4. Necessity of (11)–(12) (p. 17). If $(q^O_H,q^O_L)$ is a separating equilibrium under any beliefs, then

$$\mu(q^*(\theta_H),\theta_H,\theta_H)\ge\mu(q^*(\theta_L),\theta_H,\theta_L)\quad\text{and}\quad\mu(q^*(\theta_L),\theta_L,\theta_L)\ge\mu(q^*(\theta_H),\theta_L,\theta_H).$$

5. $\gamma\le s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H1}$, and $\mathrm{IC}'_L\iff\theta_H/\theta_L\ge\Lambda_L$.
6. $\gamma\ge s/k$ (p. 28). $\mathrm{IC}'_H\iff\theta_H/\theta_L\ge\Lambda_{H2}$, and $\mathrm{IC}'_L$ holds strictly.
7. $\Lambda_{H1}\le\Lambda_{H2}\iff\gamma\le s/k$ (p. 28).

Significance

Proposition 3 locates the boundary of truthful self-design. Above $\Lambda$, a buyer who designs its own product can both reveal its type and obtain its full-information design. The seller then learns preferences without distorting quality. Below $\Lambda$, the companion mission shows that no separating equilibrium exists at all. The paper builds on this threshold. Proposition 7 compares $\Lambda$ with the A-Learning threshold $\Delta$ to decide which learning mode supports customization over a wider range of preferences. Proposition 8 compares the seller's and buyers' payoffs in the two separating equilibria and shows that the seller prefers to design while the buyers prefer to self-design.

The result is proved in the paper's Appendix. As far as the series' searches show, it has not been machine-checked. This mission poses a formal version of the O-Learning game, its equilibrium notion, and the deviation arguments the paper sketches in a sentence each.

Difficulty

The incentive constraints are polynomial inequalities in the ratio $\theta_H/\theta_L$ once $q^*$ is substituted. The work is elsewhere.

First, the equilibrium quantifies over every request $q\ge 0$, not only over mimicking the other type. A deviation interacts with the belief the seller holds at that request and with the acceptance rule, and the payoff (9) has two kinks. The proof shows that the two stated off-path beliefs deter every deviation. Each regime needs a different belief: the low-type belief works when the acceptance constraint binds at the first-best, and the high-type belief works when it does not.

Second, the "only if" direction has to hold for every belief function. The argument must show that mimicking the other type's first-best request is always accepted, whatever the seller believes elsewhere.

Third, the paper's proof writes the payoffs without the $\max\{\cdot,0\}$ terms. Those identities hold only on part of the domain, and the formal argument has to track where.

Formalization scope

The O-Learning objects live in the namespace CustomerVoice.OLearn, in a single definition file. The model is a structure with real fields $\theta_H,\theta_L,\alpha,\gamma,k,s$. Buyer types use the shared CustomerVoice.ALearn.BType, an inductive type with constructors H and L. The standing assumptions $\theta_H>\theta_L>0$, $\alpha,\gamma\in(0,1)$ and $k,s>0$ are a hypothesis of every theorem. $\alpha$ does not enter this mission but is kept as printed. No other hypothesis is added.

Commitments of the formalization:

• Qualities, requests and deviations are real numbers $q\ge 0$.
• The payoff $\mu$ keeps both $\max\{\cdot,0\}$ terms.
• The seller accepts at indifference, as the paper prints its acceptance rule.
• A rejected request pays $0$.
• A belief function is any total map from requests to the two types. It is pinned only on the equilibrium path.
• The price stage is in reduced form, entering only through (9) and the acceptance inequality.
• Optimality in (10) is stated as attainment of the maximum (IsMaxOn on the acceptable interval) together with uniqueness.

Ruled-out trivializations. Acceptance is the printed inequality, not the threshold $q\le\gamma\hat\theta/(s+\gamma k)$, which is milestone 1. The requests are $q^*(\theta)$, and milestone 2 proves that $q^*(\theta)$ solves (10). The equilibrium is a perfect Bayesian equilibrium against all deviations, not the conjunction of (11) and (12). The "only if" direction quantifies over all belief functions. $\Lambda$ is the printed expression, not an infimum of ratios at which an equilibrium exists.

The development needs only elementary real algebra and one-variable concave quadratics from Mathlib. The equilibrium definition is a template for the other O-Learning mission of the series. Proofs of any milestone, and alternative arguments for the deviation step, are welcome.

The source is the SSRN author version (SSRN 3994319, version of 2023-11-29). All page and display numbers refer to it, and the proofs behind the milestones are in its Appendix.

Selected references

• Liang Guo, The Voice of Customers in Customization, SSRN working paper 3994319, version of 2023-11-29. https://ssrn.com/abstract=3994319
• Liang Guo, The Voice of Customers in Customization, Management Science. https://doi.org/10.1287/mnsc.2021.04025
• Vincent P. Crawford and Joel Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390

Motivation

A seller who must auction one item without knowing how buyers value it needs a mechanism that performs acceptably against every plausible value distribution. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478, Operations Research 2025) measure performance by regret: the expected revenue lost relative to a seller who knows the realized valuations and extracts the highest one. Their main result (Theorem 1, the subject of mission I of this series) shows that against independent and identically distributed valuations the minimax-regret mechanism is a second-price auction whose reserve price is random, drawn from an explicit distribution.

Practitioners rarely randomize reserves. The natural benchmark is the familiar second-price auction with a fixed deterministic reserve $r$, and the question this mission addresses is how much is lost by insisting on a deterministic reserve: what is the worst-case regret of that auction, and which reserve minimizes it? The paper answers this exactly in Proposition 5 (§5.2.1, p. 24, proof in Appendix D, pp. App-10–11). For a single buyer, regret-optimal posted pricing was studied by Bergemann and Schlag (2008), where a deterministic price $1/2$ has worst-case regret $1/2$; Proposition 5 is the $n$-buyer version of that benchmark.

Setting

There are $n\ge1$ buyers with valuations $v=(v_1,\dots,v_n)$ in the type cube $[0,1]^n$, drawn from a joint distribution $\mathbf F$ unknown to the seller. Write $v^{(1)}=\max_i v_i$ and $v^{(2)}$ for the second-highest valuation. A direct mechanism charges buyer $i$ a payment $p_i(v)$, and its regret under $\mathbf F$ is

$$R_n(m,\mathbf F)=\mathbb E_{v\sim\mathbf F}\Big[v^{(1)}-\sum_{i=1}^n p_i(v)\Big].$$

The second-price auction with reserve $r$, $\mathrm{SPA}(r)$, gives the item to the highest bidder if the highest bid is at least $r$, at price $\max(v^{(2)},r)$, and otherwise does not sell. Its revenue is $\max(v^{(2)},r)\,\mathbf 1(v^{(1)}\ge r)$.

Three classes of distributions on $[0,1]^n$ are considered:

• $\mathcal F_{\mathrm{iid}}$: product laws $G^{\otimes n}$, with $G$ a law on $[0,1]$;
• $\mathcal F_{\mathrm{aff}}$: exchangeable laws (invariant under permuting buyers) that are affiliated, meaning $\Pr(A\cap B\mid S)\ge\Pr(A\mid S)\Pr(B\mid S)$ for all increasing sets $A,B$ and every sublattice $S$ (a set closed under coordinatewise minimum and maximum);
• $\mathcal F_{\mathrm{mix}}$: mixtures of i.i.d. laws, whose joint CDF is $\mathbf F(v)=\int\prod_i G(v_i)\,d\mu(G)$ for a probability measure $\mu$ on distributions.

The worst-case regret of $\mathrm{SPA}(r)$ over a class $\mathcal F$ is $\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)$. The closed form found by the paper is

$$W_n(r)=\begin{cases}\max(1-r,\,r), & n=1,\\[2pt] \dfrac{(1-r)^n(n-1)^{n-1}}{((1-r)n-r)^{n-1}}, & n\ge 2,\ r\le\tfrac12,\\[4pt] r, & n\ge2,\ r>\tfrac12,\end{cases}$$

called wcFixed n r in the Lean development.

Formalization targets

Goal: Proposition 5

For every $n\ge1$, every class $\mathcal F\in\{\mathcal F_{\mathrm{iid}},\mathcal F_{\mathrm{aff}},\mathcal F_{\mathrm{mix}}\}$ and every $r\in[0,1]$,

$$\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)=W_n(r),$$

the no-reserve auction has $W_n(0)=1$ for $n=1$ and $\big(\frac{n-1}{n}\big)^{n-1}$ for $n\ge2$, and

$$\min_{r\in[0,1]}W_n(r)=W_n\Big(\frac1{n+1}\Big)=\Big(\frac n{n+1}\Big)^n,$$

with $r^*=1/(n+1)$ the unique minimizer.

Milestones

1. The regret of $\mathrm{SPA}(r)$ under an i.i.d. law with marginal CDF $F$: $rF_-(r)^n-\int_0^rF^n+\int_r^1(nF^{n-1}-nF^n)$.
2. For $n\ge2$, the maximum of $rc^n+(1-r)(nc^{n-1}-nc^n)$ over $c\in[\frac{n-1}{n},1]$ equals $W_n(r)$.
3. For $n=1$, the maximum of $rc+(1-r)(1-c)$ over $c\in[0,1]$ is $\max(1-r,r)$.
4. $W_n$ is minimized on $[0,1]$ exactly at $1/(n+1)$, with value $(n/(n+1))^n$.
5. For $n\ge2$, every exchangeable affiliated law gives $\mathrm{SPA}(r)$ regret at most $W_n(r)$.

Significance

The result. Proposition 5 gives the exact price of determinism. The optimal fixed reserve $1/(n+1)$ has worst-case regret $(n/(n+1))^n$: $1/2$ for one buyer, $4/9$ for two. The minimax regret of the optimal randomized auction is about $0.368$ and $0.324$ for the same cases, so the benchmark shows how much of the paper's improvement comes from randomizing the reserve. Both values converge to $1/e$ as $n\to\infty$. Proposition 5 also shows that the worst case does not change when valuations are positively dependent (affiliated, or mixtures of i.i.d.), the same robustness the paper establishes for its optimal mechanism.

Formalizing it. The result is proved on paper in the paper's Appendix D, and no machine-checked version is known. A formal proof needs an expression of the expected revenue of a second-price auction through the order-statistic CDFs, a careful treatment of atoms at the reserve, two elementary but fiddly one-variable optimizations, and, for $\mathcal F_{\mathrm{aff}}$ and $\mathcal F_{\mathrm{mix}}$, the reduction to the i.i.d. case.

Difficulty

The supremum over $\mathcal F_{\mathrm{iid}}$ is not attained. The auction's revenue jumps at the reserve: a buyer valued exactly at $r$ buys, while one valued just below does not. Nature exploits this with two-point laws placing mass just below $r$ and the rest at $1$, and the regret approaches $W_n(r)$ only in the limit. So the first idea, exhibiting a maximizing distribution, fails, and any formalization must treat the worst case as a least upper bound. The upper bound over $\mathcal F_{\mathrm{aff}}$ is the real difficulty: it rests on an order-statistic identity and on an inequality between the CDFs of the maxima of $n-1$ and $n$ affiliated valuations, which in turn needs properties of affiliation that are quoted from Milgrom and Weber (1982) rather than proved in the paper. For $\mathcal F_{\mathrm{mix}}$ the bound needs the regret to be linear in the mixing measure, i.e. a disintegration of the mixture law through its joint CDF.

Formalization scope

• Representation. Buyers are Fin n; valuations are vectors Fin n → ℝ; a distribution is a probability measure on Fin n → ℝ whose complement of the cube $[0,1]^n$ is null. $\mathcal F_{\mathrm{iid}}$ is the set of products Measure.pi (fun _ => G) of a probability law G on $[0,1]$. $\mathcal F_{\mathrm{mix}}$ uses a probability measure on Measure ℝ with the Giry σ-algebra and states the CDF identity of Definition 6 for every $v$.
• The auction. $\mathrm{SPA}(r)$ is the random-reserve auction SPA ρ at ρ = Measure.dirac r; the winner pays $\max(v^{(2)},r)$ when its bid is at least $r$. Ties go to the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule).
• Affiliation is stated cross-multiplied, $\mu(A\cap S)\mu(B\cap S)\le\mu(A\cap B\cap S)\mu(S)$, for measurable increasing $A,B$ and measurable sublattices $S$.
• Conventions committed to. The reserve ranges over $[0,1]$ (the page leaves this implicit; for $r>1$ the closed form is false). Worst-case regret is IsLUB of the set of regrets, not a maximum and not sSup. "The optimal reserve" is IsLeast of $W_n$ on $[0,1]$, its value at $1/(n+1)$, and uniqueness of the minimizer.
• Ruled out. A statement with IsGreatest would be false (the supremum is not attained); sSup of the regret image would be a junk value if the image were unbounded; classes without the $[0,1]^n$ support condition, or $r$ unconstrained, change the theorem.
• Infrastructure. Expected revenue of a second-price auction via order statistics, the CDF of the maximum and second maximum of i.i.d. variables, and the reduction of mixtures to their components are reusable for the rest of this series and for auction theory generally. Contributions to the affiliation inequalities (Milgrom–Weber) are particularly welcome.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 560–569, 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1089–1122, 1982. https://doi.org/10.2307/1911865

Motivation

A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).

This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to $e/(e+1)$ when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).

Setting

There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector $(Y,Z)$ with $Y,Z\ge0$. Values are additive: receiving both goods is worth $Y+Z$. The seller knows the distribution of the vector but not the realized values. In this mission, $Y$ and $Z$ are independent and have the same arbitrary probability law $\nu$ on $\mathbb R_{\ge0}$. A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.

A direct mechanism $\mu=(q,s)$ takes a reported pair $x=(y,z)$ and returns an allocation probability $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$ to the seller. The buyer's payoff from reporting truthfully is $b(x)=q(x)\cdot x-s(x)$. The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).

Write $R(\mu;X)$ for the expected payment under a valuation law $X$ and $\operatorname{Rev}(X)$ for the supremum of $R(\mu;X)$ over feasible, IC, IR mechanisms. For one good, write $\operatorname{Rev}_1(\nu)$. The separate-selling revenue for two identically distributed goods is $\operatorname{SRev}(Y,Z)=2\operatorname{Rev}_1(\nu)$. Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue $p\Pr[Y\ge p]$; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).

Formalization targets

Theorem B: the guarantee for two i.i.d. goods

The goal is the exact upper bound written at the start of the paper's proof:

$$\operatorname{Rev}(Y,Z)\le\frac{e+1}{e}\bigl(\operatorname{Rev}(Y)+\operatorname{Rev}(Z)\bigr)=\frac{e+1}{e}\operatorname{SRev}(Y,Z).$$

Equivalently, separate selling guarantees at least $e/(e+1)$ of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant $(e+1)/e$, not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).

Supporting targets

The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant $1/e$. The final inequality for the right side of (12) is stated for every nondecreasing allocation function into $[0,1]$, as required by the paper's argument on pp. 33–35.

Significance

Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its $e/(e+1)$ guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).

The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.

Difficulty

The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact $1/e$ numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).

Formalization scope

Valuations are finite vectors $\iota\to\mathbb R_{\ge0}$; the main theorem fixes $\iota=\operatorname{Fin}(2)$. The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds $0\le q_i\le1$. It requires IC and IR pointwise on all reports. No positive transfer (NPT) means $s(x)\ge0$ and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.

An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write $r=\operatorname{Rev}_1(\nu)$ as a real number explicitly assume $r<\infty$; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term $W$ uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on $\nu$, or a rounded constant.

The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.

Selected references

• Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory, 2017. Source used here: arXiv:1204.1846v3.
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. DOI:10.1287/moor.6.1.58.

Why a one-sided market can have a core

Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.

The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.

The market and its allocations

Let $W$ be a finite set of workers, with $m=|W|$. A coalition technology $v$ assigns a real output $v(C)$ to each worker set $C\subseteq W$. A one-sided allocation consists of a partition $P=(C_z)$ of all workers and one real salary $s_i$ for each worker. The parts of $P$ are disjoint and cover $W$. Each worker has a utility $\mu^i(s_i)$ that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.

The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:

$$s_i\ge 0\quad(i\in W),\qquad \sum_{i\in W}s_i\le\sum_{C\in P}v(C).$$

It does not require each partition block to finance its own salaries. An improving coalition is a worker set $C$ with salaries $r_i\ge s_i$ for every $i\in C$, a strict inequality for at least one member, and $\sum_{i\in C}r_i\le v(C)$. A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.

To state gross substitutes (GS), imagine $m+1$ identical firms, each with production $v$. At a salary vector $s:W\to\mathbb R$, a firm's profit from employing $C$ is $\pi(C;s)=v(C)-\sum_{i\in C}s_i$; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from $s$ to $s'$, then for every demanded set at $s$ there is a demanded set at $s'$ containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.

Formalization targets

Goal: Theorem 3

Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:

$$v(C\cup\{i\})-v(C)\ge 0,\qquad v(\varnothing)=0,\qquad \operatorname{GS}(v).$$

The goal is the exact existence statement

$$\exists (P,s),\quad (P,s)\text{ is a one-sided strict-core allocation for }v.$$

Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.

What the result gives

The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.

The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.

Why the transfer is delicate

A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.

Formalization scope

Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when $m=0$. Salaries and output are real. In the fictitious market, every firm uses the same $v$, each worker's utility at every firm is $\mu^i(s)$, and reservation salary is zero, matching unemployment utility $\mu^i(0)$. The milestones retain arbitrary strictly increasing continuous functions $\mu^i$; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.

Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.

Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1, 1971, pp. 11–26. DOI: 10.1007/BF01753431.

Motivation

Labor markets match heterogeneous workers to heterogeneous firms, and the terms of each match — the salary — are negotiated. Kelso and Crawford (Econometrica 50 (1982)) studied such a market in which a firm may hire many workers, its output depends on the whole set it hires, and salaries are set worker by worker. Their model contains the marriage problem of Gale and Shapley (1962) and the assignment game of Shapley and Shubik (1971) as special cases, and its gross substitutes condition later became the central hypothesis of the theory of matching with contracts and of ascending auctions for indivisible goods (Hatfield and Milgrom, AER 2005; Gul and Stacchetti, JET 1999).

Markets of this kind usually have many stable outcomes, so which one arises depends on how the market is organized. Gale and Shapley showed that their deferred-acceptance procedure picks the stable matching that is best for the proposing side. Crawford and Knoer (Econometrica 1981) proved the analogue for one-to-one matching with money. Theorem 4 of Kelso and Crawford extends it to firms that hire many workers, under gross substitutes: the paper's salary-adjustment process, in which firms make offers, ends at the end of the strict core that favors the firms.

Setting

There are finitely many workers $i \in W$ and firms $j \in F$. Worker $i$ values working for firm $j$ at salary $s$ by $u^i(j; s)$, strictly increasing and continuous in $s$. Firm $j$ produces $y^j(C)$ when it hires the set $C$ of workers and earns the profit $\pi^j(C; s^j) = y^j(C) - \sum_{i\in C} s_{ij}$ at the salary vector $s^j$. The number $\sigma_{ij}$ is the starting permitted salary for $i$ at $j$; Section 2 initially defines it as a reservation salary, and Section 5 permits it to be perturbed. The paper's standing assumptions are (MP), $y^j(C\cup\{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$; (NFL), $y^j(\varnothing) = 0$; and (GS): if $C$ maximizes firm $j$'s profit at $s^j$ and salaries rise weakly to $\tilde s^j$, some profit-maximizing set at $\tilde s^j$ still contains every worker of $C$ whose salary did not change.

In a discrete market with unit $\delta > 0$, firm $j$ may offer worker $i$ only the salaries $\sigma_{ij} + k\delta$, $k \in \mathbb{N}$. An allocation assigns every worker $i$ to a firm $f(i)$ at a salary; $C^j$ is the set hired by $j$. It is individually rational if every worker gets at least $\sigma_{if(i)}$ and every firm a nonnegative profit. A firm and a set of workers at permitted salaries improve upon it if all of them are weakly better off and one of them strictly; they strictly improve upon it if all are strictly better off. Discrete strict core allocations (D2) admit no improving coalition, discrete core allocations (D3) no strictly improving one.

The salary-adjustment process (R1–R5) starts with permitted salaries $s_{ij}(0) = \sigma_{ij}$ and offers from every firm to every worker. In each round, each firm offers jobs to a profit-maximizing set at its current permitted salaries, repeating unrejected offers; each worker holds a favorite offer and rejects the others; a rejected firm's permitted salary for that worker rises by $\delta$. The process stops in a round with no rejections. A worker is (strictly) $s$-possible for firm $j$ if some discrete (strict) core allocation assigns him or her to $j$ at salary $s$. The no-ties conditions are (NTW): a worker who is $s_{ij}$-possible for $j$ is never indifferent between $(j, s_{ij})$ and any permitted salary at another firm; and (NTF): a firm is never indifferent between its profit in a discrete core allocation and the profit from another nonempty set of workers at permitted salaries.

Formalization targets

Goal: Theorem 4 (p. 1495)

Under regularity, (MP), (NFL), (GS) on the permitted salary vectors, (NTW) and (NTF): every run of the process stops at some round, and at every stopping round $T$ the resulting allocation $\phi$ is a discrete strict core allocation with

$$\pi^j(C^j_{A'}; s'^j) \le \pi^j(C^j_\phi; s^j(T)) \qquad \text{for every firm } j \text{ and every discrete strict core allocation } A'.$$

Milestones (proof of Theorem 4, p. 1495)

1. Every equilibrium of the process is a discrete strict core allocation.
2. No worker ever rejects a firm at a salary $s$ at which he or she is strictly $s$-possible for it.
3. For every strict core allocation $(f; s')$, every round $t$ and every worker $i$: $s_{if(i)}(t) \le s'_{if(i)}$.

Significance

Theorem 4 says that the outcome of a decentralized ascending process, in which firms make the offers, is not an arbitrary stable outcome but the one best for every firm simultaneously. This existence of a firm-optimal point of the strict core is itself a consequence. Its Corollary (uniqueness of the equilibrium, mission 5 of this series) and Theorem 5 (an entering firm helps every worker, a departing worker hurts every firm, also mission 5) are both proved from it.

The result has been proved on paper since 1982, and nothing of this paper was on Prove2Me before this series. The mission produces a machine-checked version of the paper's model, of the salary-adjustment process for every tie-breaking rule, and of the firm-optimality argument. The no-money analogue, Gale and Shapley's optimality theorem for college admissions, has a proved formalization on the platform (GS62CollegeAdmissions.PaperInterface.theorem2_applicant_optimality); it does not involve salaries and is credited, not reused.

The series has seven missions: 1 (Theorem 1, convergence to a discrete core allocation), 2 (Theorem 2, the continuous strict core), 3 (Theorem 3, one-sided markets), 4 (this mission), 5 (comparative statics, Theorem 5), 6 (Theorem 6, gross substitutes and returns to workers), 7 (the no-core example of Section 6). This mission does not depend on the others: it states its own copy of the model.

Difficulty

The process is defined for every tie-breaking rule of firms and workers, so the claim concerns an entire family of executions, each indexed by rounds and carrying offers, tentative acceptances and salaries. The firm-optimality statement compares the process outcome with every strict core allocation, objects defined by a nonexistence condition over all coalitions and permitted salaries. The step that does not follow from Theorem 1 alone is that rejections never occur at a strictly possible salary. That claim is about the entire history of a run, not about its final round, and it ties a property of the core to every intermediate rejection. Without the no-ties hypotheses the paper guarantees only that the process stops at a discrete core allocation (D3, Theorem 1).

Formalization scope

Workers and firms are arbitrary finite types, with at least one firm; salaries are real numbers; larger utility is better. A discrete market is given by the unit $\delta > 0$, and the permitted salaries are $\sigma_{ij} + \delta\mathbb{N}$ (the paper's unit is 1; Theorem 2 lets it shrink, so it is kept general). The starting salaries $\sigma_{ij}$ are data; the relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed, because Section 5 perturbs $\sigma_{ij}$ independently of $u^i(0;0)$ to obtain (NTW), and under that relation (NTW) typically fails in round 0. Allocations assign every worker to a firm. (GS) is imposed on the permitted salary vectors of the discrete market only.

Explicit readings of the paper's phrases:

• "converges to" means: every run stops at some round, and every stopping round yields the stated allocation;
• "any other strict core allocation" means any discrete strict core allocation of the same discrete market;
• "at least as good for every firm" is a weak profit inequality at every firm;
• (NTW) and (NTF) are about discrete core allocations (D3), as printed, and "any other non-empty set of workers" in (NTF) is read as a nonempty set different from $C^j$;
• a run of R1–R5 is any sequence of salaries, offers and tentative acceptances obeying the rules, with all ties broken arbitrarily; the statements cover every run.

Statements that quantify over runs would be empty if no run existed, and (NTW), (NTF) are hypotheses about the core that could in principle be contradictory; a sorry-free local check confirms all hypotheses on a market with one firm and one worker and exhibits a run that stops at a strict core allocation, so the goal is not vacuous. Trivializing readings — comparing with continuous strict core allocations, imposing (NTW)/(NTF) only on strict core allocations, or comparing a single firm — are excluded by the statement.

Infrastructure needed: the model, the run encoding, and lemmas about runs (salaries are monotone and stay on the grid, every worker always holds an offer, every run stops — Theorem 1). These are reusable for missions 1 and 5. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912758
• D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
• L. S. Shapley and M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466
• F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531

Motivation

Labour markets match workers to firms that hire teams: a firm's output depends on the whole set of workers it employs, while each worker holds one job. A salary agreement is stable when no firm and group of workers can renegotiate among themselves to the benefit of all of them. Shapley and Shubik (1971) showed that such stable outcomes exist when each firm hires at most one worker and utility is transferable; Crawford and Knoer (1981) extended this to general utilities, still one-to-one. Kelso and Crawford (1982) let firm size be endogenous and identified the condition under which existence survives: workers must be gross substitutes for every firm. Their condition later became the standard assumption for existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti, 1999) and the basis of matching with contracts (Hatfield and Milgrom, 2005).

This mission is the second of a seven-mission series on the paper: 1, the salary-adjustment process; 2, existence of a strict core with continuous salaries (this mission); 3, one-sided coalition formation; 4, the firm-optimal allocation; 5, comparative statics; 6, gross substitutes versus nonincreasing returns; 7, a market with no core. Each mission is self-contained. Nothing of this paper was on Prove2Me before this series.

Setting

There is a finite set $W$ of $m$ workers and a nonempty finite set $F$ of firms. Worker $i$'s utility of working for firm $j$ at salary $s\in\mathbb R$ is $u^i(j;s)$, strictly increasing and continuous in $s$. Firm $j$'s gross product when it hires the set $C\subseteq W$ is $y^j(C)$, and its profit at the salary vector $s^j=(s_{ij})_{i\in W}$ is

$$\pi^j(C;s^j)=y^j(C)-\sum_{i\in C}s_{ij}.$$

The reservation salary $\sigma_{ij}$ is defined by $u^i(j;\sigma_{ij})=u^i(0;0)$, worker $i$'s utility of unemployment. Section 2 of the paper assumes, for every firm $j$:

• (MP) $y^j(C\cup\{i\})-y^j(C)-\sigma_{ij}\ge0$ whenever $i\notin C$;
• (NFL) $y^j(\emptyset)=0$;
• (GS) if $C$ maximizes $\pi^j(\cdot\,;s^j)$ and $\tilde s^j\ge s^j$ componentwise, then some maximizer $\tilde C$ of $\pi^j(\cdot\,;\tilde s^j)$ contains every $i\in C$ with $\tilde s_{ij}=s_{ij}$.

An allocation assigns each worker $i$ to a firm $f(i)$ at salary $s_{if(i)}$; firm $j$ hires $C^j=\{i:f(i)=j\}$. It is individually rational (D1) if $s_{if(i)}\ge\sigma_{if(i)}$ and $\pi^j(C^j;s^j)\ge0$ for all $i,j$. A firm $j$, a set $C$ and salaries $r_{ij}$ improve upon it if $u^i(j;r_{ij})\ge u^i(f(i);s_{if(i)})$ for $i\in C$ and $\pi^j(C;r^j)\ge\pi^j(C^j;s^j)$, with at least one inequality strict; they strictly improve upon it if all are strict. A strict core allocation (D2) is an individually rational allocation no coalition improves upon; a core allocation (D3) is one no coalition strictly improves upon. In the continuous market coalitions may use any real salaries; in the discrete market of unit $\delta>0$ all salaries lie on the grids $\sigma_{ij}+\delta\mathbb N$.

Formalization targets

Goal: Theorem 2

Under regular utilities, (MP), (NFL), the reservation-salary relation and (GS) on all real salary vectors,

$$\exists\,(f;s)\ \text{individually rational that no firm–worker coalition can improve upon (D2).}$$

The goal fixes no grid, no constant and no particular technology.

Milestones, in the order of the paper's proof

1. Every discrete market has a core (p. 1490): for every $\delta>0$, if (GS) holds on grid salary vectors, a discrete core allocation (D3) exists.
2. The gains are bounded above zero (p. 1491, eqs. (8)–(11)): if the continuous market has no strict core allocation, there is $H>0$ such that every individually rational allocation admits a coalition that leaves its workers no worse off and raises its firm's profit by at least $H$.
3. A fine grid inherits the improvement (pp. 1491–1492): with such an $H$, every individually rational grid allocation of unit $0<\delta<H/(m+1)$ can be strictly improved upon in the discrete market.

Significance

Theorem 2 gives existence of a stable assignment of workers to firms with salaries, for arbitrary technologies under which workers are gross substitutes, without any convexity or divisibility of labour. Because the core and the competitive equilibrium coincide in this model when salaries are divisible (p. 1487), it is also an existence theorem for competitive equilibrium in a market with indivisible workers; the example of mission 7 shows that it fails without (GS). The Shapley–Shubik assignment game is the special case $u^i(j;s)=a_{ij}+s$, $y^j(C)=\sum_{i\in C}b_{ij}$ with at most one worker per firm.

The result has been proved since 1982; it has not been machine-checked. Prove2Me holds a formalization of the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core-existence theorem is a different model and is not yet proved, and Murota's gross-substitutes axioms for demand on $\mathbb Z^n$, which concern one price per good rather than firm-specific salary vectors over sets of workers. Neither supplies this market or Theorem 2.

Difficulty

Discrete core allocations exist at every unit $\delta$, so the natural first idea is to take a sequence of them as $\delta\to0$ and pass to a limit. A limit of discrete core allocations need only be a core allocation of the continuous market in the weak sense D3, and a coalition that improves upon the limit may need salaries off every grid; nothing in the discrete statements controls how much a coalition gains, so the blocking coalitions of the continuous market may vanish on the grids. The required control has to be uniform over all individually rational allocations, which form an infinite set, while each blocking comparison involves the utilities of several workers and a nonadditive technology. A second obstacle is in the paper's notation: the gain (8) uses the salary $\rho_{ij}$ with $u^i(j;\rho_{ij})=u^i[f(i);s_{if(i)}]$, which need not exist when $u^i(j;\cdot)$ is bounded.

Formalization scope

Workers and firms are arbitrary finite types; every theorem assumes at least one firm (the paper's $n\ge1$), since with no firm and some worker no allocation exists. Salaries, utilities, outputs and profits are real numbers. An allocation has no unemployment, as in D1. The reservation salaries $\sigma$ are data, and the paper's definition of $\sigma_{ij}$ enters as the hypothesis $u^i(j;\sigma_{ij})=u^i(k;\sigma_{ik})$; it is assumed on the goal and on milestones 2 and 3, where the discretization step needs every improving salary to be at least $\sigma_{ij}$. Milestone 1 assumes neither this relation nor continuous (GS). The standing assumptions of p. 1486, which Theorem 2's sentence does not repeat, are hypotheses of the goal.

Explicit readings of the paper's phrases: "continuous market" means coalitions may use any real salary; "bounded above zero" is one $H>0$ valid for every individually rational allocation, stated without $\rho_{ij}$ by quantifying over admissible coalition salaries; "the unit of measurement smaller than $H/(m+1)$" is $0<\delta<H/(m+1)$ with $m=|W|$ and the division in $\mathbb R$; the discrete market's salaries are $\sigma_{ij}+\delta k$, $k\in\mathbb N$, the paper's integer salaries starting at $\sigma_{ij}$ (R1, R4) with a general unit.

Trivializing formalizations are ruled out: the goal assumes (GS) on all real vectors rather than on one grid (a stronger theorem the paper does not prove), its conclusion is the strict core D2 rather than the weaker core D3, and its hypotheses are satisfiable (a one-worker, one-firm market satisfies all of them).

A complete development needs finite optimization over sets of workers, a compactness argument over the individually rational salary schedules of each assignment, and the existence of discrete core allocations (the existence form of Theorem 1, mission 1). Proofs of the milestones, of the equivalence of D2 and D3 in the continuous market, and lemmas on finite demand correspondences reusable across the series are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job Matching, Coalition Formation, and Gross Substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job Matching with Heterogeneous Firms and Workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912751
• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• F. Gul and E. Stacchetti, Walrasian Equilibrium with Gross Substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
• J. W. Hatfield and P. R. Milgrom, Matching with Contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466

Motivation

Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.

Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.

Timeline.

• 1962: Gale and Shapley, deferred acceptance for one-to-one and many-to-one matching without money.
• 1971: Shapley and Shubik, the assignment game: one-to-one matching with transferable utility; the core is nonempty and is the set of solutions of a dual linear program.
• 1981: Crawford and Knoer, a salary-adjustment process for one-to-one matching with money, converging to the core.
• 1982: Kelso and Crawford, many-to-one matching with money and production complementarities; existence of the core under gross substitutes via the salary-adjustment process (Theorem 1, the target of this mission).

Setting

There are finitely many workers $i \in W$ and firms $j \in F$, with at least one firm. Worker $i$'s utility of working for firm $j$ at salary $s$ is $u^i(j; s)$, strictly increasing and continuous in $s$. Firm $j$'s gross product from hiring the set $C \subseteq W$ is $y^j(C)$, and its profit at the salary vector $s^j = (s_{1j},\dots,s_{mj})$ is

$$\pi^j(C; s^j) = y^j(C) - \sum_{i \in C} s_{ij}.$$

$M^j(s^j)$ is the set of profit-maximizing $C$. Each pair has a starting salary $\sigma_{ij}$. The assumptions (p. 1486) are (MP) $y^j(C \cup \{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$; (NFL) $y^j(\emptyset) = 0$; and (GS): if $C \in M^j(s^j)$ and $\tilde s^j \ge s^j$, some $\tilde C \in M^j(\tilde s^j)$ contains $\{i \in C : \tilde s_{ij} = s_{ij}\}$.

In the discrete market with unit $\delta > 0$, firm $j$ may pay worker $i$ only $\sigma_{ij} + k\delta$, $k = 0, 1, 2, \dots$. An allocation sends each worker $i$ to a firm $f(i)$ at a salary $s_{if(i)}$; it is individually rational (D1) if $s_{if(i)} \ge \sigma_{if(i)}$ and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm $j$, set $C$ and permitted salaries $r^j$ satisfy $u^i(j; r_{ij}) > u^i(f(i); s_{if(i)})$ for all $i \in C$ and $\pi^j(C; r^j) > \pi^j(C^j; s^j)$.

The salary-adjustment process (pp. 1488–1489), verbatim:

R1. Firms begin facing a set of permitted salaries $s_{ij}(0) = \sigma_{ij}$. Permitted salaries at round $t$, $s_{ij}(t)$, remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).

R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries $s^j(t) \equiv [s_{1j}(t), \dots, s_{mj}(t)]$. That is, firm $j$ makes offers to the members of $C^j[s^j(t)]$, where $C^j[s^j(t)]$ maximizes $\pi^j[C; s^j(t)]$. Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm $j$ in round $t - 1$ that was not rejected must be repeated in round $t$. By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.

R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.

R4. Offers not rejected in previous periods remain in force. If worker $i$ rejected an offer from firm $j$ in round $t - 1$, $s_{ij}(t) = s_{ij}(t - 1) + 1$; otherwise $s_{ij}(t) = s_{ij}(t - 1)$. Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.

R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.

Formalization targets

Goal: Theorem 1 (p. 1489)

"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:

$$\Big(\exists \text{ a run}\Big)\ \wedge\ \forall \rho \text{ run}:\ \Big(\exists T:\ \rho \text{ issues no rejections in round } T\Big)\ \wedge\ \Big(\forall T \text{ such rounds},\ \text{outcome}_\rho(T) \text{ is a discrete core allocation}\Big).$$

Milestones, in the paper's order

1. R2 is well defined: a run exists (each firm has a favorite set containing its unrejected offers).
2. Lemma 1: every worker has at least one offer in every period.
3. Lemma 2: after finitely many rounds every worker has exactly one offer and the process stops.
4. Lemma 3: the allocation at a stopping round is individually rational.
5. Lemma 4: the allocation at a stopping round is a discrete core allocation.

Significance

Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).

The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.

Difficulty

The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below $\sigma_{ij}$ or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.

Formalization scope

Lean representation, in namespace KelsoCrawford.Process:

• Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's $n \ge 1$; with no firms and some worker no run exists).
• Allocation assigns every worker to a firm (no unemployment, as in the paper's $f$).
• (GS) is GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.
• The core is D3 with permitted salaries M.grid δ $= \{\sigma_{ij} + k\delta : k \in \mathbb N\}$.
• A Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.

Explicit readings of the paper's phrases:

• "converges in finite time" = every run has a round without rejections; no bound on that round is claimed;
• "to a discrete core allocation" = at every round without rejections, the allocation read off is in the discrete core;
• the unit $1$ of R4 is a parameter $\delta > 0$ (same theorem in rescaled units);
• $\sigma_{ij}$ is data; its defining relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed (a more general statement).

The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below $\sigma_{ij}$ (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1913320
• D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
• L. S. Shapley and M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466