Algorithmic Game Theory

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

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$, the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$, where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$. The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$.

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$, and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

$$C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.$$

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$, in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$. Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$, and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$, the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$. The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$:

$$\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.$$

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$, choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

$$\Pr\{C_t<\varepsilon\}>1-\varepsilon.$$

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$. The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$. Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$: the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$. The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$; nonnegative weights make its numerator zero as well. At horizon $0$, the weighted calibration score is $0$. The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$. Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

• D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
• D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.

Motivation

The core of an exchange economy is the set of allocations that no group of consumers can improve upon by trading only among themselves. The Walras equilibria (competitive equilibria) are the allocations supported by a price system at which every consumer maximizes preference on a budget set. Every Walras equilibrium is in the core, but for a fixed finite economy the core is usually much larger. Edgeworth (1881) conjectured that the core shrinks to the competitive allocations as the number of traders grows; Debreu and Scarf (1963) proved this for replica economies, and Aumann (1964) proved exact equality for an atomless continuum of traders.

Jean-Pierre Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6 (1981) 1–13) gives a third route to the same conclusion, with a fixed finite number of consumers. Coalitions are allowed to be fuzzy: a consumer may join with any rate of participation between 0 and 1. Once all fuzzy coalitions may block, the core of the economy, now called the fuzzy core, is exactly the set of Walras equilibria (Theorem 4.1, p. 6). The paper presents this as a slight modification of the Debreu–Scarf theorem; in Remark 4.2 it observes that Debreu–Scarf's replica coalitions correspond to the rational points of the cube $[0,1]^n$.

This mission formalizes §4 of the paper. It is the fourth mission of a series on the paper; the others treat the cores of fuzzy games with and without side payments and the values of smooth fuzzy games.

Setting

There are $n$ consumers $i \in N = \{1,\dots,n\}$ and $l$ commodities. Consumer $i$ consumes bundles in $\mathbb{R}^l_+$, ranks them by a preference relation $\succcurlyeq_i$ (with strict part $\succ_i$), and owns a set $Y(i) \subset \mathbb{R}^l$ of possible initial endowments. Each $Y(i)$ is closed, convex and comprehensive: whenever $y \in Y(i)$ and $z \ge 0$, also $y - z \in Y(i)$.

A fuzzy coalition is a vector $\tau \in [0,1]^n$; $\tau_i$ is the rate at which consumer $i$ participates, and $A_\tau = \{i : \tau_i > 0\}$ is the set of participants. The coalition $\tau$ disposes of the endowments

$$Y(\tau) = \sum_{i \in N} \tau_i\, Y(i),$$

and its allocations are the families $x_\tau = (x_\tau^i)_{i \in A_\tau}$ of bundles $x_\tau^i \in \mathbb{R}^l_+$ with $\sum_i \tau_i x_\tau^i \in Y(\tau)$; this set is $X(\tau)$. The allocations of the whole economy are $X(N) = X(\tau^N)$, $\tau^N = (1,\dots,1)$.

An allocation $x \in X(N)$ is in the fuzzy core if there is no nonzero fuzzy coalition $\tau$ and allocation $x_\tau \in X(\tau)$ with $x_\tau^i \succ_i x^i$ for every $i \in A_\tau$.

The income of consumer $i$ at prices $p \in \mathbb{R}^l$ is $r_i(p) = \sup_{y \in Y(i)} p\cdot y$, and the budget set is $B_i(p) = \{x \in \mathbb{R}^l_+ : p \cdot x \le r_i(p)\}$. An allocation $\bar x \in X(N)$ is a Walras equilibrium if some price $\bar p \in \mathbb{R}^l$ satisfies, for every $i$,

$$\bar p \cdot \bar x^i = r_i(\bar p) \qquad\text{and}\qquad \bar x^i \succcurlyeq_i x \ \text{ for all } x \in B_i(\bar p).$$

Assumption (1) of §4 requires each preference to be continuous and convex, with $x \succ_i y \Rightarrow \alpha x + (1-\alpha) y \succ_i y$ for $\alpha \in\, ]0,1[$; no consumer to be satiated; and each $Y(i)$ to contain a vector with all coordinates strictly positive.

Formalization targets

Goal: Theorem 4.1

Under assumption (1),

$$\text{fuzzy core} \;=\; \{\text{Walras equilibria}\}.$$

Milestones, from the proof of Theorem 4.1

1. Every Walras equilibrium belongs to the fuzzy core.
2. For an allocation $\bar x \in X(N)$, each set $Q(i) = Y(i) - \{x \in \mathbb{R}^l_+ : x \succ_i \bar x^i\}$ is nonempty.
3. If $\bar x$ belongs to the fuzzy core, then

$$0 \notin \operatorname{co}\Big(\bigcup_{i=1}^n Q(i)\Big).$$

The remaining step of the paper, from milestone 3 to the existence of the equilibrium price, is stated there only as "by known arguments" and is left to the solver as part of the goal.

Significance

The result. Theorem 4.1 is a core equivalence theorem for an economy with finitely many consumers and no replication or continuum of traders. It identifies the competitive allocations as exactly the allocations that are stable against partial coalitions. It also makes visible which coalitions matter: Remark 4.1 attributes the equivalence to the fact that all fuzzy coalitions are allowed to form, so that the set of coalitions is convex. The same fuzzy-coalition device underlies the nonemptiness results for cores of fuzzy games in §5–§7 of the paper.

Formalizing it. The theorem is proved in the paper, in one paragraph that defers its final step to "known arguments". To our knowledge neither the theorem nor the Debreu–Scarf or Aumann core equivalence theorems have been formalized in Lean. A complete development provides a reusable model of an exchange economy with preference relations and comprehensive endowment sets, a checked argument from separation to equilibrium prices, and a template for the classical core equivalence theorems.

Difficulty

The inclusion of the Walras equilibria in the fuzzy core is a budget computation. The converse is the content of the theorem: from the mere absence of improving fuzzy coalitions, a single price vector must be produced that works for all consumers simultaneously. Separating consumer by consumer gives one price per consumer, not a common one, so the coalitional structure has to enter before any price exists. Once a candidate price is available, it still has to be shown nonnegative, each equilibrium bundle has to exhaust its owner's income, and no bundle in a budget set may be strictly preferred; each of these uses a different part of assumption (1), and the paper leaves all three to "known arguments". The incomes $r_i(p)$ may be $+\infty$ for prices with negative coordinates, so finiteness at the equilibrium price is part of the conclusion, not an assumption.

Formalization scope

Consumers are Fin n, commodities Fin l; an allocation is a function Fin n → Fin l → ℝ, a price a vector Fin l → ℝ, and $p \cdot y = \sum_k p_k y_k$. A single definitions file (FuzzyGames.Walras.Basic) holds the economy, its assumptions, $Y(\tau)$, $X(\tau)$, the fuzzy core, incomes, budget sets, Walras equilibria and the sets $Q(i)$.

The formalization commits to the following readings, each recorded in the items' Formalization Notes:

• Complete preferences. The paper's "preference preordering" is read, as in Debreu's usage, as a reflexive, transitive and complete relation on $\mathbb{R}^l_+$. The relation is a predicate on $\mathbb{R}^l$, but every assumption and every use is restricted to $\mathbb{R}^l_+$.
• Continuity means closed upper and lower contour sets in $\mathbb{R}^l_+$; convexity means convex upper contour sets, plus the condition of (1)(i).
• Assumption (1)(i) is printed with $x \succcurlyeq y$ in the premise, which fails at $x = y$; it is stated with $x \succ y$.
• Blocking is strict and by nonzero coalitions. The fuzzy-core definition is printed with $x_\tau^i \succcurlyeq x^i$; the proof uses $\succ$, and the weak version would let every allocation block itself. The coalition $\tau = 0$ is excluded, since its condition over $A_\tau = \emptyset$ is vacuous.
• Dummy coordinates. An allocation of $\tau$ is a full family of $n$ bundles; those with $\tau_i = 0$ are multiplied by $0$, unconstrained and never compared.
• $Y(\tau)$ is Mathlib's pointwise Minkowski sum of scaled sets.
• Incomes take values in the extended reals (EReal), so that $r_i(p) = +\infty$ is represented and never replaced by a default value.

A trivializing formalization is ruled out: the assumptions are satisfiable, and a sorry-free check (one consumer, one commodity, $x \succcurlyeq y \iff x \ge y$, $Y(1) = (-\infty, 1]$) verifies them together with a Walras equilibrium, so neither side of the goal is empty by construction.

Contributions welcome: proofs of the milestones, a separation-to-prices lemma for comprehensive endowment sets, and general facts about complete continuous convex preferences on $\mathbb{R}^l_+$, which are reusable for any general equilibrium development.

Selected references

• J.-P. Aubin, Cooperative fuzzy games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• G. Debreu, H. Scarf, A limit theorem on the core of an economy, International Economic Review 4(3) (1963) 235–246. https://doi.org/10.2307/2525290
• R. J. Aumann, Markets with a continuum of traders, Econometrica 32 (1964) 39–50. https://doi.org/10.2307/1913732
• G. Debreu, Theory of Value, Cowles Foundation Monograph 17, Yale University Press, 1959.

Motivation

A prophet inequality compares two observers of a sequence of nonnegative random variables $X_1, \dots, X_n$. The prophet knows all values in advance and collects $X_n^* = \max(X_1, \dots, X_n)$. The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of $EX_n^*$, and the factor $2$ is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.

Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least $c$, is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor $2$: with $m$ a median of $X_n^*$, Theorem 1 of the paper gives $EX_n^* \le 2E^+X_{s(m)}$ or $EX_n^* \le 2E^+X_{t(m)}$. Mission I of this series formalizes that theorem.

Timeline (as recounted on p. 1213 of the paper).

• 1978: Krengel and Sucheston show $EX_n^* \le 2V_n(\underline X)$, where $V_n$ is the optimal stopping value, for independent $X_i \ge 0$; the constant $2$ cannot be improved for any $n \ge 2$.
• 1981: Hill and Kertz show that strict inequality holds in all but trivial cases.
• 1982: Hill and Kertz show that for i.i.d. $X_i$ the best constant $\alpha_n$ for optimal rules depends on $n$ and is bounded by $1.6$.
• 1983: Kertz (unpublished at the time) proves $\lim \alpha_n = 1 + a^* = 1.341\ldots$ for a constant $a^*$ given by an integral equation.
• 1984: Samuel-Cahn shows that a median threshold rule achieves the factor $2$ (Theorem 1), and that for threshold rules the factor $2$ cannot be lowered even for i.i.d. variables (Theorem 2). This mission is Theorem 2.

Setting

Fix $n \ge 1$ and a probability law $\mu$ on $[0, \infty)$. Let $X_1, \dots, X_n$ be independent with common law $\mu$, and $X_n^* = \max(X_1, \dots, X_n)$. For a constant $c \ge 0$ the threshold rules are

• $t(c)$: the smallest $i < n$ with $X_i \ge c$, and $t(c) = n$ otherwise;
• $s(c)$: the smallest $i < n$ with $X_i > c$, and $s(c) = n$ otherwise.

The stopped value is $X_{t(c)}$ or $X_{s(c)}$. The truncated expectations are $E^+X_{t(c)} = E[X_{t(c)} I(X_{t(c)} \ge c)]$ and $E^+X_{s(c)} = E[X_{s(c)} I(X_{s(c)} > c)]$: they discard the forced stop at time $n$ below the threshold. The class $T_n^*$ is the set of all $t(c)$ and $s(c)$ with $c \ge 0$.

The lower half of the theorem uses an explicit family. For $0 < a < 1$, $b > 0$, $c > 0$ and $n > b + c$, the variables $X_i^{(n)}$ take the values $0$, $a$, $1$ with probabilities $1 - (b+c)/n$, $c/n$, $b/n$. Two constants enter:

$$a^* = \frac{c(1 - e^{-b}) - b e^{-b}(1 - e^{-c})}{c(1 - e^{-b-c})}, \qquad Q(b, c) = 1 + \frac{e^{-b} - e^{-b-c}}{1 - e^{-b-c}} - \frac{b(e^{-b} - e^{-b-c})^2}{c(1 - e^{-b-c})(1 - e^{-b})}.$$

This $a^*$ is unrelated to the $a^*$ of the NOTE in §1 of the paper.

In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are $t(c)$ and $s(c)$; Emax, EstopT, EstopS, EplusT, EplusS are $EX_n^*$, $EX_{t(c)}$, $EX_{s(c)}$ and the $E^+$ terms; supE and supEplus are the two suprema over $T_n^*$; threePoint n a b c is the law of $X_i^{(n)}$; aStarIID and Q are the constants above.

Formalization targets

Goal: Theorem 2 (p. 1215)

$$\sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} E^+X_t}\right] = \sup_n \sup_{\underline X} \left[\frac{EX_n^*}{\sup_{t \in T_n^*} EX_t}\right] = 2,$$

over i.i.d. nonnegative $\underline X$. It is stated as three facts: $EX_n^* \le 2 \sup_{T_n^*} E^+X_t$ for every $n$ and law; $\sup_{T_n^*} E^+X_t \le \sup_{T_n^*} EX_t$; and for every $\varepsilon > 0$ some $n$ and law with $(2 - \varepsilon)\sup_{T_n^*} EX_t < EX_n^*$.

Milestones (proof of Theorem 2, p. 1215)

1. The upper bound $EX_n^* \le 2\sup_{T_n^*} E^+X_t$, attributed to Theorem 1.
2. $\lim_n EX_n^{(n)*} = 1 - e^{-b} + a\{e^{-b} - e^{-b-c}\}$.
3. For the three-point law, $\sup_{T_n^*} EX_t = \max\{EX_{t(a)}, EX_{t(1)}\}$.
4. $W(a) = \lim_n EX^{(n)}_{t(a)} = (1 - e^{-b-c})(b + ac)/(b + c)$.
5. $W(1) = \lim_n EX^{(n)}_{t(1)} = 1 - e^{-b}$.
6. $W(a^*) = W(1)$ and $0 < a^* < 1$.
7. With $a = a^*$, $\lim_n EX_n^{(n)*}/\sup_{T_n^*} EX_t^{(n)} = Q(b, c)$.
8. $Q(b, c) \to 2$ as $b \to 0^+$ and $c \to \infty$.

Significance

Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most $1.6$ (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class $T_n^*$ to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.

Difficulty

The limits are "easily seen" on the page, but each requires controlling $(1 - x/n)^{n-1}$ uniformly with the exact law of a stopped index on a product space, including the forced stop at $n$ whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every $t(c)$ and $s(c)$ with $c \ge 0$ must be shown to coincide almost surely with one of $t(0)$, $t(a)$, $t(1)$ or stopping at $n$, and the first and last must be shown dominated by $t(a)$ for every finite $n > b + c$, not only asymptotically. The final step is a joint limit in $(b, c)$, in which $b/(1 - e^{-b}) \to 1$ while the correction term vanishes like $1/c$; an iterated limit is not the statement.

Formalization scope

The i.i.d. variables are the coordinates of $\mathbb R^n$ under the product measure $\mu^{\otimes n}$; all quantities depend only on the joint law, so the supremum over $\underline X$ is a supremum over laws $\mu$ with $\mu((-\infty, 0)) = 0$. Indices are 0-based in Fin n with [NeZero n], the paper's index $n$ being ⊤. Expectations are lintegrals of ENNReal.ofReal in $[0, \infty]$: no integrability is assumed and $EX_n^* = \infty$ is allowed. The sup over $T_n^*$ ranges over $c \ge 0$ and over both families $t(c)$ and $s(c)$. Limits along the triangular array are indexed by $n = k + 1$ and taken in $\mathbb R$ after toReal; the early terms with $n \le b + c$, where the clipped weights of threePoint do not form a probability measure, do not affect any limit.

The page's ratios are not written literally: in $[0, \infty]$ the quotients $0/0$ and $\infty/\infty$ take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on $[0, \infty)$, which rules out the Dirac mass at $0$ and sub-probability witnesses.

A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit $(1 - x/n)^n \to e^{-x}$ along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.

Selected references

• E. Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Ann. Probab. 12(4) (1984) 1213–1216. https://doi.org/10.1214/aop/1176993150
• U. Krengel and L. Sucheston, On semiamarts, amarts, and processes with finite value, in Probability on Banach Spaces, Adv. Probab. Related Topics 4, Dekker, New York (1978) 197–266.
• T. P. Hill and R. P. Kertz, Ratio comparisons of supremum and stop rule expectations, Z. Wahrsch. verw. Gebiete 56 (1981) 283–285. https://doi.org/10.1007/BF00536175
• T. P. Hill and R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Ann. Probab. 10(2) (1982) 336–345. https://doi.org/10.1214/aop/1176993861

Motivation

Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.

Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).

Setting

There are $m$ major players $M = \{1, \dots, m\}$ with weights $w_1, \dots, w_m \ge 0$, and $w(S) = \sum_{j \in S} w_j$. The ocean is the interval $I = [0,1]$ with Lebesgue measure, carrying total weight $\alpha > 0$. In the oceanic game $[c; w_1, \dots, w_m; \alpha]$ with quota $c$, a coalition wins when the weight of its major players plus $\alpha$ times its share of the ocean is at least $c$.

The random order is modelled by a uniform random point $x = (x_1, \dots, x_m)$ of the cube $I^m$: major player $j$ is inserted into the ocean at position $x_j$, and $P(t) = \{ j : x_j < t \}$ is the set of major players placed before position $t$. Player $i$ is pivotal when

$$w(P(x_i)) + \alpha x_i \le c \le w(P(x_i)) + w_i + \alpha x_i, \qquad (2.4)$$

and the value $\varphi_i$ of player $i$ is the probability of (2.4), i.e. the volume of the set $A_i \subseteq I^m$ where it holds. The combined value of the ocean is $\Phi = 1 - \sum_{i} \varphi_i$ (2.5).

With the quota $y$ as a variable, $\Gamma(y) = [y; w_1, \dots, w_m; \alpha]$ has values $\varphi_i(y)$, $\Phi(y)$, and the pivot location $F(y) = \inf\{t \ge 0 : w(P(t)) + \alpha t \ge y\}$ is a random, nondecreasing, piecewise linear function of $y$ with expectation $E\{F(y)\}$. Adding a major player $m+1$ of weight $w_{m+1}$ gives the game $\Gamma^+$.

The game is interior when

$$w(M) \le c \le \alpha,$$

that is, the ocean alone wins and the major players together lose. With $\bar w_j = \alpha - w_j$, define $\pi(S) = \prod_{j \in S} \tfrac{w_j}{\alpha} \prod_{j \in M - S} \tfrac{\bar w_j}{\alpha}$ for $S \subseteq M$, the analogous product $\pi_i(S)$ over $M - \{i\}$ for $S \subseteq M - \{i\}$, and the integers $a_0 = 1$, $a_n = 1 - n a_{n-1}$, i.e. $1, 0, 1, -2, 9, -44, \dots$

Formalization targets

Goal: Theorem 6 (p. 20)

In an interior game, with $s = |S|$,

$$\varphi_i = \frac{w_i}{\alpha} \sum_{S \subseteq M - \{i\}} a_s \, \pi_i(S), \qquad \Phi = \sum_{S \subseteq M} a_s \, \pi(S).$$

Both identities are part of the goal. The values do not depend on $c$ within the interior range.

Milestones

1. §2, p. 5: the pivot sets $A_1, \dots, A_m$ overlap only in measure zero.
2. (4.3): $\varphi_i(y) = \operatorname{Prob}\{F(y) = x_i\}$ for $0 \le y \le w(M) + \alpha$.
3. (4.4)–(4.5): for $0 < y < w(M) + \alpha$, $F$ is differentiable at $y$ almost surely, $\sum_i \varphi_i(y) = \operatorname{Prob}\{F'(y) = 0\}$ and $\Phi(y) = \operatorname{Prob}\{F'(y) = 1/\alpha\}$.
4. Theorem 2, (4.7): $\Phi(y) = \alpha \, \frac{d}{dy} E\{F(y)\}$.
5. Lemma, (4.12)–(4.13): $\varphi^+_{m+1}(z) = \frac{1}{\alpha} \int_{t_1}^{t_2} \Phi(y)\, dy$ with $t_1 = \max(z - w_{m+1}, 0)$, $t_2 = \min(z, w(M) + \alpha)$.
6. Theorem 5, (5.4): if $[c; w_1, \dots, w_m; \alpha]$ and $[d; w_1, \dots, w_{m+1}; \alpha]$ are both interior, $\varphi^+_{m+1} = \frac{1}{\alpha} \Phi w_{m+1}$.
7. Proof of Theorem 6, p. 21: the right-hand sides above add up to 1, an identity valid for all real $w_j$ and $\alpha \ne 0$.

Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ($|a_n|$ is the nearest integer to $n!/e$ and counts derangements).

Significance

Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios $w_j/\alpha$. Table 1 of the memorandum lists the cases $m \le 3$, and the theorem gives every $m$. Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.

The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.

Difficulty

The values are volumes of regions of $I^m$ cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into $m!$ order cells, with the quota $c$ entering each. The paper's route avoids this by passing through the random function $F$, Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in $y$, with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of $[0, w(M) + \alpha]$. Theorem 6 is then an induction on $m$ that uses Theorem 5 for every player in turn, so it also needs the invariance of $\varphi_i$ under a relabelling of the major players.

Formalization scope

• Major players are Fin m ($m = 0$ is allowed; then $\Phi = 1$). The probability of an event is the Lebesgue volume of its intersection with $[0,1]^m$; no probability space is built.
• $P(t)$ uses the strict inequality $x_j < t$, as printed.
• $\varphi_i$ is defined as the volume of the pivot set (2.4), for every real quota. $\Phi$ is defined by (2.5), as the paper allows ("We might equally well take (2.5) as the definition of $\Phi$"). Neither is defined through the formulas of Theorem 6 or through $F$; defining them that way would make the goal an unfolding, and is ruled out.
• The paper writes (4.2) as a minimum $F(y) = \min\{x \mid w(P(x)) + \alpha x \ge y\}$, which need not be attained; $F$ is the infimum over $t \ge 0$, the value shown in its Fig. 3.
• The standing assumptions $w_j \ge 0$ and $\alpha > 0$ (§2) are explicit hypotheses. The p. 5 footnote's $0 \le c \le w(M)+\alpha$ applies to the pivot-set milestone. Other quota ranges are explicit: $0 \le y \le w(M) + \alpha$ for (4.3) and Theorem 2 (one-sided derivatives at the ends), the open interval for (4.4)–(4.5) (two-sided derivatives, stated with HasDerivAt), and $0 \le z \le w(M) + w_{m+1} + \alpha$ for the Lemma, as on p. 14.
• The added player is appended with Fin.snoc as index Fin.last m.
• Corollary (5.5) assumes $w_i > 0$, since it divides by $w_i$. Theorem 4, stated in the paper "in the general oceanic game", is false at quota $0$ and when the limit game has no winning coalition; it is stated for $0 < c \le w(M - \{i\}) + \alpha$.
• The identity of milestone 7 is pure algebra and is stated for all real weights and $\alpha \ne 0$.

A complete development needs: measurability of the pivot sets and of $F$ in $x$, the structure of $F$ as a piecewise linear function of $y$, differentiation of $E\{F\}$, and invariance of the values under permutations of the major players. The pivot-set and $F$ infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.

Selected references

• J. W. Milnor and L. S. Shapley, Values of Large Games, II: Oceanic Games, The RAND Corporation, Research Memorandum RM-2649, February 1961. https://www.rand.org/pubs/research_memoranda/RM2649.html
• J. W. Milnor and L. S. Shapley, Values of Large Games II: Oceanic Games, Mathematics of Operations Research 3(4):290–307, 1978. https://doi.org/10.1287/moor.3.4.290
• L. S. Shapley, A Value for n-Person Games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, 307–317. https://doi.org/10.1515/9781400881970-018
• L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, The RAND Corporation, Research Memorandum RM-2648, November 1960.
• R. J. Aumann and L. S. Shapley, Values of Non-Atomic Games, Princeton University Press, 1974. https://doi.org/10.1515/9781400867080

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