Mechanism Design

Motivation

When a bank or firm in a network of mutual obligations cannot meet its liabilities, some rule must decide how much each debtor pays each creditor. The rule used almost universally in the systemic-risk literature is the proportional rule of Eisenberg and Noe (2001): every agent pays its liabilities in full if it can, and otherwise distributes its whole asset value over its creditors in proportion to their claims. Central banks and regulators use it to measure contagion in interbank markets; Elsinger, Lehar and Summer (2006) apply it to the 881 banks reporting to the Austrian Central Bank, and Upper (2011) surveys fifteen such studies.

The rule is usually taken as given. Csóka and Herings (2021) ask which properties of a bankruptcy rule single it out, without assuming in advance that payments depend only on an agent's asset value and liabilities. Their answer is an axiomatization: five basic axioms together with one axiom on splitting an agent into identical copies.

For claims problems (one estate, several claimants) the proportional rule has classical characterizations through nonmanipulability by merging and splitting claims (O'Neill 1982, de Frutos 1999, Moreno-Ternero 2006, Ju, Miyagawa and Sakai 2007). Csóka and Herings show that the network analogue of nonmanipulability is too strong (no rule satisfies it together with the basic axioms) and replace it by invariance to mitosis.

Setting

Agents are natural numbers. A financial network $F = (N, z, L)$ consists of a nonempty finite set $N \subseteq \mathbb N$ of agents, endowments $z_i > 0$ for $i \in N$, and a nonnegative liability matrix $L$ on $N \times N$ with $L_{ii} = 0$; $L_{ij}$ is what $i$ owes $j$. The class of all financial networks is $\mathfrak F$. The relative liability matrix is $\Pi_{ij} = 0$ if $L_{ij} = 0$ and $\Pi_{ij} = L_{ij}/\sum_{k \in N} L_{ik}$ otherwise.

A payment matrix is an element of $\mathcal M(N)$, the nonnegative $N \times N$ matrices with zero diagonal; $P_{ij}$ is the amount $i$ pays $j$. Agent $i$'s asset value is $a_i(N,z,P) = z_i + \sum_{j \in N} P_{ji}$ and its equity is $e_i(N,z,P) = a_i(N,z,P) - \sum_{j \in N} P_{ij}$. For rows, $P_i < L_i$ means $P_{ij} \le L_{ij}$ for all $j$ with strict inequality for some $j$.

A bankruptcy rule $b$ assigns to each $F \in \mathfrak F$ a payment matrix $b(F) \in \mathcal M(N)$ (Definition 2.1). The proportional rule $p$ assigns the solution of

$$P_{ij} = \min\Big\{\Pi_{ij}\Big(z_i + \sum_{k \in N} P_{ki}\Big),\ L_{ij}\Big\}, \qquad i, j \in N. \tag{2.1}$$

The axioms, in the order of the paper:

• claims boundedness: $b(F) \le L$;
• limited liability: $e_i(N,z,b(F)) \ge 0$;
• priority of creditors: $b_i(F) < L_i$ implies $e_i(N,z,b(F)) = 0$;
• continuity: $b(F^n) \to b(F)$ whenever $F^n \to F$, where convergence means that the populations eventually coincide and endowments and liabilities converge;
• impartiality: $L_{ij} = L_{ik}$ implies $b_{ij}(F) = b_{ik}(F)$;
• invariance to mitosis: if agent $j$ is split into $|K|+1$ identical agents $\{j\} \cup K$, each receiving the fraction $1/(|K|+1)$ of $j$'s endowment, liabilities and claims and none toward each other, then the total payments of the copies to, and from, each other agent equal $j$'s original payments, and payments among the other agents do not change.

Formalization targets

Goal: Theorem 4.2

$$\text{(a)}\quad \forall F \in \mathfrak F,\ \exists!\, P \text{ solving (2.1) for } F,$$ $$\text{(b)}\quad b \text{ satisfies the six axioms} \iff \forall F,\ b(F) \text{ solves (2.1) for } F .$$

Part (a) makes $p$ a well-defined bankruptcy rule; part (b) says that $p$ satisfies the axioms and that every rule satisfying them is $p$.

Milestones

1. Uniqueness and existence of the solution of (2.1) (Eisenberg–Noe, Theorem 2, cited on p. 2801).
2. Every solution of (2.1) gives nonnegative equities, and zero equity to any agent not paying in full (Part (I), p. 2808).
3. A limit of solutions of (2.1) along converging networks solves (2.1) for the limit network (Part (I), p. 2808).
4. The split payment matrix (A.1) solves (2.1) for the split network (Part (I), pp. 2808–2809).
5. Part (I): the proportional rule satisfies the six axioms.
6. Lemma A.1: under impartiality and invariance to mitosis, $L_{ij} = (q/r) L_{ik}$ implies $b_{ij}(F) = (q/r) b_{ik}(F)$.
7. Part II for rational liabilities, without continuity; then Part II in general.

Significance

The theorem justifies the proportional rule by properties rather than by convention. Because the axioms make no assumption on the form of the rule, consequences such as the absence of pairwise netting are derived, not assumed. Together with the paper's Theorem 5.3 (no rule satisfies the basic axioms and full nonmanipulability), it shows that invariance to mitosis is the strongest splitting requirement compatible with the basic axioms.

The result is proved on paper; no part of it, and no part of the Eisenberg–Noe clearing theory, has a machine-checked proof on this platform. A formalization contributes a reusable layer for clearing payments in financial networks: the system (2.1), its existence and uniqueness under strictly positive endowments, nonnegativity and zero-equity properties of clearing vectors, and their continuity in the data. These are the objects every stress-testing model on top of Eisenberg–Noe starts from.

Difficulty

Existence and uniqueness of a solution of (2.1) is a fixed-point statement about a nonlinear, non-contracting map; uniqueness holds only because every endowment is strictly positive, and fails without it (two agents owing each other one unit with no endowments admit both $P = 0$ and $P = L$).

In the characterization direction, impartiality only equalizes payments to equal claims, and invariance to mitosis only relates networks that differ by splitting one agent into identical copies. Neither axiom speaks directly about payments to unequal claims, and splitting reaches only ratios of positive integers. Passing from rational to real liabilities needs continuity of the rule and continuity of $p$, and the latter rests on uniqueness of the clearing vector, so the two halves of the theorem are not independent.

Formalization scope

• Model. Agents are natural numbers and populations are nonempty Finset ℕ; a fixed finite type cannot express mitosis, which creates fresh agents. Endowments, liabilities and payment matrices are functions on $\mathbb N$ (resp. $\mathbb N \times \mathbb N$) that vanish outside the population, as part of the network structure and of $\mathcal M(N)$. All quantities are real.
• Conventions. $\Pi$ is written with the page's case split. Continuity is sequential, exactly in the paper's convergence criterion (eventual equality of populations, coordinatewise convergence of endowments, liabilities and payments); the paper's topology is first countable, so this is continuity. The split network of Axiom 4.1 is a predicate fixing every coordinate of the new network; $K$ is a finite set of fresh agents and may be empty. The divisor $|K|+1$ is real.
• Added hypothesis. In Lemma A.1, $q$ and $r$ are required to be positive integers; the page writes $q, r \in \mathbb N$ and its proof splits agents into $q$ and $r$ copies.
• Goal shape. "$b = p$" is expressed as "$b(F)$ solves (2.1) for every $F$", and the goal also asserts that (2.1) has a unique solution. Without part (a) the iff would be compatible with an empty class of rules satisfying (2.1); a formalization that drops it, or that defines $p$ by choice from an unproved existence claim, is not the theorem.
• Out of scope. Nonmanipulability (Axiom 5.1, Theorem 5.3), the independence examples of Section 6 and Appendix B, and the linear-programming characterization (2.2).
• Welcome contributions. A general Knaster–Tarski proof of existence for (2.1) via Mathlib's OrderHom.lfp, the uniqueness argument under positive endowments, and lemmas on the split network (sums over the copies, the relative liabilities of copies) that serve both Part (I) and Lemma A.1.

Selected references

• P. Csóka, P. J.-J. Herings, An Axiomatization of the Proportional Rule in Financial Networks, Management Science 67(5):2799–2812, 2021. https://doi.org/10.1287/mnsc.2020.3700
• L. Eisenberg, T. H. Noe, Systemic Risk in Financial Systems, Management Science 47(2):236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• H. Elsinger, A. Lehar, M. Summer, Risk Assessment for Banking Systems, Management Science 52(9):1301–1314, 2006. https://doi.org/10.1287/mnsc.1060.0531
• C. Upper, Simulation Methods to Assess the Danger of Contagion in Interbank Markets, Journal of Financial Stability 7(3):111–125, 2011. https://doi.org/10.1016/j.jfs.2010.12.001
• B. O'Neill, A Problem of Rights Arbitration from the Talmud, Mathematical Social Sciences 2(4):345–371, 1982. https://doi.org/10.1016/0165-4896(82)90029-4
• B. Moreno-Ternero, Proportionality and Non-Manipulability in Bankruptcy Problems, International Game Theory Review 8(1):127–139, 2006. https://doi.org/10.1142/S0219198906000825

Why intermediation changes an auction

An online display impression often reaches an advertiser through a chain of ad exchanges and networks instead of through a direct sale. Each intermediary runs its own auction among its downstream bidders and decides what to report to the auction above it. Its profit depends on whether it wins upstream and on what it can charge downstream. Even when every local auction is a second-price auction, the sale becomes a sequential game in which agents choose mechanisms. Balseiro, Candogan and Gurkan study this game on a symmetric tree. They characterize a subgame perfect equilibrium in which every intermediary applies a projected virtual value to its highest downstream report (SSRN 2661459; journal version in Manufacturing & Service Operations Management, 2020, doi:10.1287/msom.2019.0854). The single-auctioneer case is Myerson's optimal auction (Myerson 1981). In it, a seller facing i.i.d. bidders with increasing virtual values sets the reserve at the zero of the virtual value.

Network, mechanisms and virtual values

The seller occupies tier $n+1$ of a symmetric $\mathbf k$-tree, intermediaries occupy tiers $n,\dots,1$, and buyers are the leaves at tier $0$. Every tier-$t$ node has $k_t\ge1$ downstream agents. Buyers' values are i.i.d. draws from a law $V$ on $[0,\infty)$ with lower support end $0$, a continuous strictly positive density on its support, and a finite mean. Buyers report their values.

An intermediary's mechanism $(r,Y)\in\mathcal M$ is a reserve $r\ge0$ and a nondecreasing reporting function $Y:\mathbb R_+\to\mathbb R_+$. If its highest downstream report $w$ satisfies $w\ge r$, it reports $Y(w)$ upstream. If it wins upstream, it allocates to that downstream agent. The seller runs a second-price auction with a reserve $r_S\ge0$. A winning agent pays the minimum report that would still have won (Definition A.1). An intermediary's profit is what its winning child pays minus what it pays upstream.

For a law $X$ with cdf $G_X$ and density $g_X$, the virtual value is $\phi_X(x)=x-(1-G_X(x))/g_X(x)$ and its inverse is $\phi_X^{-1}(w)=\inf\{x\in\mathcal X:\phi_X(x)\ge w\}$. The projection point is $z_X=\phi_X^{-1}(0)$. The projected virtual value $\psi_X$ equals $0$ below $z_X$, equals $\phi_X$ from $z_X$ up to $\sup\mathcal X$, and equals $\sup\mathcal X$ beyond. If $X$ has an atom at $0$, these objects use the positive part $X\mid X>0$ (Definitions 3.1–3.2).

The anticipated reports are laws defined by recursion: $W_0=V$ and $W_t=\psi_{W_{t-1}}\big(W_{t-1}^{\mathrm{FH}(k_t)}\big)$, the projected virtual value of the maximum of $k_t$ i.i.d. copies of $W_{t-1}$ (Definition 3.3). Assumption 3.1 asks that, for $t=1,\dots,n$, $W_t$ has finite mean and its positive part has a continuous positive density and a strictly increasing virtual value.

Formalization targets

Goal: Theorem 3.1

$$Y_t^*(w)=\psi_{W_{t-1}}(w),\quad r_t^*=z_{W_{t-1}}\ \ (t=1,\dots,n),\qquad r_{n+1}^*=z_{W_n}$$

form a subgame perfect equilibrium. Fix any tier $t$ and any history: arbitrary mechanisms in $\mathcal M$ for tiers $t+1,\dots,n$ and any seller reserve. Then no tier-$t$ node gains by switching to any mechanism in $\mathcal M$. The seller gains nothing from any reserve $r_S\ge0$ instead of $z_{W_n}$.

Milestones, in attack order

1. Lemma G.1: $\phi_V\to\sup\mathcal V$; $z_V$ is finite and positive with $\phi_V(z_V)=0$; $\psi_V$ is continuous.
2. Optimal reserve with a cost (proof of Lemma 3.1): with $m$ i.i.d. bidders and seller cost $c\le\sup\mathcal V$, the reserve $\phi_V^{-1}(c)$ maximizes $\mathbb E[(\max(\delta,V^{\mathrm{SH}(m)})-c)\mathbf 1\{V^{\mathrm{FH}(m)}\ge\delta\}]$.
3. Lemma 3.1: an intermediary facing a second-price auction with reserve $r_S\le\sup\mathcal V$ and a random competing bid has $(z_V,\psi_V)$ as an optimal mechanism in $\mathcal M$.
4. Lemma B.1: the same when $V$ has an atom at zero.
5. Lemma 2.1(A): every agent other than the seller faces an upstream threshold that acts as a second-price auction in allocation and payment.
6. Anticipated reports: under the equilibrium mechanisms the tier-$t$ report has law $W_t$, and siblings' reports are independent.
7. Seller's optimal reserve (proof of Theorem 3.1): $z_{W_n}$ maximizes $\mathbb E[\max(r,W_n^{\mathrm{SH}})\mathbf 1\{W_n^{\mathrm{FH}}\ge r\}]$.

What the result gives

The theorem identifies optimal mechanisms at every tier from the distribution of the reports directly below that tier alone. It also gives the seller's reserve after the network has transformed the buyers' values. Every later result of the paper is stated at this equilibrium. Examples are the profit ratios along chains with generalized Pareto values, the effect of market size, and the comparison of network shapes. Without the characterization each of these would need its own strategic analysis.

The paper proves the result on paper; none of these statements has a machine-checked proof yet. Formalizing it means building a finite tree auction with threshold payments and laws of maximum reports. It also needs virtual values for laws on unbounded supports and with an atom at zero, and Myerson-type reserve optimality for such laws. The last two are standard tools of auction theory that are absent from Mathlib in this generality.

Where the difficulty lies

In a single second-price auction, truthful bidding is dominant and the reserve is the only choice. An intermediary is different. Its report changes its chance of winning upstream, while its reserve and reporting function change what it can charge downstream. So the local second-price argument does not settle its choice. In a tree, a deviation must also be evaluated after arbitrary upstream histories, including reporting functions that are flat on intervals or jump. There, ties and payment thresholds matter. The paper's closed payment formula (2) can disagree with the minimum report that actually wins under a fixed tie rule. With that formula, a deviation with a jump beats $\psi$, so the theorem would be false. The anticipated reports $W_t$ also carry an atom at zero from tier $1$ on, so the one-stage lemma is needed in its atom version.

Formalization scope

Laws are probability measures on $\mathbb R$; $W_t$ is the pushforward of a product measure under $\psi_{W_{t-1}}\circ\max$. The density is the derivative of the cdf, read only at $x>0$, where it also gives the virtual value of the positive part. The support of a positive part is the interval $\{x>0:G(x)<1\}$, and "$x\ge\sup\mathcal X$" means $G(x)=1$. The general objects (virtual value, projection, regularity, reserve objectives) are a separate definition module, reusable beyond this mission.

The tree has $\prod_{s=1}^{n+1}k_s$ buyers with a product law. A report below the reserve is no report, which is never allocated. Ties go to the lowest index, and a report equal to a reserve wins. Payments are minimum winning reports. Buyers report truthfully (Lemma 2.1(B)). The seller's reserves range over $\mathbb R_+$, and in Lemma 3.1 the competing bid is independent of the buyers. Strict increase of $\phi_V$ is an explicit hypothesis: Assumption 3.1 starts at tier $1$, but $\psi_V$ and Lemma 3.1 need it at tier $0$.

Expected profits are single integrals of realized profits. The equilibrium profit is nonnegative pointwise, so a non-integrable deviation never violates the inequality. Deviations range over all of $\mathcal M$, and histories over all upstream mechanisms and reserves, so the equilibrium cannot hold for want of competitors. With rate-one exponential values and one intermediary with one buyer, the intermediary earns $e^{-2}>0$. Proofs of any milestone, and the measure-theoretic groundwork (measurability of $\psi$, laws of maxima, Myerson's reserve on unbounded supports), are welcome.

Selected references

• S. R. Balseiro, O. Candogan and H. Gurkan, Multi-stage Intermediation in Display Advertising, SSRN manuscript 2661459, 2019. https://ssrn.com/abstract=2661459
• S. R. Balseiro, O. Candogan and H. Gurkan, Multistage Intermediation in Display Advertising, Manufacturing & Service Operations Management, 2020. https://doi.org/10.1287/msom.2019.0854
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• V. Krishna, Auction Theory, 2nd ed., Academic Press, 2009, ISBN 978-0-12-374507-1.

Motivation

The Hospital Readmissions Reduction Program (HRRP), created by the US Affordable Care Act and run by the Centers for Medicare & Medicaid Services since 2012, cuts the Medicare payments of hospitals whose 30-day readmission rates exceed a benchmark computed from other hospitals. It is a form of yardstick competition in the sense of Shleifer (1985): a regulator that cannot observe a provider's costs pays it according to what comparable providers achieve. The penalty differs from Shleifer's scheme in three ways: it is scaled by a multiplier that grows as the benchmark readmission rate falls, it is capped, and no bonus is paid for beating the benchmark.

Arifoğlu, Ren and Tezcan (2021) build a game-theoretic model to separate the effect of each feature. Their Proposition 1 isolates the multiplier: with the cap and the no-bonus rule removed (the scheme they call HRRP-I), hospitals still choose readmission rates below the social optimum and treatment costs above it. Medical and policy researchers had argued informally that the multiplier distorts incentives; Proposition 1 is the paper's precise version of that argument.

Setting

There are $N\ge 2$ identical hospitals. Patients arrive at each hospital at rate $\lambda>0$. Hospital $i$ chooses a readmission rate $r_i$ and a marginal treatment cost $c_i$ in the action box

$$B=[r_{\min},r_{\max}]\times[c_{\min},c_{\max}],\qquad 0<r_{\min}\le r_{\max}<1,\quad 0\le c_{\min}<c_{\max},$$

and pays an investment cost $R(r_i,c_i)$ to reach them. Each admitted patient is readmitted with probability $r_i$, so the hospital treats $(1+r_i)\lambda$ patients per unit time at cost $c_i$ each.

Standing assumptions on $R$ (p. 10 of the paper): $R$ is twice differentiable, decreasing in each variable, and jointly convex; on $B$,

$$R_{rr}R_{cc}>(R_{rc}+\lambda)^2,\qquad R_{cr}\ge 0,$$

where subscripts denote partial derivatives.

The regulator's objective is the social welfare

$$S(r,c)=V(\lambda)-c(1+r)\lambda-R(r,c),$$

where $V(\lambda)$ is a fixed total patient utility. A maximizer $(r^*,c^*)$ of $S$ over $B$ is the first best (Lemma 1 of the paper: it exists, is unique and is interior).

The regulator observes every hospital's cost, readmission rate and investment, and computes the yardsticks

$$\bar c_i=\frac{1}{N-1}\sum_{k\ne i}c_k,\qquad \bar r_i=\frac{1}{N-1}\sum_{k\ne i}r_k,\qquad \bar R_i=\frac{1}{N-1}\sum_{k\ne i}R(r_k,c_k).$$

Under HRRP-I hospital $i$ receives

$$T_i=\bar c_i\lambda(1+r_i)-\frac{1}{\bar r_i}(r_i-\bar r_i)(1+r_i)\bar c_i\lambda+\bar R_i$$

and earns the profit $\Pi_i=T_i-c_i(1+r_i)\lambda-R(r_i,c_i)$. The factor $(1+r_i)/\bar r_i$ multiplying the excess readmission rate $r_i-\bar r_i$ is the multiplier. An equilibrium is a pure-strategy Nash equilibrium: a profile of actions in $B$ from which no hospital can raise its profit by changing its own action within $B$. A symmetric equilibrium $(\tilde r,\tilde c)$ is an equilibrium in which every hospital plays the same action.

Formalization targets

Goal: Proposition 1 (p. 14)

For every $N\ge2$:

$$\exists\,(\tilde r,\tilde c)\ \text{symmetric equilibrium};\qquad \text{every symmetric equilibrium satisfies}\ \ \tilde r<r^*,\ \ \tilde c>c^*;$$

and for $N=2$ every equilibrium is symmetric.

Milestones

1. Lemma 1 (p. 11): $S$ has a unique maximizer $(r^*,c^*)$ over $B$; it is interior and satisfies the first-order conditions $\lambda c^*+R_r(r^*,c^*)=0$ and $\lambda(1+r^*)+R_c(r^*,c^*)=0$.
2. Proposition 1, existence: a symmetric equilibrium exists.
3. Proposition 1, ordering: every symmetric equilibrium has $\tilde r<r^*$ and $\tilde c>c^*$.
4. Proposition 1, two hospitals: with $N=2$ there is no asymmetric equilibrium.

The goal is the conjunction of milestones 2–4; Lemma 1 supplies the comparison point.

Significance

Proposition 1 is the paper's first main result and the base for its later analysis: the capped scheme HRRP-II and the actual HRRP (Propositions 2 and 3) are studied relative to the HRRP-I symmetric equilibrium, and the remedy the paper proposes (m-HRRP, Proposition 4) removes the multiplier precisely because Proposition 1 identifies it as a source of distortion. The ordering $\tilde r<r^*$ says that hospitals over-invest in readmission reduction; $\tilde c>c^*$ says that, as a consequence, they under-invest in reducing treatment costs.

The paper's proofs are in its online appendix, which is not part of the source this mission cites (the authors' accepted manuscript, LBS Research Online eprint 1402). No machine-checked proof of any statement of the paper is known. The mission produces a checked version of the model and of all three claims of Proposition 1; the two-hospital claim in particular has no published argument in the cited source.

Difficulty

Lemma 1 is the routine part. The ordering claim is harder: a symmetric equilibrium need not be interior (in simple examples $\tilde r=r_{\min}$), so the first-order conditions of the hospital's problem hold only as variational inequalities on $B$, and the comparison with $(r^*,c^*)$ must work from those inequalities and the curvature hypotheses alone. The existence claim needs a fixed-point theorem for the best-response map of a hospital facing yardsticks $(\bar r,\bar c)$, and therefore continuity of the best response, which rests on strict concavity of the hospital's profit; Brouwer's theorem is not in Mathlib. The two-hospital claim is a uniqueness-type statement about a two-player game with non-separable payoffs; the obvious route through contraction of the best-response map does not follow from the stated assumptions without further estimates.

Formalization scope

The Lean development lives in the namespace ReadmissionsHRRP.HRRPI. A Model carries lam ($\lambda$, a Lean keyword), V, the box bounds and the curried cost R r c. Partial derivatives are deriv of the sections of R. Profiles are maps Fin N → ℝ × ℝ (first coordinate $r_i$, second $c_i$); the averages divide by the real number $N-1$. The equilibrium notion is the published pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every hospital's feasible set equal to $B$; deviations keep the other hospitals' actions, so the yardsticks of the deviating hospital do not move.

The standing assumptions are one predicate, Model.Standing: the inequalities on the box bounds, $\lambda>0$ (implicit in the paper), $R$ of class $C^2$ on an open set containing $B$, non-increasing in each variable on $B$, jointly convex on $B$, and the two pointwise curvature conditions on $B$. The paper's Appendix A, which imposes boundary conditions "to ensure that optimal actions are interior", is not in the cited manuscript; it is replaced by the separate hypothesis Model.FirstBestInterior, that every maximizer of $S$ over $B$ is interior. Every theorem assumes $N\ge2$.

The first best is a maximizer of $S$ over $B$, never a solution of the first-order conditions; the ordering claim quantifies over every such maximizer, and the existence claim is part of the goal so that the ordering claim is not vacuous. A sorry-free sanity file checks that the hypotheses are jointly satisfiable for $\lambda=1$, $B=[1/10,1/2]\times[0,2]$, $R(r,c)=(1-r)^2+(2-c)^2$.

Useful infrastructure: strict concavity on a box from a Hessian condition, variational inequalities at constrained maxima, continuity of argmax maps, and Brouwer's theorem on a planar box (proved on the platform as AGT.brouwer_fixed_point). Contributions to any of these, or to the hand proofs of the separate claims, are welcome.

Selected references

• K. Arifoğlu, H. Ren, T. Tezcan, Hospital Readmissions Reduction Program does not provide the right incentives: Issues and remedies, Management Science 67(4), 2021; author-accepted manuscript, LBS Research Online eprint 1402. https://doi.org/10.1287/mnsc.2020.3649, https://lbsresearch.london.edu/id/eprint/1402/
• A. Shleifer, A theory of yardstick competition, RAND Journal of Economics 16(3), 1985. https://doi.org/10.2307/2555767
• D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991. https://mitpress.mit.edu/9780262061414/game-theory/

Motivation

Many allocation problems divide an object whose value to the participants is uncertain at the time the division rule is designed: computing time on a shared cluster, a recurring chore, the cost of a service used jointly. If the rule must be fixed before the realizations are known, and must treat everyone fairly in expectation, the designer faces a tradeoff between ex ante fairness and ex post efficiency. Bogomolnaia, Moulin and Sandomirskiy (arXiv:1903.10361, published in Management Science, 2022) study this tradeoff for a single divisible object, in the setting of online and repeated fair division (Moulin 2019).

The paper characterizes the most efficient fair rules that need almost no knowledge of the underlying distribution. For a good the efficient fair rules form a one-parameter family; for a bad (a chore, a cost) there is a single most efficient fair rule, the Bottom-Heavy rule. This mission formalizes the bads result, Theorem 17 of the paper.

Setting

There are $n\ge2$ agents $N=\{1,\dots,n\}$ and one divisible bad. A profile $x\in\mathbb R^N_+$ lists the agents' disutilities for the whole bad; zero disutilities are allowed. Write $x_N=\sum_i x_i$, $\bar x=x_N/n$ and $e^N=(1,\dots,1)$. The disutility profile is random, with distribution $\mu$ on $\mathbb R^N_+$; the coordinates may be correlated. A problem is normalized if $\mathbb E_\mu X_i=1$ for every $i$.

A division rule maps each realized profile $x$ to a lottery $\varphi(x)\in\Delta(N)$; agent $i$ bears the fraction $\varphi_i(x)$ of the bad. A rule is almost prior-independent (API) if it is a single measurable map, used for every distribution once disutilities are normalized by their means. It is symmetric if permuting agents permutes shares. It satisfies Fair Share if in every normalized problem each agent's expected disutility is at most $1/n$ of her expected disutility for the whole bad:

$$\mathbb E_\mu\big(\varphi_i(X)\,X_i\big)\le\frac1n .$$

The social cost of $\varphi$ at $x$ is $\sum_i\varphi_i(x)x_i$, and $\varphi$ dominates $\psi$ if its social cost is at most that of $\psi$ at every profile and strictly lower at some profile.

For $\theta\in[0,1]$, let $\psi^\theta_i(x)=\frac1n+\frac{\theta}{n-1}\big(\frac{\bar x}{x_i}-1\big)$ (with $1/0=+\infty$). The Bottom-Heavy rule $\varphi^\theta$ orders agents by disutility, gives the full $\psi^\theta_i(x)$ to the longest prefix of low-disutility agents that fits into the simplex, splits the remainder equally among the next class of tied agents, and gives nothing to the others. The canonical rule is $\varphi^1$, whose prefix shares are $x_{N\setminus\{i\}}/(n(n-1)x_i)$.

Formalization targets

Goal: Theorem 17 (p. 16)

For every $n\ge2$, $\varphi^1$ is a symmetric API rule satisfying Fair Share, and for every symmetric API rule $\varphi$ satisfying Fair Share with $\varphi\ne\varphi^1$ somewhere on $\mathbb R^N_+$,

$$\sum_i\varphi^1_i(x)x_i\le\sum_i\varphi_i(x)x_i\ \ \forall x\in\mathbb R^N_+,\quad\text{with strict inequality for some }x .$$

Milestones

1. Proof of Proposition 14 (p. 25). Fair Share gives a supporting vector $\alpha$ with $\varphi_1(x)x_1\le\alpha\cdot(x-e^N)+\frac1n$ on $\mathbb R^N_+$, and then $\delta\ge0$ with $\varphi_i(x)\le\frac1n+\delta\big(\frac{\bar x}{x_i}-1\big)$.
2. Proposition 14 (p. 15). A symmetric API rule satisfies Fair Share iff for some $\theta\in[0,1]$

$$\varphi_i(x)\le\min\Big\{\frac1n+\frac{\theta}{n-1}\Big(\frac{\bar x}{x_i}-1\Big),1\Big\}\quad\forall i,\ x\in\mathbb R^N_+ .\tag{9}$$

3. Step 1 (p. 25). $\psi^\theta_i\ge0$ and $\sum_i\psi^\theta_i\ge1$, strictly off the diagonal for $\theta\ne0$; with a helper stating that $\varphi^\theta$ is a symmetric API rule satisfying (9).
4. Remark after Definition 15 (p. 16). The shares $\varphi^1_i(x)$ are anti-monotonic to the $x_i$.
5. Step 2 (p. 25). For $\theta=0$, (9) forces Equal Split on profiles with positive coordinates; for $\theta\in(0,1]$, a symmetric API rule satisfying (9) equals $\varphi^\theta$ or is dominated by it.
6. Step 3 (p. 26). $\varphi^{\theta^+}$ dominates $\varphi^{\theta^-}$ for $1\ge\theta^+>\theta^->0$.

Significance

Theorem 17 says that, for a bad, the efficiency cost of ex ante fairness without knowledge of the prior is resolved by a single explicit rule: no fair API rule is ever cheaper ex post, at any realization, than the Bottom-Heavy rule. This is the basis of the paper's worst-case and asymptotic comparisons for bads (competitive ratio and price of fairness, §5–6), and it contrasts with goods, where the undominated fair rules form a family. Proposition 14 is of independent use: it turns a condition on all priors (Fair Share) into a pointwise inequality on the rule.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the model (normalized random objects, API rules, Fair Share, ex post domination) and a path of eight milestones to the main theorem. The formalization also makes precise two points the printed proof leaves implicit: the convention $1/0=+\infty$ at $\theta=0$ and at zero disutilities, and the case $\theta=0$ of the final domination argument, which Step 3 does not cover.

Difficulty

The "only if" direction of Proposition 14 is the analytic core. Fair Share is a statement about expectations under every normalized distribution, and has to be turned into a bound on the rule at each profile. Testing Fair Share on finitely supported normalized laws shows that $f(x)=\varphi_1(x)x_1$ agrees with its concave majorant at $e^N$; extracting a supporting affine function there and pinning down its coefficients needs the symmetry of the rule and the boundary profiles $x=e^{\{i\}}$. Mathlib has supporting-hyperplane and separation theorems but no concavification operator.

The domination steps are exchange arguments around the threshold $\tilde t$ that defines the Bottom-Heavy rule. Step 3 compares two thresholds as $\theta$ varies; it is proved on profiles with distinct coordinates, and ties need a separate argument (the paper invokes continuity of the total disutility, while the rule itself is discontinuous there). The natural first idea, that $\varphi^1$ minimizes cost among rules satisfying (9) for $\theta=1$, does not suffice: a fair rule may satisfy (9) only for a smaller $\theta$, so the comparison across the whole family is needed, and the case $\theta=0$ (Equal Split) requires the anti-monotonicity of $\varphi^1$ and Chebyshev's sum inequality.

Formalization scope

Agents are Fin n (0-based; the paper's agent 1 is agent 0), and $n\ge2$ throughout. Profiles are vectors x : Fin n → ℝ; $\mathbb R^N_+$ is 0 ≤ x and includes zero coordinates. A distribution is a measure on Fin n → ℝ, normalized meaning probability, carried by the orthant, integrable coordinates with mean $1$. An API rule is a measurable map (Fin n → ℝ) → (Fin n → ℝ) that is simplex-valued on the orthant; values off the orthant never matter. Fair Share quantifies over all normalized laws, not only finitely supported ones. Domination is for a bad: lower social cost, weakly everywhere on the orthant and strictly somewhere.

The convention $1/0=+\infty$ is explicit: the bound (9) is $1$ whenever $x_i=0$, for every $\theta$; in $\varphi^\theta$ with $\theta>0$, agents with zero disutility split the bad equally (at $x=0$ this is $e^N/n$). The threshold $\tilde t$ is encoded at the level of values (prefix masses $\sum_{j:x_j\le v}\psi^\theta_j$) rather than by sorting. Two printed claims are posed in corrected form and disclosed in the statements: the case $\theta=0$ of Step 2 holds only on profiles with all coordinates positive, and "α ≥ 0" in the proof of Proposition 14 is $\beta\ge0$.

A trivializing formalization is ruled out: the goal asserts that $\varphi^1$ is itself a symmetric API rule satisfying Fair Share (so a mis-encoded $\varphi^1$, such as the cost-minimizing utilitarian rule, cannot pass), "other" means differing at some profile of the orthant, and domination includes a strict inequality.

A complete development needs: integrals of bounded measurable functions against probability measures on Fin n → ℝ; a supporting-hyperplane or concave-envelope argument for Proposition 14; finite-sum manipulations over filtered Finsets and Chebyshev's sum inequality for the domination steps; measurability of piecewise-defined maps. The model layer (normalized random objects, API rules, Fair Share, domination) is reusable for the goods half of the paper. Proofs of any milestone, and sanity checks of the definitions (Example 16 for $n=2$), are welcome.

Selected references

• A. Bogomolnaia, H. Moulin, F. Sandomirskiy, On the Fair Division of a Random Object, arXiv:1903.10361v4, 2021; Management Science 68(2), 2022. https://arxiv.org/abs/1903.10361
• H. Moulin, Fair Division in the Internet Age, Annual Review of Economics 11, 2019. https://doi.org/10.1146/annurev-economics-080218-025559
• R. Laraki, On the Regularity of the Convexification Operator on a Compact Set, Journal of Convex Analysis 11(1), 2004.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.

Motivation

Firms that sell large catalogues of digital goods (streaming titles, cable channels, software features) rarely price every subset of products separately: with $N$ products there are $2^N$ bundles. A common simplification is bundle-size pricing (BSP), where the price depends only on how many items the customer takes and the customer picks which items go into the bundle. BSP sits between pure bundling (one price for everything) and full mixed bundling, and its menu has only $N$ prices.

Bakos and Brynjolfsson (Management Science, 1999) showed that for many products a pure bundle extracts almost all surplus under suitable concentration. Armstrong (Review of Economic Studies, 1999) showed that a cost-based two-part tariff asymptotically achieves the perfect-price-discrimination profit. Chu, Leslie and Sorensen (American Economic Review, 2011) computed optimal BSP menus numerically for up to five goods. Abdallah, Asadpour and Reed (Operations Research, 2021) develop an asymptotic theory of BSP as $N \to \infty$. This mission formalizes their homogeneous-cost result: with identical marginal costs, optimal BSP asymptotically earns the perfect-price-discrimination profit.

Setting

A firm sells $N$ products to one customer with valuations $X_1, \dots, X_N \ge 0$, additive over bundles. Let $X_{(1)} \le \dots \le X_{(N)}$ be the order statistics. A bundle of size $n$ is worth $V_N(n) = \sum_{k=0}^{n-1} X_{(N-k)}$ to the customer, the sum of her $n$ largest valuations, with $V_N(0) = 0$. The firm incurs a marginal cost $c_n \ge 0$ for item $n$, so a bundle of size $n$ costs $c_N(n) = \sum_{k=0}^{n-1} c_{\tau(N-k)}$, where $\tau$ lists the items by valuation and ties go to the lowest index.

A BSP menu is $p = (p(1), \dots, p(N))$ with $p(n) \in \mathbb R_+ \cup \{+\infty\}$, where $+\infty$ means size $n$ is not offered. The customer buys a size $\zeta(X,p) \in \arg\max_{0 \le n \le N} (V_N(n) - p(n))$, with $n = 0$ the free no-purchase option. The firm's profit is $\pi(p) = \sum_{n=1}^N (p(n) - c_N(n))\,\mathbf 1\{\zeta(X,p) = n\}$, and the BSP problem is $\mathbb E[\pi(p^\star_N)] = \sup_p \mathbb E[\pi(p)]$. The benchmark is perfect price discrimination, $\mathrm{PPD} = \sum_{n=1}^N \mathbb E[(X_n - c_n)^+]$, the most any selling mechanism can earn.

The large-offering regime describes the valuations as one random sequence $X_1, X_2, \dots$:

• (Assumption 1) the empirical distribution function $\mathbb F_{X,N}(x) = \frac1N\sum_{n \le N}\mathbf 1\{X_n \le x\}$ converges in probability to $F_X(x)$ for each $x \ge 0$, where $F_X$ is the distribution function of a nonnegative variable with finite mean $\mu$;
• (Assumption 2) $\{X_n\}$ is uniformly integrable and $\frac1N\sum_{n\le N} X_n \to \mu$ in probability;
• (Assumption 3) the costs are bounded and their empirical distribution converges.

The normalized curves are $\bar V_N(t) = \frac1N V_N(\lfloor Nt\rfloor)$ and $\bar c_N(t) = \frac1N c_N(\lfloor Nt\rfloor)$ for $t \in [0,1]$. The quantile function is $F_X^{-1}(s) = \inf\{x \ge 0 : F_X(x) \ge s\}$.

Formalization targets

Goal: Theorem 2

With identical costs $c_n = c \ge 0$, for every $t \in [0,1]$,

$$\bar V_N(t) \Rightarrow \bar V(t) = \int_0^t F_X^{-1}(1-s)\,ds, \qquad \bar c_N(t) \Rightarrow t c.$$

The size fraction $t^\star = \sup\{s : F_X^{-1}(1-s) \ge c\}$ maximizes $\bar V(t) - tc$ over $[0,1]$, and $t^\star = 1 - F_X(c)$ when $c$ is a continuity point of $F_X$. If $F_X(c) < 1$,

$$\lim_{N\to\infty}\frac{\mathbb E[\pi(p^\star_N)]}{\mathrm{PPD}} = 1.$$

Theorem 1 and the steps of the proofs

Theorem 1 is the general principle behind the goal. Suppose $\bar V_N \Rightarrow \bar V$ and $\bar c_N \Rightarrow \bar c$ pointwise, with nondecreasing continuous limits, and $t^\star \in \arg\max \bar V - \bar c$. Offer the single size $\lfloor Nt^\star\rfloor$ at price $N\bar V(t^\star) - g(N)$, where $g(N)$ grows faster than $\sqrt{\mathbb E[(V_N(\lfloor Nt^\star\rfloor) - N\bar V(t^\star))^2]}$ but is $o(N)$. Then

$$\frac{\mathbb E[\pi(p_N)]}{\mathbb E[\pi(p^\star_N)]} \to 1, \qquad \frac{\mathbb E[\pi(p_N)]}{N(\bar V(t^\star) - \bar c(t^\star))} \to 1.$$

The milestones follow the appendix proofs in order:

1. the pathwise bound $\pi(p)/N \le \sup_t \bar V_N(t) - \bar c_N(t)$;
2. the upper limit (A1);
3. the purchase probability (A4);
4. the lower limit (A5);
5. Theorem 1;
6. (A6), with $\mu = \int_0^1 F_X^{-1}(1-s)\,ds$;
7. the identity between $\bar V_N$ at grid points and integrals of the empirical quantile function;
8. convergence of empirical quantiles at continuity points;
9. (A7);
10. $\mathrm{PPD}/N \to \bar V(t^\star) - t^\star c$;
11. $\int_0^1 (F_X^{-1}(1-s) - c)^+ds = \bar V(t^\star) - t^\star c$.

Significance

Theorem 2 says that, with identical marginal costs and enough statistical concentration across products, a menu of $N$ size prices earns, to first order, everything a seller who knew each valuation could earn. Theorem 1 says more: one well-chosen bundle size, sold at a price slightly below its fluid value, is asymptotically as good as the optimal BSP menu. The paper's later results on heterogeneous costs (Theorems 3–4), clustered BSP and unknown budgets reuse this framework: Theorem 1 reduces each of them to computing the limit curves $\bar V$ and $\bar c$.

The results are proved in the paper and have no machine-checked version. This mission formalizes them under a weak-convergence hypothesis on the empirical distribution, with no independence assumption. The formal statements also fix points the page leaves implicit: the tie-breaking rules, the value of the BSP problem as a supremum, and the case $F_X(c) = 1$, where the goal's ratio degenerates.

Difficulty

The obvious route to Theorem 2 goes through Theorem 1, as the paper does. That needs a $g(N)$ dominating the $L^2$ fluctuation of $V_N(\lfloor Nt^\star\rfloor)$, and Assumptions 1–2 give no second moments. A proof of the goal must therefore avoid Theorem 1's $g(N)$ condition or replace it with a weaker device.

The convergence $\bar V_N(t) \Rightarrow \bar V(t)$ is a statement about sums of top order statistics of a dependent sequence. Pointwise convergence of the empirical cdf does not by itself control the upper tail, which carries the mass of $V_N$. The weak law and uniform integrability have to supply that control.

The upper bound (A1) requires exchanging a supremum over $t$ with a limit in probability, which uses monotonicity of $\bar V_N, \bar c_N$ in $t$ and continuity of the limits. The step "$\bar V_N(t) = \int_0^t \mathbb F^{-1}_{X,N}(1-s)\,ds$ for $0 \le t \le 1$" holds only at grid points $t = n/N$, so the off-grid error must be bounded separately.

Formalization scope

Everything lives in the namespace LargeBSP.Homog. Items are 0-indexed: coordinate n < N is the paper's item $n+1$. The valuations are one sequence X : ℕ → Ω → ℝ on a probability space, measurable and nonnegative; the $N$-product model uses its first $N$ terms. $F_X$ is cdf ν for a probability measure ν on $\mathbb R$ with $\nu(-\infty,0) = 0$ and finite mean. "$\Rightarrow$" toward a constant is convergence in probability (TendstoInMeasure); deterministic sequences use Tendsto.

Menus are ℕ → WithTop ℝ, with ⊤ meaning "not offered". Within a bundle size, items are ranked by valuation with ties to the lowest index, as on the page. Among sizes, the customer picks the smallest maximizer of surplus, a disclosed tie-break, so an indifferent customer does not buy. $\mathbb E[\pi(p^\star_N)]$ is the real supremum of the expected profit over all menus with prices in $\mathbb R_+\cup\{\infty\}$. It is bounded by $\mathbb E\sum_{n\le N}X_n$, so it is never the junk value of an unbounded supremum.

The quantile is $\inf\{y \ge 0 : F(y) \ge s\}$. Its set is empty only outside $(0,1)$, where Lean returns $0$; every use is at $s\in(0,1)$ or inside an integral. The set defining $t^\star$ is taken over $(0,1)$.

Disclosed readings:

• the hypothesis $F_X(c) < 1$ on the goal's ratio claim (otherwise $\mathrm{PPD}/N \to 0$ and the ratio is undetermined);
• in Theorem 1, continuity of $\bar V, \bar c$ (stated where the theorem is introduced and used in its proof) and $\bar V(t^\star) > \bar c(t^\star)$ (the second ratio's denominator);
• $\omega_+$ and $o(\cdot)$ encoded as $\mathbb E[\cdot^2]/g^2 \to 0$ and $g/N \to 0$ with $g$ eventually positive;
• the grid-point form of the $\bar V_N$–quantile identity.

The tail condition (6) of the paper is not assumed: neither proof uses it.

The goal cannot be satisfied trivially. $\mathbb E[\pi(p^\star_N)]$ is the value of the BSP problem over all menus, not a chosen menu. PPD is the sum of the per-item expectations. The instance $X_n \equiv 1$, $c = 1/2$ satisfies every hypothesis with $\mathrm{PPD} = N/2 > 0$, $\bar V(t) = t$ and $t^\star = 1$. So the ratio is neither $0/0$ nor fixed by a degenerate menu.

Needed infrastructure: order statistics of a finite family through a rank function, empirical distribution and quantile functions, the identity "mean = integral of the quantile function", convergence of quantiles under weak convergence (van der Vaart, Lemma 21.2), and uniform integrability of averages. These parts are reusable well beyond pricing. Contributions are welcome on any milestone, and on proofs of the goal that bypass Theorem 1's second-moment condition.

Selected references

• T. Abdallah, A. Asadpour, J. Reed, Large-Scale Bundle-Size Pricing: A Theoretical Analysis, Operations Research 69(4), 2021 (author's manuscript used). https://doi.org/10.1287/opre.2020.2097
• Y. Bakos, E. Brynjolfsson, Bundling Information Goods: Pricing, Profits, and Efficiency, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1613
• M. Armstrong, Price Discrimination by a Many-Product Firm, Review of Economic Studies 66(1), 1999. https://doi.org/10.1111/1467-937X.00079
• C. S. Chu, P. Leslie, A. Sorensen, Bundle-Size Pricing as an Approximation to Mixed Bundling, American Economic Review 101(1), 2011. https://doi.org/10.1257/aer.101.1.263
• A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 2000, Chapter 21. https://doi.org/10.1017/CBO9780511802256

Motivation

Public buyers of medicines, school meals, computers and similar goods often run a framework agreement. A central agency selects an assortment of products through an auction and fixes their unit prices. Public offices then buy from that menu as needed, each choosing what suits it. The European Union awarded €80 billion through framework agreements in 2010, 17% of all public procurement by value. Chile's ChileCompra bought US$3 billion this way in 2018, 22% of the country's public procurement (figures as cited in the paper's introduction). Two decisions are bundled in such a mechanism: which differentiated products to put in the assortment, and at what prices. A larger assortment serves heterogeneous users better; a smaller one lets the buyer extract lower prices from the suppliers, whose costs are private.

Saban and Weintraub (Operations Research, 2021; author version SSRN 3453144) model this trade-off as a mechanism-design problem and ask a structural question: how much does the buyer lose by being restricted to linear prices, where users pick quantities from the posted menu and every supplier is paid its unit price times the quantity sold, compared with a centralized planner who could dictate allocations and arbitrary transfers? Their answer for the Hotelling model of horizontal differentiation, Theorem 4.1, is the goal of this mission.

Setting

There are $n \ge 2$ suppliers $i \in N = \{1,\dots,n\}$. Supplier $i$ has a private unit cost $\theta_i$ in a finite set $\Theta_i$ of positive reals, drawn independently with probability mass function $f_i > 0$ and cdf $F_i$. A profile is $\theta = (\theta_1,\dots,\theta_n) \in \Theta = \prod_i \Theta_i$.

A unit mass of consumers sits uniformly on $[0,1]$; supplier $i$ is located at $\ell_i$, with $0 \le \ell_1 < \dots < \ell_n \le 1$. A consumer at $u$ buying from $i$ at price $p_i$ has utility $-(\delta|\ell_i - u| + p_i)$, with transportation cost $\delta > 0$. Allocations $x \in \mathcal X = \{x \ge 0 : \sum_i x_i = 1\}$ (no outside option) give gross consumer surplus $GCS(x)$, minus $\delta$ times the total transportation cost, and consumer surplus $CS(x,p) = GCS(x) - \sum_i p_i x_i$. The demand $d(Q,p)$ for an assortment $Q \subseteq N$ and prices $p$ is a maximizer of $CS(\cdot, p)$ over $x \in \mathcal X$ with $x_i = 0$ for $i \notin Q$.

The virtual cost of type $\theta_i$ is

$$v_i(\theta_i) = \theta_i + \frac{F_i(\rho_i(\theta_i))}{f_i(\theta_i)}\big(\theta_i - \rho_i(\theta_i)\big),$$

where $\rho_i(\theta_i)$ is the predecessor of $\theta_i$ in $\Theta_i$ (itself for the lowest type). Virtual costs are assumed strictly increasing (Assumption 3.1).

In a direct mechanism with allocation $x(\theta)$ and transfers $t(\theta)$, supplier $i$ of type $\theta_i$ reporting $\theta_i'$ gets interim utility $U_i(\theta_i' \mid \theta_i) = \sum_{\theta_{-i}} f_{-i}(\theta_{-i})\big(t_i(\theta_i',\theta_{-i}) - \theta_i x_i(\theta_i',\theta_{-i})\big)$. The two problems are:

• Cent: maximize $\mathbb E_\theta[GCS(x(\theta)) - \sum_i t_i(\theta)]$ subject to incentive compatibility (IC), individual rationality (IR) and $x(\theta) \in \mathcal X$;
• DecLin: choose an assortment $q(\theta)$, unit prices $p(\theta)$ and an allocation $x(\theta)$ to maximize $\mathbb E_\theta[CS(x(\theta),p(\theta))]$ subject to (IC), (IR) with transfers $t_i = p_i x_i$, $x(\theta) \in \mathcal X$, and (Demand) $x(\theta) = d(q(\theta), p(\theta))$.

$OPT(\cdot)$ denotes the optimal value. Every DecLin mechanism is a Cent mechanism with the same value, so $OPT(DecLin) \le OPT(Cent)$ always.

Formalization targets

Goal: Theorem 4.1

Let $c^* = \min_{1 \le i \le n-1}(\ell_{i+1} - \ell_i)$. If (1) some profile has $|v_{i+1}(\theta_{i+1}) - v_i(\theta_i)| \le \delta(\ell_{i+1}-\ell_i)/4$ for all $i$, and (2) every $|\Theta_i| \ge 3$ and consecutive virtual costs differ by at most $\delta c^*/8$, then

$$OPT(DecLin) = OPT(Cent).$$

Milestones

The proof runs through the following statements, in attack order:

1. Proposition 3.1: an allocation maximizing $CS(\cdot, v(\theta))$ with decreasing interim allocations and transfers given by the discrete envelope formula (7) is optimal for Cent.
2. The explicit Hotelling demand (active set $Q(p)$, neighbours split the segment between them) maximizes consumer surplus.
3. Proposition 3.2 (parts 1–2) for the general Hotelling model: the Hotelling demand at virtual costs, with the transfers of Appendix B, is feasible, meets Proposition 3.1's conditions, and is ex-post individually rational.
4. Corollary 4.1: prices that reproduce the optimal allocation (10) and the optimal interim transfers (11) give $OPT(DecLin) = OPT(Cent)$.
5. For the Hotelling model, (10) is the linear system $A(\theta)p(\theta) = A(\theta)v(\theta)$ of $(M_i(\theta))$ and (13).
6. Lemma F.1, the finite Fredholm alternative.
7. Lemma F.2: an all-active box of profiles, and paths of profiles that change one active cost at a time.
8. Lemma F.3: a dependency (14) among the rows forces $\sum_{i \in Q(\theta)} g_i(\theta_i)x_i(\theta) = 0$.
9. Step 1 of the proof: (14) forces every transfer-row coefficient with a nonzero row to vanish.
10. Step 2 of the proof: with those coefficients zero, (15) holds.

Significance

The theorem identifies a regime where linear pricing, the format actually used in framework agreements, loses nothing relative to the best mechanism with arbitrary transfers. In general it does lose: the paper's Example 4.1 has $OPT(Cent) > OPT(DecLin)$ (values $-2.0638$ and $-2.0645$). The conditions say that virtual costs are close relative to the transportation cost, so that every supplier is in the optimal assortment for some profile and costs can be moved one supplier at a time without leaving the assortment. This gives a design guideline: when products are differentiated enough relative to cost uncertainty, posting unit prices suffices. The companion result for two-part tariffs (Proposition 4.1) and the affine-demand analogue (Theorem 4.2) are outside this mission.

The theorem has a complete proof in the paper (Appendix F and the electronic companion), but no machine-checked version exists. A formal proof would check the discrete-type envelope argument (Proposition 3.1), the explicit Hotelling demand as an optimal-transport maximizer, and the linear-algebraic consistency argument, which has gaps at ties (see Formalization scope). Each of these is reusable: the discrete Myerson characterization applies to any procurement or auction model with finite type spaces, and the Hotelling demand result applies to any model of spatial competition on a segment.

Difficulty

The obvious argument is: solve Cent by Proposition 3.1, then pick prices equal to virtual costs, which induce the right demand. This fails because prices must do two jobs at once. They must reproduce the centralized allocation through consumer choice, which pins down price differences among active suppliers profile by profile, and they must reproduce the interim transfers (11), which pins down averages of $p_i x_i$ across profiles. Prices equal to virtual costs satisfy the first and generally violate the second. The question becomes whether one linear system in all prices of all profiles is consistent.

Lemma F.1 converts consistency into the statement that every dependency among the rows is also a dependency of the right-hand side. Proving that requires showing that the coefficients on transfer rows vanish (Step 1), and this is where Theorem 4.1's conditions enter: Lemma F.2's all-active box and connecting paths propagate $g_i = 0$ from one profile to its neighbours. Without such connectivity the profiles split into classes whose transfer constraints conflict, which is exactly what happens in Example 4.1.

Formalization scope

The Lean development lives in the namespace ProcureAssort.Hotelling, with one definition item (Setting) and eleven theorem items. Conventions:

• Suppliers are Fin n, 0-indexed, ordered by location; $n \ge 2$ is assumed because $c^*$ needs two suppliers. Types are a Finset ℝ per supplier; "consecutive types" means no element strictly between. Profiles are dependent functions; all expectations are finite sums.
• $f_i > 0$ on $\Theta_i$ and $\sum f_i = 1$; $\Theta_i$ positive; Assumption 3.1 is a hypothesis of every Hotelling statement. In the model-free Proposition 3.1, consumption vectors are assumed nonnegative, as the paper's proof uses.
• $GCS(x) = -\delta \sum_i \int_{x_1+\dots+x_{i-1}}^{x_1+\dots+x_i}|u - \ell_i|\,du$: suppliers serve consecutive blocks of consumers in location order, which is the cost-minimizing assignment. For $n = 2$, $\ell = (0,1)$ it equals Example 2.1's $-\frac\delta2(x_1^2+x_2^2)$.
• (Demand) is consumer optimality, the defining property (2) of $d$. $OPT$ is a real supremum; both value sets are nonempty and bounded above by $0$ in the Hotelling instance.
• $Q(p)$ is defined with $\le$ as printed. At ties a supplier can be in $Q(p)$ with zero demand. For this reason, Proposition 3.2's uniqueness clause and Corollary 4.1's "only if" are not stated. Step 1 is stated for the transfer rows with a nonzero coefficient, the only rows the paper's argument uses. Lemma F.2's second property is stated in the existential form its proof establishes.

The goal cannot be satisfied trivially. DecLin ranges only over mechanisms whose allocation is consumer-optimal for the posted assortment and prices, and whose payments are price times quantity. DecLin therefore cannot choose allocations freely or pay lump sums, and an equality with OPT(Cent) is a substantive claim. The hypotheses are satisfiable, for example with two suppliers at $0$ and $1$, $\delta = 16$ and $\Theta_i = \{1,2,3\}$ uniform.

A complete development needs: finite-type mechanism-design bookkeeping (interim sums, the envelope formula), the Hotelling demand as a maximizer (a one-dimensional transport argument), finite-dimensional linear algebra for Lemma F.1, and the combinatorics of Lemma F.2. Contributions to any milestone are welcome, as are proofs of the Fredholm alternative and of the discrete Myerson lemma in general form.

Selected references

• D. Saban, G. Y. Weintraub, Procurement Mechanisms for Assortments of Differentiated Products, Operations Research, 2021. https://doi.org/10.1287/opre.2020.2053 (author version: https://ssrn.com/abstract=3453144)
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• R. V. Vohra, Mechanism Design: A Linear Programming Approach, Cambridge University Press, 2011. https://doi.org/10.1017/CBO9780511835216
• H. Hotelling, Stability in Competition, The Economic Journal 39(153), 1929. https://doi.org/10.2307/2224214

Motivation

A seller who sells over two periods, at a full price now and a discount later, loses revenue to strategic customers who wait for the discount. Waiting is costly to the customer only through availability risk: if inventory is scarce, the product may be gone by the second period. Inventory is usually known to the firm and not to its customers, so the firm can try to shape how scarce the product looks. Drakopoulos, Jain and Randhawa (SSRN 3191629, version of April 17, 2020) study this as a problem of Bayesian persuasion (Kamenica and Gentzkow, AER 2011) with many receivers: the firm commits to prices and to a signaling policy before it learns its inventory, and then sends each customer a recommendation.

Their two main results separate public from private information. Theorem 1 (p. 15): with a public signal, seen by all customers, the firm earns no more than with prices alone. Theorem 2 (p. 17): with personalized signals, which may depend on each customer's valuation and be randomized independently across customers, a simple Buy/Wait/No mechanism is optimal and strictly beats every public mechanism when the low inventory level is small. Personalized recommendations are the kind of information online retailers and travel platforms send (low-stock alerts, buy-now prompts).

Setting

There is a unit mass of customers with valuations distributed on $V=[0,b]$ with density $f$ and complementary distribution $\bar F(v)=\int_v^b f$; the hazard rate $f/\bar F$ is non-decreasing. The firm's inventory $Q$ is high, $q_H=1$ (enough for everyone), with probability $P(H)\in(0,1)$, and low, $q_L\in(0,1]$, with probability $P(L)=1-P(H)$. The monopoly price is $p^m=\arg\max_p p\bar F(p)$, and $\bar F^{-1}(q)$ is the valuation at which a mass $q$ of customers lies above.

A straightforward mechanism fixes prices $p_1,p_2\ge0$ and, after seeing $Q$, draws a latent index $k$ from a finite set with a state-dependent law; given $(Q,k)$, each $v$-customer is independently told Buy (in period 1), Wait (buy in period 2) or No. A customer who requests the product in a period with $s$ units left and demand of mass $D$ from the others gets it with probability $\mathrm{avail}(s,D)$: $0$ if $s\le0$, $1$ if $D\le s$, $s/D$ otherwise (random rationing). The mechanism is obedient if every customer (for almost every $v$) weakly prefers to follow her recommendation, given the availabilities she can expect conditional on it: (Buy-1)–(No), p. 40. The firm's revenue is the expected value of rationed sales $p_1\min\{D_1,Q\}+p_2\min\{D_2,(Q-D_1)^+\}$. A mechanism is public when the recommendations depend only on $(k,v)$ and obedience holds for each realized $k$.

The personalized mechanism (PS1)–(PS2), p. 17, sets $p_1=\bar F^{-1}(q_L)$. In state $L$ it tells customers with $v\ge p_1$ to buy and the rest No; in state $H$ it tells $v\ge p_1$ to buy with probability

$$\sigma_H(v)=\min\Big\{\frac{P(L)}{P(H)}\frac{v-p_1}{p_1-p_2},1\Big\}\tag{13}$$

and to wait otherwise, tells $p_2\le v<p_1$ to wait, and $v<p_2$ No. The price $p_2$ solves $\bar F(p_2)-p_2f(p_2)=\bar F(\bar v)$ (14) with $\bar v=\sup\{v:\sigma_H(v)<1\}$ (15).

Formalization targets

Goal: Theorem 2

If $q_L\le\bar F(p^m)$, then (14) has a root $p_2\in(0,p_1)$, and for every such root the mechanism (PS2) is obedient, its revenue $R_{private}$ is at least that of every obedient mechanism at any prices, and

$$R_{private}>R^*_\phi=P(L)\,\bar p_1\bar F(\bar p_1)+P(H)\,p^m\bar F(p^m),\qquad \bar p_1=\max\{\bar F^{-1}(q_L),p^m\}.\tag{11}$$

Milestones

1. Lemma 2 (p. 35): the L-state profit $\phi(t,p)$ of a public threshold $t$ satisfies $\phi(t,p)\le\max\{(\bar F^{-1}(q_L)-p)q_L,0\}$, and for $q_L<\bar F(p)$ its unique maximizer is $\bar F^{-1}(q_L)$.
2. Theorem 1 (c) (p. 15): $R^*_\phi$ is the largest revenue of a public mechanism.
3. Lemma 3 (p. 44): at fixed prices $p_1>p_2$, the $(t^*,p_1,p_2)$-mechanism built from an optimal threshold $t^*$ of the one-parameter program (A.16) is obedient, earns its value $\bar D(p_1,p_2)$, and is optimal among obedient mechanisms with those prices.
4. Lemma 4 (p. 44, corrected reading): if $\bar F(p_2)>q_L$, then $\bar D(p_1,p_2)\le\bar D(\bar F^{-1}(q_L),p_2)$.
5. (16) (p. 17): (PS2) is obedient and earns

$$R_{private}=P(H)p_2\bar F(p_2)+P(H)(p_1-p_2)\bar F(\bar v)+P(L)\int_{p_1}^{\bar v}(v-p_1)\,dF(v)+P(L)p_1q_L.$$

Significance

The result says that the value of information in this market lies entirely in its personalization: public information is worthless (Theorem 1), and private recommendations strictly raise revenue whenever low inventory is scarce relative to the monopoly market. The optimal mechanism is explicit and has a simple form, with the low-type firm selling out exactly in period 1 and the high-type firm mimicking it as far as incentive compatibility allows; in the paper's uniform example ($q_L=P(H)=1/2$) revenue rises from $1/4$ to $13/48$. The proof technique, a relaxation to a linear program over signal profiles followed by a dual reduction to a single threshold, is a template for many-receiver persuasion problems with congestion.

The theorems are proved in the paper; none of them has a machine-checked proof. The mission produces a formal model of strategic customers under rationing and personalized signaling, and the formal versions of the five steps. Two printed steps need correction to be true and are stated in corrected form (Lemma 4's tie case, the location of the root of (14)); formal proofs settle that the corrections suffice.

Difficulty

The obvious argument is a pointwise one: for each valuation, the Buy incentive constraint caps the high-state Buy probability given the low-state one, so set every cap tight. It fails because the availabilities in the constraints depend on the aggregate masses that the recommendations themselves create, so the constraints for different valuations are coupled; the paper resorts to an infinite-dimensional linear program and asserts strong duality without proof (p. 41). Lemma 4 is the algebraically heavy step (pp. 46–50): an envelope argument over the threshold combined with the hazard-rate monotonicity. Theorem 2 then needs a one-dimensional optimization in $p_2$, the existence of a root of (14) (a fixed-point equation, since $\bar v$ depends on $p_2$), and the case $p_2>p_1$, which the paper never treats.

Formalization scope

The paper's game (Definitions 1–2: a continuum of customers, Bayesian Nash equilibrium, sender-preferred selection) is re-expressed as the class its proofs reduce to by the revelation principle (p. 39, footnote 5): obedient straightforward mechanisms with aggregate masses. Revenue optimality over this class is what Theorem 2 asserts after that reduction. The latent index is finite (Fin n, for every n); it carries the correlation between customers' signals that public signals need. Obedience is required for almost every valuation, as in Definition 1.

Committed conventions: $V=[0,b]$, $b>0$, $f$ continuous on $[0,b]$ and positive on $[0,b)$; $0<P(H)<1$, $0<q_L\le1$; $q_H=1$ and customer mass $1$. Availability is avail above; at zero demand it is $1$ with stock left and $0$ without. (14) is written $\bar F(p_2)-p_2f(p_2)=\bar F(\bar v)$. In (PS2)(a) "$v>p_1$" is taken as $v\ge p_1$ (a null set). (B) is read with $\min\{\cdot,1\}$. The program (A.16) keeps the no-Buy mechanism ($\bar F(t)=0$), which the printed version drops. "The optimal mechanism" is stated as "an optimal mechanism" (ties exist). Lemmas 3–4 take $p_2<p_1$, implicit in the paper's divisions; the goal ranges over all prices $p_1,p_2\ge0$, including $p_2>p_1$ (p. 8). Milestone (16) is stated at the prices of (PS1): $p_1=\bar F^{-1}(q_L)$ and $p_2\in[0,p_1)$ a root of (14).

Trivializing formalizations are ruled out: revenue counts rationed sales, not $p_1D_1+p_2D_2$; obedience is the printed conditional constraint multiplied by the probability of the recommendation, never divided by a possibly zero probability; availability never uses Lean's $x/0=0$; the goal carries the existence of a root of (14), so "for every root" is not vacuous; the mechanism class contains public and correlated mechanisms; and $R_{private}$ is the revenue of the mechanism (PS2), tied to the formula (16) by a milestone.

A complete development needs: the density measure on $[0,b]$ and its tail function $\bar F$, monotonicity and continuity of $\bar F$ and its inverse, the quasi-concavity of $p\bar F(p)$ under a non-decreasing hazard rate, and bounds for the rationing function. The hazard-rate and $\bar F^{-1}$ lemmas are reusable for other pricing models. Contributions of helper lemmas, of a primal proof of Lemma 3 avoiding the duality argument, and of the case $p_2>p_1$ are welcome.

Selected references

• K. Drakopoulos, S. Jain, R. S. Randhawa, Persuading Customers to Buy Early: The Value of Personalized Information Provisioning, SSRN working paper 3191629, version of April 17, 2020. https://ssrn.com/abstract=3191629
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6):2590–2615, 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Bergemann, S. Morris, Information Design: A Unified Perspective, Journal of Economic Literature 57(1):44–95, 2019. https://doi.org/10.1257/jel.20181489