All missions

Motivation

Loss aversion, the tendency to weigh a loss more heavily than a gain of the same size, is the central ingredient of reference-dependent preferences. Measured degrees of loss aversion vary widely across experiments and markets. One explanation is that the reference point is not fixed. People form it partly from their own expectations about what they will choose, and partly from an external benchmark. He and Strub (SSRN 3318295; Operations Research, 2022, doi:10.1287/opre.2022.2309) ask how this endogenization changes the loss aversion an outside observer would infer from portfolio choices in a complete market.

The relevant models have a short history. Kőszegi and Rabin (QJE 2006; AER 2007) introduced personal equilibrium: a plan that remains optimal when it serves as its own reference point. De Giorgi and Post (Management Science 2011) introduced a state-dependent version together with a partially endogenous variant, in which deviating from an exogenous benchmark carries a mental cost. They applied it to a choice among four strategies. He and Strub solve the partially endogenous model for a general portfolio problem.

Setting

An agent with initial wealth $x_0>0$ buys a prospect, a nonnegative random variable $X$ on a probability space $(\Omega,\mathcal F,P)$. The market is complete with pricing kernel $\rho>0$, integrable, so $X$ costs $\mathbb E[\rho X]$. The affordable prospects form $\mathcal X(x_0)=\{X\ \mathcal F\text{-measurable}: X\ge 0,\ \mathbb E[\rho X]\le x_0\}$.

Given a reference point $B$ (itself a prospect), the agent values $X$ by

$$V_\lambda(X\mid B)=\mathbb E[u(X)]+\alpha\,\mathbb E\big[\mu(u(X)-u(B))\big],\qquad \mu(z)=z\mathbf 1_{\{z\ge0\}}+\lambda z\mathbf 1_{\{z<0\}}.$$

Here $\alpha>0$ is the weight of gain-loss utility and $\lambda\ge 1$ is the intrinsic degree of loss aversion. The utility $u$ satisfies Assumption 1: it is strictly increasing, strictly concave and $C^1$ on $(0,\infty)$, with $u(0)=\lim_{x\downarrow0}u(x)\in[-\infty,\infty)$, the Inada conditions, and integrability of $\rho\,(u')^{-1}(\nu\rho)$ and $u((u')^{-1}(\nu\rho))$ for every $\nu>0$. Reference points satisfy $\mathbb E|u(B)|<\infty$, and an expectation $\mathbb E[Y]$ is $-\infty$ whenever $\mathbb E|Y|=\infty$.

With an exogenous reference point $B_0$, problem (4) maximizes $V_\Lambda(X\mid B_0)$ over $\mathcal X(x_0)$. Its optimum is denoted $X^*_{\rm ex}(\Lambda)$. A threshold $\lambda_{\max}\in[1,+\infty]$, given by an explicit formula (6) in terms of $\operatorname{esssup}$ and $\operatorname{essinf}$ of $u'(B_0)/\rho$, marks where $X^*_{\rm ex}(\Lambda)$ stops depending on $\Lambda$.

A mental cost $f_{B_0}(V_\lambda(X\mid B_0))$, with $f_{B_0}$ strictly decreasing and continuous, is charged for choosing $X$. An agent who tolerates cost at most $c_0$ chooses from $\mathcal Y(B_0,c_0)=\{X\in\mathcal X(x_0): f_{B_0}(V_\lambda(X\mid B_0))\le c_0\}$. A partially endogenous PE is an $X\in\mathcal Y(B_0,c_0)$ with $V_\lambda(X\mid X)\ge V_\lambda(Y\mid X)$ for all $Y\in\mathcal Y(B_0,c_0)$. The partially endogenous PPE $X^*_{\rm pe}(\lambda,c_0)$ maximizes $V_\lambda(X\mid X)$ among these.

Formalization targets

Goal: Theorem 3 (p. 19)

Let $\underline c=f_{B_0}(V_\lambda(X^*_{\rm ex}(\lambda)\mid B_0))$ and $\bar c=f_{B_0}(V_\lambda(X^*_{\rm ex}(1)\mid B_0))$. Then

$$X^*_{\rm pe}(\lambda,c_0)=\begin{cases}X^*_{\rm ex}(\lambda)=X^*_{\rm ex}(\lambda\wedge\lambda_{\max}), & c_0=\underline c,\\ X^*_{\rm ex}(\Lambda_{\rm pe}(c_0)), & \underline c<c_0<\bar c,\\ X^*_{\rm ex}(1)=(u')^{-1}(\nu\rho), & c_0\ge\bar c.\end{cases}$$

Here $\Lambda_{\rm pe}(c_0)\in(1,\lambda\wedge\lambda_{\max})$ is the unique solution of $f_{B_0}(V_\lambda(X^*_{\rm ex}(\Lambda)\mid B_0))=c_0$. It is strictly decreasing and continuous, with limits $\lambda\wedge\lambda_{\max}$ as $c_0\downarrow\underline c$ and $1$ as $c_0\uparrow\bar c$. In each case the partially endogenous PPE exists and is unique up to almost sure equality.

Milestones

1. $V_\lambda(X\mid X)=\mathbb E[u(X)]$ (proof of Theorem 2).
2. Theorem 1: the optimum of (4) exists, is unique, and is given by the three-region formula (5) with a budget-exhausting multiplier; the optimum and its value vary continuously with $(\lambda,\alpha)$.
3. Proposition 1 (i)–(iii): $X^*_{\rm ex}(\lambda)$ is gains-only, equal to $B_0$, or losses-only exactly when $\lambda\ge\lambda_{\max}$.
4. Proposition 1, "Furthermore": $X^*_{\rm ex}(\Lambda)$ is constant on $[\lambda_{\max},\infty)$ and injective on $[1,\lambda_{\max})$.
5. Theorem 2: the personal equilibria are characterized by (7), and the preferred one is $(u')^{-1}(\nu\rho)$.
6. Problem (10) is equivalent to problem (16), which maximizes $\mathbb E[u(X)]$ over $\mathcal Y(B_0,c_0)$.
7. The Lagrangian of (17) equals a positive multiple of $V_{\Lambda(\eta)}(X\mid B_0)$ plus a constant, with $\Lambda(\eta)$ given by (19).
8. $\Lambda\mapsto V_\lambda(X^*_{\rm ex}(\Lambda)\mid B_0)$ is continuous on $[1,\infty)$.
9. The same map is strictly increasing on $[1,\lambda\wedge\lambda_{\max})$.
10. $\Lambda_{\rm pe}(c_0)$ exists and is unique, and $X^*_{\rm ex}(\Lambda_{\rm pe}(c_0))$ solves (17).

Significance

Theorem 3 says that partial endogenization is observationally a reduction of loss aversion. An agent with intrinsic degree $\lambda$ and mental-cost tolerance $c_0$ chooses exactly what a standard agent with exogenous reference point $B_0$ and the lower degree $\Lambda_{\rm pe}(c_0)$ would choose. The exhibited degree interpolates monotonically between the intrinsic level (capped at $\lambda_{\max}$) and $1$, so empirical estimates of loss aversion confound the intrinsic parameter with the flexibility of the reference point. Theorem 2 is the other extreme: with a fully endogenous reference point and state-dependent evaluation, loss aversion has no effect at all.

The results are proved in the paper; none of them has a machine-checked proof. The mission adds a formal model of reference-dependent preferences in a complete market, with the paper's $-\infty$ convention for expectations and utilities with $u(0)=-\infty$. It also provides formal versions of the exogenous-reference optimum, the personal-equilibrium notions of Kőszegi–Rabin and De Giorgi–Post, and Theorem 3 itself. Three printed slips are corrected along the way: the second limit of Theorem 3 (iii), the constant in the rewrite of (18), and the budget condition in Theorem 2.

Difficulty

Given its inputs, the proof of Theorem 3 is short: a Lagrangian rewrite, the intermediate value theorem and a duality step. The inputs carry the weight. Theorem 1 is an existence and uniqueness result for an infinite-dimensional concave problem whose objective is not differentiable where $X=B_0$. The optimal multiplier is defined implicitly, through continuity and monotone limits of a budget map. Proposition 1 needs essential suprema and infima that can be $0$ or $+\infty$. Continuity of $\Lambda\mapsto V_\lambda(X^*_{\rm ex}(\Lambda)\mid B_0)$ needs dominated convergence under Assumption 1. Strict monotonicity uses Proposition 1's injectivity, and it fails to be strict at $\lambda_{\max}$.

A first idea is to maximize $V_\lambda(X\mid X)$ directly over $\mathcal Y(B_0,c_0)$. This identifies the PPE only after the reduction (10) ⇔ (16) is proved, and that reduction uses $\lambda\ge1$ through $\mu(z)\le z$.

Formalization scope

Everything is defined in the namespace EndoRefLA.PartialPPE, in one definitions file. Conventions:

• Prospects are functions $\Omega\to\mathbb R$; "prospect" means measurable and pointwise nonnegative. Equalities between prospects are $P$-almost sure, and "unique" means unique up to a.s. equality.
• Expected utilities are extended reals computed with the paper's convention ($-\infty$ unless $\mathbb E|Y|<\infty$). Prices are lower Lebesgue integrals in $[0,\infty]$, so an unaffordable prospect never gets a junk price of $0$.
• $u(0)$ is a separate parameter in $[-\infty,\infty)$. Where $B_0=0$, $u'(B_0)=+\infty$ is handled explicitly.
• $\lambda_{\max}$ is an extended real with every infinite case written out. $\lambda\wedge\lambda_{\max}$ equals $\lambda$ when $\lambda_{\max}=+\infty$.
• The multipliers $\nu_G,\nu_L$ of (6) are passed as roots of their defining equations. Proposition 1 proves that the roots exist and are unique.
• The optima $X^*_{\rm ex}(\Lambda)$ are a family taken as a hypothesis ("an optimal solution of (4) for each $\Lambda\ge1$"); Theorem 1 shows that the family exists.
• The domain of $f_{B_0}$ is never stated. Here $f:\mathbb R\to\mathbb R$, and a prospect with $V_\lambda(X\mid B_0)=-\infty$ is not in $\mathcal Y(B_0,c_0)$.
• A PE candidate must satisfy $\mathbb E|u(X)|<\infty$, the paper's standing restriction on reference points.

$X^*_{\rm ex}(\Lambda)$ is the optimum of (4), not formula (5), and the PPE is the De Giorgi–Post equilibrium object, not the maximizer of (16). Defining either one by the formula that a milestone proves would make the goal tautological.

A complete development needs the following, all reusable beyond this mission: pointwise maximization of concave integrands under a budget constraint; continuity and monotonicity of budget maps in a Lagrange multiplier; and properties of $(u')^{-1}$ under the Inada conditions. Proofs of any milestone are welcome. The paper's other two models (§3.2–§3.3) are outside this mission.

Selected references

• X. D. He and M. S. Strub, How Endogenization of the Reference Point Affects Loss Aversion: A Study of Portfolio Selection, SSRN 3318295 (version of May 4, 2022); Operations Research, 2022. https://ssrn.com/abstract=3318295, https://doi.org/10.1287/opre.2022.2309
• E. G. De Giorgi and T. Post, Loss Aversion with a State-Dependent Reference Point, Management Science 57(6), 2011. https://doi.org/10.1287/mnsc.1110.1334
• B. Kőszegi and M. Rabin, A Model of Reference-Dependent Preferences, Quarterly Journal of Economics 121(4), 2006. https://doi.org/10.1093/qje/121.4.1133
• B. Kőszegi and M. Rabin, Reference-Dependent Risk Attitudes, American Economic Review 97(4), 2007. https://doi.org/10.1257/aer.97.4.1047
• A. B. Berkelaar, R. Kouwenberg and T. Post, Optimal Portfolio Choice under Loss Aversion, Review of Economics and Statistics 86(4), 2004. https://doi.org/10.1162/0034653043125167

Motivation

A stochastic game (Shapley, 1953) is a dynamic game in which the players' actions influence the evolution of a state variable. Whether every multiplayer stochastic game admits an $\varepsilon$-equilibrium for every $\varepsilon>0$ is open even for finitely many states and the long-run average payoff; it is open as well for the general class in which each player's payoff is an arbitrary bounded Borel-measurable function of the infinite play, introduced by Blackwell (1969). This class contains the discounted and long-run average payoffs and the winning conditions of verification (Büchi, parity, Müller).

Flesch and Solan (arXiv:2208.12096; Mathematics of Operations Research, 2024) prove a weaker, unconditional statement: every such game has a subgame that admits an $\varepsilon$-equilibrium. Their tool is the Martin function, a real-valued function on histories which reduces playing well in the stochastic game to playing well in a one-shot game at each history.

Timeline.

• 1981: Mertens and Neyman construct, for two-player zero-sum games with the long-run average payoff, functions with the properties later abstracted as Martin's.
• 1991: Thuijsman and Vrieze show that every two-player stochastic game with finitely many states and the long-run average payoff has an easy initial state, an initial state with an $\varepsilon$-equilibrium.
• 1998: Martin proves determinacy of Blackwell games, for two players, zero-sum, one state; Maitra and Sudderth extend it to countable state spaces.
• 2000: Vieille (2000c) introduces solvable states and proves their existence for $N$ players with the long-run average payoff and finitely many states.
• 2015: Mashiah-Yaakovi proves existence of extensive-form correlated $\varepsilon$-equilibria for bounded Borel payoffs.
• 2022: Ashkenazi-Golan, Flesch, Predtetchinski and Solan generalize the Martin function to multiplayer games (PNAS 119(11)).
• 2022–2024: Flesch and Solan obtain the existence of an $\varepsilon$-solvable subgame for every bounded Borel payoff.

The game, its subgames and its values

A stochastic game $\Gamma=(I,S,(A_i)_{i\in I},p,(f_i)_{i\in I})$ consists of

• a nonempty finite set $I$ of players;
• a nonempty finite or countable set $S$ of states;
• for each player $i$ a nonempty finite action set $A_i$, with $A=\prod_i A_i$;
• a transition $p(\cdot\mid s,a)\in\Delta(S)$;
• for each player a payoff function $f_i$, bounded and Borel-measurable on the space of runs $(s^1,a^1,s^2,a^2,\dots)$.

A history $h=(s^1,a^1,\dots,s^n)$ of stage $n$ is a finite prefix with positive transition probabilities; $H$ is the set of histories and $s_h$ the final state of $h$. A behavior strategy $\sigma_i$ assigns a mixed action $\sigma_i(h)\in\Delta(A_i)$ to every history. A profile $\sigma$ and a history $h$ determine a probability measure $\mathbf P_{h,\sigma}$ on runs that continue $h$. Player $i$'s payoff in the subgame $\Gamma_h$ is $\mathbf E_{h,\sigma}[f_i]=\int f_i(hr)\,\mathbf P_{h,\sigma}(dr)$, and the minmax value there is

$$\overline v_i(h)=\inf_{\sigma_{-i}}\sup_{\sigma_i}\mathbf E_{h,\sigma_i,\sigma_{-i}}[f_i].$$

A profile $\sigma$ is an $\varepsilon$-equilibrium in $\Gamma_h$ if no player gains more than $\varepsilon$ by a unilateral deviation, measured by $\mathbf E_{h,\cdot}[f_i]$. The subgame $\Gamma_h$ is $\varepsilon$-solvable if it has one (Definition 4.8).

A function $D_i:H\to\mathbb R$ induces at every $h$ the one-shot game $G_O(D,h)$, in which player $i$ receives $\mathbf E[D_i\mid h,a]=\sum_s p(s\mid s_h,a)D_i(h,a,s)$; its minmax value is $\overline v_{O,i}(D_i,h)$.

Formalization targets

Goal: Theorem 4.9

For every stochastic game as above and every $\varepsilon>0$,

$$\exists\,h\in H\ \ \exists\,\sigma:\qquad \mathbf E_{h,\sigma}[f_i]\ \ge\ \mathbf E_{h,\sigma_i',\sigma_{-i}}[f_i]-\varepsilon\quad\text{for all }i\in I\text{ and all strategies }\sigma_i'.$$

The history may depend on $\varepsilon$ and is not required to start in a prescribed initial state.

Milestones

1. Theorem 3.1 (minmax version): for every $\varepsilon>0$ and player $i$ there is a bounded $D^\varepsilon_i$ with $\overline v_i-\varepsilon\le D^\varepsilon_i\le\overline v_i$, $D^\varepsilon_i(h)\le\overline v_{O,i}(D^\varepsilon_i,h)$, and the local-to-global property (3).
2. Theorem 4.4: playing an equilibrium of $G_O(D^\varepsilon,h)$ at every $h$ gives $\mathbf E_{h,\sigma^*}[f_i]\ge\overline v_i(h)-\varepsilon$ for all $i$ and $h$ (a minmax $\varepsilon$-acceptable profile), so such a profile exists.
3. Eq. (10): for a prefix-free set $Q$ of histories and a stopping time $\theta$, the expected fictitious hitting count equals the probability of reaching $Q$ before $\theta$.
4. §4.4 Step 2: $(\mathbf E_{r^n,\sigma}[f_i])_n$ is a martingale converging almost surely to $f_i(r)$.
5. Eq. (15): under $\sigma^*$, $D^\delta_i(r^n)$ is a submartingale.
6. Eq. (19): an event of positive probability has conditional probability above $1-\delta$ at some history beyond any given stage.

Significance

The result. Theorem 4.9 is the strongest unconditional existence statement known for multiplayer stochastic games with general payoffs. When the payoffs are shift-invariant (long-run average, limsup, parity) the solvable subgame yields an initial state with an $\varepsilon$-equilibrium (Corollary 4.10). This recovers the results of Thuijsman and Vrieze (1991) and Vieille (2000c) for the long-run average payoff. Theorem 4.4 along the way answers a question of Simon (2016): no three-player zero-sum-on-every-play game has all minmax values strictly positive.

Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formalization produces:

• a reusable model of multiplayer stochastic games with payoffs on infinite plays, built on Mathlib's Ionescu-Tulcea kernel Kernel.traj;
• the one-shot reduction through Martin functions;
• a checked version of the martingale and stopping-time arguments of §4.4.

Difficulty

The first idea, to play the profile $\sigma^*$ of Theorem 4.4 everywhere, fails: $\sigma^*$ keeps every player above the minmax value, but it is not an equilibrium, because a player may prefer some actions in the support of its own mixed action or may steer the play to histories where its own minmax value is high. Handling the first problem needs a compact set of runs on which payoffs are almost constant and a way to identify who left it. That second ingredient is the blame function of Alon, Gunby, He, Shmaya and Solan (2022), which is not available on the platform. Handling the second needs the fictitious hitting counts of (8)–(10) and a careful choice of punishment thresholds. Theorem 3.1 itself is not proved in the paper: it rests on Martin's (1998) determinacy of Blackwell games, on the multiplayer extension of Ashkenazi-Golan et al. (2022a, Theorem 3.6 and Claim 3.5, with the modification of footnote 3), and on the countable-state method of Maitra and Sudderth (1998).

Formalization scope

• Players, states and actions. Players form a Fintype with decidable equality and are nonempty. States form a nonempty Countable type, and action sets are nonempty Fintypes, the same in every state. The transition is p : S → (∀ i, A i) → PMF S.
• Runs. A run is a sequence of coordinates: coordinate $0$ is $s^1$, coordinate $n+1$ is $(a^{n+1},s^{n+2})$. Each coordinate carries the discrete σ-algebra, and runs carry the product σ-algebra, which is the paper's Borel σ-algebra.
• Indexing and feasibility. A Lean history of index $n$ is the paper's history of stage $n+1$. Payoffs are defined on all sequences, not only on the closed set of runs with positive transitions; this is equivalent, since a bounded Borel function on that set extends and the set has full measure. Every quantifier over $H$ carries the predicate Feasible.
• Play measure. playMeasure G σ n h is Kernel.traj of the one-stage kernel (independent mixed actions, then $p$) started at $h$. Its runs begin with $h$, so ∫ f i ∂(playMeasure G σ n h) is $\mathbf E_{h,\sigma}[f_i]$.
• Values. $\inf$/$\sup$ and the one-shot $\min$/$\max$ are real ⨅/⨆; they are the paper's values because payoffs and Martin functions are bounded.
• One-shot equilibria. These are the platform's AGT.IsMixedNash.
• Not formalized. The maxmin version of Theorem 3.1 is not stated. Eq. (19) is stated for an arbitrary measurable event of positive probability, with the added and disclosed conclusion that $h^*$ has positive probability.
• No trivialization. The goal is stated for every game, with a feasible witness history and with deviations over all strategies. It is not stated for a fixed one-player or constant-payoff game, and $\varepsilon$-solvability is not weakened to deviations that agree with $\sigma$ before $h$.
• Infrastructure. A full development needs Markov properties of Kernel.traj (conditioning on the first $n$ coordinates), Lévy's upward and zero-one laws (the platform's FamousTheorems.levy_upward_theorem is Proved), and existence of Nash equilibria in finite games (AGT.nash_existence, Proved). It also needs regularity of probability measures on Polish spaces, and either a proof of Theorem 3.1 or the blame-function result of Alon et al. Contributions to any of these, and proofs of the milestones independently of one another, are welcome.

Selected references

• J. Flesch and E. Solan, Stochastic Games with General Payoff Functions, arXiv:2208.12096v1, 2022; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2208.12096
• D. A. Martin, The determinacy of Blackwell games, Journal of Symbolic Logic 63, 1565–1581, 1998. https://doi.org/10.2307/2586667
• A. Maitra and W. Sudderth, Finitely additive stochastic games with Borel measurable payoffs, International Journal of Game Theory 27, 257–267, 1998.
• G. Ashkenazi-Golan, J. Flesch, A. Predtetchinski and E. Solan, Existence of equilibria in repeated games with long-run payoffs, PNAS 119(11), e2105867119, 2022. https://doi.org/10.1073/pnas.2105867119
• N. Alon, B. Gunby, X. He, E. Shmaya and E. Solan, Identifying the deviator, arXiv:2203.03744, 2022. https://arxiv.org/abs/2203.03744
• L. S. Shapley, Stochastic games, PNAS 39(10), 1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• N. Vieille, Solvable states in N-player stochastic games, SIAM Journal on Control and Optimization 38, 1794–1804, 2000.
• F. Thuijsman and O. J. Vrieze, Easy initial states in stochastic games, in Stochastic Games and Related Topics, Springer, 85–100, 1991.
• A. Mashiah-Yaakovi, Correlated equilibria in stochastic games with Borel measurable payoffs, Dynamic Games and Applications 5, 120–135, 2015.
• D. Blackwell, Infinite G_δ-games with imperfect information, Applicationes Mathematicae 10, 99–101, 1969.

Services whose length the customer chooses

In many services the customer, not the provider, decides how long to stay: a gym session, a car-wash bay, an electric-vehicle charger, a call to a help line, a slot on a shared computing resource. Such services are called discretionary. Their congestion depends on how many customers join and on how long each of them stays. Providers manage them with per-use fees, with price rates per unit of time, and with time limits, caps on the time any one customer may spend in service. Time limits are common in practice (charging stations, library computers, public parking), and the operations literature on discretionary services (Hopp, Iravani and Yuen 2007; Tong and Rajagopalan 2014; Debo and Li 2020) studies how such systems should be priced and operated.

Feldman and Segev (SSRN 3424317) ask whether a time limit is merely convenient or actually optimal. Their answer for a single-server queue is that a revenue-maximising provider who may use any incentive-compatible price and time schedule chooses to impose a time limit when congestion is high, and that this mechanism attains the first-best social welfare.

Setting

Service needs arise as a Poisson process of rate $\Lambda > 0$ at a single server that serves in first-come-first-served order. A customer's type $\theta$ is her ideal time in service, uniformly distributed on $[0, \bar\theta]$ with $\bar\theta > 0$. Time $t$ in service is worth $\min\{t, \theta\}$ to a customer of type $\theta$. Customers pay a waiting cost $c > 0$ per unit of expected waiting time.

An allocation $(\Phi, t)$ consists of a measurable admitted set $\Phi \subseteq [0, \bar\theta]$ and a measurable time function $t$ with $0 \le t(\theta) \le \theta$ on $\Phi$. Its expected waiting time is the Pollaczek–Khinchine mean wait of the resulting M/G/1 queue, which for uniform types reads

$$W(\Phi, t) = \frac{\Lambda \int_\Phi t(\theta)^2\,d\theta}{2\left(\bar\theta - \Lambda \int_\Phi t(\theta)\,d\theta\right)},$$

and the allocation is feasible when the queue is stable, $\Lambda \int_\Phi t < \bar\theta$. Its social welfare is

$$SW(\Phi, t) = \frac{\Lambda}{\bar\theta}\int_\Phi \big(t(\theta) - c\,W(\Phi, t)\big)\,d\theta ,$$

and an allocation is first-best if it is feasible and maximises $SW$ among all feasible allocations.

A direct mechanism $(\Phi, t, p)$ adds a non-negative price $p(\theta)$ for $\theta \in \Phi$. It is incentive compatible (IC) if $\min\{t(\theta), \theta\} - p(\theta) \ge \min\{t(\theta'), \theta\} - p(\theta')$ for all $\theta, \theta' \in \Phi$, and individually rational (IR) if $\min\{t(\theta), \theta\} - p(\theta) - cW \ge 0$ on $\Phi$. Its revenue is $\pi = \frac{\Lambda}{\bar\theta}\int_\Phi p(\theta)\,d\theta$.

The thresholds of the paper are

$$\Lambda_1 = \frac{32\left(4c+5-\sqrt{2c(8c+7)}\right)}{3(26c+25)\,\bar\theta},\qquad \Lambda_2 = \frac{4\left(1-\sqrt{c/(c+2)}\right)}{\bar\theta},\qquad \widetilde T = \sqrt{\frac{\bar\theta}{\Lambda}\left(1-\sqrt{\frac{c}{c+2}}\right)} .$$

Formalization targets

Goal: Theorem 8

For each congestion regime, take the first-best allocation of Theorem 1:

$$t(\theta) = \begin{cases} \theta \text{ on } [\theta_l, \bar\theta] & \Lambda \le \Lambda_1,\\ \min\{\theta, T\} \text{ on } [\theta_l, \bar\theta] & \Lambda_1 \le \Lambda \le \Lambda_2,\\ \widetilde T \text{ on } [\widetilde T, 2\widetilde T] & \Lambda \ge \Lambda_2,\end{cases}$$

and the full-extraction price $p(\theta) = \min\{\theta, t(\theta)\} - c\,W(\Phi, t)$. Then $(\Phi, t)$ is first-best, $(\Phi, t, p)$ is a feasible IC and IR mechanism with $p \ge 0$, a non-admitted type gains nothing by claiming an admitted type, no IC and IR mechanism earns more revenue, and

$$\pi(\Phi, p) = SW(\Phi, t).$$

Milestones

1. Sub-problem (4) (pp. 35–36): on $[a, b]$, among $0 \le t \le \theta$ with $\int_a^b t = k$, $\int_a^b t^2$ is minimised uniquely (a.e.) by the constant $k/(b-a)$ when $k \le a(b-a)$ and by $\min\{\theta, T\}$, $T = b - \sqrt{b^2-a^2-2k}$, when $a(b-a) \le k \le (b^2-a^2)/2$.
2. The definition of $\Lambda_1$ (p. 39): without a time limit, $\partial SW/\partial\theta_l = 0$ at $\theta_l = \bar\theta/4$ exactly when $\Lambda = \Lambda_1$.
3. Theorem 1, $\Lambda \ge \Lambda_2$: admitting $[\widetilde T, 2\widetilde T]$ at time $\widetilde T$ is first-best, with welfare $\tfrac12(c+2)\big(1-\sqrt{c/(c+2)}\big)^2$.
4. Theorem 1, $\Lambda \le \Lambda_1$: a unique $\theta_l$ with $[\theta_l, \bar\theta]$, $t(\theta) = \theta$ first-best.
5. Theorem 1, $\Lambda_1 \le \Lambda \le \Lambda_2$: a unique pair $\theta_l \le T$ with $[\theta_l, \bar\theta]$, $t = \min\{\theta, T\}$ first-best.
6. A strict time limit (p. 39): for $\Lambda_1 < \Lambda \le \Lambda_2$ the first-best $T$ is $< \bar\theta$.
7. Revenue is bounded by welfare (p. 47) for every IR mechanism.
8. Full extraction (p. 47): the price $\min\{\theta, t(\theta)\} - cW$ is IC, leaves zero utility, and turns revenue into welfare.

Significance

The result. Theorem 1 shows that the welfare-optimal schedule in a discretionary M/G/1 service is an admission threshold followed, at high congestion, by a time limit. The reason is that the waiting time depends on the second moment of service times, and a time limit is the cheapest way to cut that second moment for a given total service. Theorem 8 then shows that a monopolist with unrestricted pricing loses nothing relative to the planner: the optimal mechanism reproduces the first best, time limit included, and extracts all surplus. Together they justify time limits as an optimal instrument rather than a heuristic, and they supply the benchmark ($\mathcal{FB} = \pi^*$) against which the paper's simpler schemes, per-use fees and price rates with or without limits, are compared in its Theorem 10.

The formalization. The results are proved in the paper, partly by "standard arguments" (the reduction to admitted intervals) and by first-order conditions whose global optimality is argued informally; two displays in the proof of Theorem 1 are misprinted. No part of the paper has been machine-checked, and the platform has no development of discretionary services, endogenous service times or mechanism design with congestion. A complete formal proof would verify the case analysis of Theorem 1, including uniqueness in its first two cases, and the full-extraction argument, which the paper does not check for the non-negativity of prices.

Difficulty

The hard step is Theorem 1. The first-best program is a non-convex optimisation over measurable sets and functions, in which welfare involves the ratio of the second moment to the slack $\bar\theta - \Lambda\int t$. The natural approach, pointwise optimisation of the integrand, fails because every customer's time enters every other customer's waiting cost through two integrals. The paper's route goes through a reduction to intervals, a water-filling sub-problem and a three-parameter calculus problem with implicit first-order conditions, and a formal proof must justify each reduction globally, not only at stationary points. Theorem 8 on top of Theorem 1 is short, but it needs the first-best time function to leave $p \ge 0$, which follows from the optimality of the lower threshold.

Formalization scope

Everything is real-valued, in the namespace ServTimeLimit.OptMech. Parameters are a structure with fields Lam ($\Lambda$), c and θbar ($\bar\theta$), and every statement assumes $\Lambda, c, \bar\theta > 0$; $c > 0$ is made explicit. Allocations are pairs of a set Φ : Set ℝ and a function t : ℝ → ℝ of which only the values on $\Phi$ matter; integrals are Lebesgue integrals over $\Phi$.

No queueing process is modelled: the waiting time is defined by the Pollaczek–Khinchine display above, which is the paper's own formula with $\lambda E[S] = (\Lambda/\bar\theta)\int_\Phi t$. The program's condition "$W \ge 0$" is read as stability, $\Lambda\int_\Phi t < \bar\theta$, and is part of feasibility. Welfare integrates over the admitted set, as in the proof of Theorem 1 and the program of Theorem 8; §4's display over $[0, \bar\theta]$ would charge the waiting cost to customers who are not admitted. IC is stated on $\Phi \times \Phi$, as printed, and the goal adds the proof's check for excluded types. Prices must be measurable, integrable and non-negative. Uniqueness in Theorem 1 is of the threshold (and time limit) within the displayed shape; for $\Lambda \ge \Lambda_2$ the first best is not unique and no uniqueness is stated. The milestone for $\Lambda_1$ adds the stability range $\Lambda < 32/(15\bar\theta)$ at $\theta_l = \bar\theta/4$.

The goal is not Theorem 8 for an arbitrary first-best allocation: that version would drop "according to Theorem 1" and reduce to milestones 7 and 8. The goal names Theorem 1's admitted sets and time functions in each regime, so a proof must establish the first-best characterisation.

A complete development needs Lebesgue integrals over intervals, a water-filling (or convexity) argument for sub-problem (4), and one-variable calculus for the first-order conditions. The sub-problem lemma, minimising $\int t^2$ under a mean and a pointwise upper constraint, is reusable beyond this paper. Contributions of any of the milestones, or of intermediate lemmas such as the reduction to admitted intervals, are welcome.

Selected references

• P. Feldman and E. Segev, The Important Role of Time Limits when Consumers Choose their Time in Service, Management Science, 2022 (SSRN version of 2021-10-07). https://ssrn.com/abstract=3424317, DOI 10.1287/mnsc.2021.4236
• W. J. Hopp, S. M. R. Iravani and G. Y. Yuen, Operations Systems with Discretionary Task Completion, Management Science 53(1), 61–77, 2007. https://doi.org/10.1287/mnsc.1060.0598
• C. Tong and S. Rajagopalan, Pricing and Operational Performance in Discretionary Services, Production and Operations Management 23, 689–703, 2014.
• L. Debo and C. Li, Design and Pricing of Discretionary Service Lines, Management Science (forthcoming as of the 2020 citation in the paper).

Motivation

Many decision problems have set-valued outcomes rather than single numbers. Typical cases are a portfolio whose risk is a set of capital vectors, a vector optimization problem whose image is upper-bounded by an ordering cone, or a robust model whose value is the set of all achievable outcomes. Set optimization minimizes such a map $f\colon X\to\mathcal P(Z)$. The first difficulty is how to compare two sets. In the complete lattice approach of Heyde and Löhne (2011) and of the survey by Hamel, Heyde, Löhne, Rudloff and Schrage (2015), the values are taken in a complete lattice of sets, so that infima exist. A solution is then a set of arguments that attains the infimum and consists of minimal points.

Crespi, Hamel, Rocca and Schrage (arXiv:1812.03300v1, published in Mathematics of Operations Research, 2021) generate both the set relation and the lattice from an arbitrary family $\Psi$ of monotone scalar functions on a preordered set. The construction needs no linear structure on the image space. It covers vector orders, scalarizations by linear functionals and orders given by indicator functions. On top of it they define approximate solutions with tolerance $\varepsilon$, and prove a Weierstrass-type existence theorem: compactness of approximate minimizer sets yields exact solutions, and the approximate sets converge to the exact ones in the Hausdorff sense.

Setting

Let $(Z,\preceq)$ be a preordered set and $\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$. Let $\Psi$ be a family of monotone functions $\psi\colon Z\to\overline{\mathbb R}$, so that $z_1\preceq z_2$ implies $\psi(z_1)\le\psi(z_2)$.

• The inf-extension of $\psi$ is $\psi^\triangle(D)=\inf_{z\in D}\psi(z)$ for $D\subseteq Z$, with $\psi^\triangle(\emptyset)=+\infty$.
• The set relation $D_1\preceq_\Psi D_2$ holds when $\psi^\triangle(D_1)\le\psi^\triangle(D_2)$ for every $\psi\in\Psi$.
• The Ψ-hull is $\operatorname{cl}_\Psi D=\bigcap_{\psi\in\Psi}\{z\in Z\mid\psi^\triangle(D)\le\psi(z)\}$. A set is Ψ-closed when $D=\operatorname{cl}_\Psi D$, and $\mathcal P(Z,\Psi)$ denotes the family of Ψ-closed sets.
• $(\mathcal P(Z,\Psi),\supseteq)$ is a complete lattice with $\inf\mathcal A=\operatorname{cl}_\Psi\bigcup_{A\in\mathcal A}A$.

For a map $f\colon X\to\mathcal P(Z,\Psi)$ on a non-empty set $X$, the problem is

$$\text{minimize } f(x)\ \text{ over } x\in X, \tag{P}$$

and $\inf f[M]=\operatorname{cl}_\Psi\bigcup_{x\in M}f(x)$ for $M\subseteq X$. For $a\in\overline{\mathbb R}$ and $\varepsilon\ge0$, let $b(a,\varepsilon)=a+\varepsilon$ if $a\ne-\infty$ and $b(-\infty,\varepsilon)=-1/\varepsilon$, with $-1/0=-\infty$.

• An $(\varepsilon,\Psi)$-infimizer is a non-empty $M\subseteq X$ with $\psi^\triangle(\inf f[M])\le b(\psi^\triangle(\inf f[X]),\varepsilon)$ for all $\psi\in\Psi$.
• $\operatorname{Min}(f,\varepsilon,\Psi)$ is the set of $x$ for which some $\psi\in\Psi$ satisfies $\psi^\triangle(f(x))\le b(\psi^\triangle(\inf f[X]),\varepsilon)$.
• $\operatorname{Min}(f,\varepsilon+,\Psi)$ is the set of $x$ such that for every $\delta>0$ some $\psi\in\Psi$ satisfies $\psi^\triangle(f(x))\le b(\psi^\triangle(\inf f[X]),\varepsilon+\delta)$.
• An $(\varepsilon,\Psi)$-solution is an $(\varepsilon,\Psi)$-infimizer contained in $\operatorname{Min}(f,\varepsilon,\Psi)$.

In §4, $X$ is a separated (Hausdorff) topological linear space over $\mathbb R$.

Formalization targets

Goal: Theorem 4.3 (p. 23)

Let $\Psi\ne\emptyset$ and $\varepsilon_0>0$, and suppose $\operatorname{Min}(f,\varepsilon+,\Psi)$ is compact for all $0<\varepsilon\le\varepsilon_0$. Then $\operatorname{Min}(f,0+,\Psi)$ is non-empty and compact, and for every neighbourhood $U$ of $0\in X$ and all sufficiently small $\varepsilon>0$

$$\operatorname{Min}(f,\varepsilon+,\Psi)\subseteq\operatorname{Min}(f,0+,\Psi)+U,\qquad\operatorname{Min}(f,0+,\Psi)\subseteq\operatorname{Min}(f,\varepsilon+,\Psi)+U .$$

If, additionally, every $\psi^\triangle\circ f$ is lower semicontinuous, then $\operatorname{Min}(f,0,\Psi)$ is non-empty and a $(0,\Psi)$-solution of (P).

Milestones

1. Lemma 2.1: $D\preceq_\Psi E\iff\operatorname{cl}_\Psi D\supseteq\operatorname{cl}_\Psi E$, and $\psi^\triangle(\operatorname{cl}_\Psi D)=\psi^\triangle(D)$.
2. Proposition 2.2: $\operatorname{cl}_\Psi$ is a hull operator.
3. Proposition 2.3: $(\mathcal P(Z,\Psi),\supseteq)$ is a complete lattice with the stated infimum and supremum.
4. Lemma 2.4 (inf-stability): $\psi^\triangle\big(\operatorname{cl}_\Psi\bigcup_{A\in\mathcal A}A\big)=\inf_{A\in\mathcal A}\psi^\triangle(A)$.
5. Remark 3.3: monotonicity in $\varepsilon$ and $\operatorname{Min}(f,0+,\Psi)=\bigcap_{\varepsilon>0}\operatorname{Min}(f,\varepsilon,\Psi)=\bigcap_{\varepsilon>0}\operatorname{Min}(f,\varepsilon+,\Psi)$ (3.2).
6. Proposition 3.9: an $(\varepsilon,\Psi)$-solution exists for every $\varepsilon>0$.
7. Proposition 4.1: a Weierstrass theorem for $\overline{\mathbb R}$-valued functions with compact sublevel sets $L_\varphi(r)$, $\inf\varphi<r\le\bar r$.
8. Theorem 4.2: if each $\psi^\triangle\circ f$ is lower semicontinuous with a compact sublevel set above its infimum, then the points attaining some scalarized infimum form a $(0,\Psi)$-solution.

Significance

The theorem is the existence result of the paper's framework. It turns a compactness condition on approximate minimizer sets into an exact solution in the sense of Definition 3.7: a set of arguments that attains the lattice infimum and consists of minimizers. The Hausdorff convergence statement is a well-posedness result: approximate minimizers computed with a tolerance $\varepsilon$ lie close to exact $(0+,\Psi)$-minimizers when $\varepsilon$ is small. The framework applies to vector optimization with a cone order, to set-valued risk measures and to orders given by indicator functions, all as instances of the same $\Psi$.

The results are proved in the paper. None of them is formalized on the platform or in Mathlib, which has neither set relations nor lattice-valued solution concepts. This mission produces machine-checked statements of the lattice of Ψ-closed sets, inf-stability, approximate solution concepts with their $\pm\infty$ conventions, and the existence theorem. Later set optimization missions can build on these definitions.

Difficulty

The individual arguments are short. The work lies in the extended-real bookkeeping and in using the lattice structure correctly:

• Lattice infima versus scalar infima. Every scalarized statement passes through inf-stability (Lemma 2.4), which equates $\psi^\triangle(\inf f[M])$ with $\inf_{x\in M}\psi^\triangle(f(x))$. Without it, the infimizer conditions cannot be compared with the minimizer conditions.
• Three regimes of the infimum. The infimum $\psi^\triangle(\inf f[X])$ can be finite, $-\infty$ or $+\infty$, and each case needs its own argument. With $-\infty$, the tolerance is $-1/\varepsilon$. With $+\infty$, every point is a minimizer, and the paper's route through Theorem 4.2 has no real level $r_\psi$ above the infimum.
• Hausdorff convergence. Proving the upper half needs a compactness argument on the nested family $\operatorname{Min}(f,\varepsilon+,\Psi)$ in a topological vector space that need not be metrizable, so sequences do not suffice.

Formalization scope

• Types. Extended reals are Lean's EReal, and the empty infimum is $+\infty=\top$. $Z$ carries [Preorder Z], and $\Psi$ is a Set (Z → EReal) with every member monotone. A map into $\mathcal P(Z,\Psi)$ is f : X → Set Z together with the hypothesis that every value is Ψ-closed. The lattice structure is therefore Proposition 2.3, not a built-in instance.
• The lattice infimum. $\inf f[M]$ is defined as $\operatorname{cl}_\Psi\bigcup_{x\in M}f(x)$, the formula of Proposition 2.3. Infimizers are defined through this lattice infimum, never through the scalar $\inf_{x\in M}\psi^\triangle(f(x))$; that would assume Lemma 2.4.
• Minimizer sets. $\operatorname{Min}(f,\varepsilon+,\Psi)$ is defined by "for every $\delta>0$ there is $\psi$", so (3.1) and (3.2) are theorems. The convention $-1/0=-\infty$ is an explicit case, because Lean's real division gives $-1/0=0$.
• §4 setting. $X$ is an additive commutative group and a real module, with a topology making it a topological vector space, and it is Hausdorff.
• Hausdorff convergence. The paper uses the term without defining it. It is formalized as the upper and lower inclusions above for every neighbourhood $U$ of $0$, eventually as $\varepsilon\downarrow0$, which is the reading the proof of Theorem 4.3 uses.
• Added hypotheses. $\Psi\ne\emptyset$ is added to Proposition 3.9 and Theorems 4.2 and 4.3: for $\Psi=\emptyset$ all minimizer sets are empty and the existence claims fail. Proposition 4.1 receives $\inf\varphi<\bar r$, without which the compactness hypothesis can be vacuous and the conclusion false. Lemma 2.1 (c) is stated for $\psi\in\Psi$.
• Ruled-out trivialization. A formalization that defines $\operatorname{Min}(f,0+,\Psi)$ as an intersection, or Hausdorff convergence as eventual equality of the sets, would make half of the goal definitional; neither is done.

The development needs extended-real infima, lower semicontinuity into EReal, and Cantor's intersection theorem for nested compact sets in Hausdorff spaces, all available in Mathlib. The definitions of inf-extension, Ψ-hull, set relation and approximate solutions are reusable beyond this paper. Proofs of any milestone, and of alternative routes to the goal, are welcome.

Selected references

• G. P. Crespi, A. H. Hamel, M. Rocca, C. Schrage, Set Relations via Families of Scalar Functions and Approximate Solutions in Set Optimization, Mathematics of Operations Research, 2021; preprint Set Relations and Approximate Solutions in Set Optimization, arXiv:1812.03300v1, 2018. https://arxiv.org/abs/1812.03300
• F. Heyde, A. Löhne, Solution concepts in vector optimization: a fresh look at an old story, Optimization 60(12), 1421–1440, 2011.
• A. H. Hamel, F. Heyde, A. Löhne, B. Rudloff, C. Schrage, Set optimization — a rather short introduction, in: Set Optimization and Applications — the State of the Art, Springer, 2015, pp. 65–141.
• A. Löhne, Vector Optimization with Infimum and Supremum, Springer, 2011.

Recommendations, reputation and the shape of a labor market

Hiring decisions often rest on a recommendation from someone who knows the candidate: a thesis adviser, a former supervisor, a colleague. Referrals are a common channel of labor market matching, and their value depends on whether the recommender can be trusted. An adviser who cares about his candidate has a reason to overstate the candidate's quality, and the main check on this is the adviser's reputation: a recommendation that turns out badly costs the adviser future credibility.

Câmara, Jia and Raffiee (2023) study this trade-off in a one-period recommendation game in which reputation enters as a state variable, and ask a question about matching between advisers and firms: which firms are more likely to hire the candidates of strong-reputation advisers? Their answer is that it depends on the shape of the firm's outside market, not only on its average quality. This mission formalizes that result, together with the equilibrium characterization it rests on.

The recommendation game

A focal candidate has skill $s \in \{s_L, s_H\}$, $0 < s_L < s_H < 1$, high with probability $p \in (0,1)$; the average skill is $\hat s = p\,s_H + (1-p)\,s_L$. An adviser with reputation $r > 0$ privately observes $s$ and a personal bias $b$, distributed on $[0,1]$ with a continuous CDF $Z$ of full support. He sends a message $m \in \{R, NR\}$ (recommend or not). A firm privately observes the value $x$ of an outside candidate, distributed on $[0,1]$ with a continuously differentiable CDF $F$, density $f$ and full support, and hires either the focal candidate (payoff equal to the candidate's skill) or the outside one (payoff $x$).

If the adviser recommends a high-skilled candidate who is hired, his reputation rises to $r + g(r)$; if he recommends a low-skilled candidate who is hired, it falls to $r - c(r)$, with $c(r) \in (0,r)$; otherwise it stays at $r$. He receives the reputation payoff $v(\tilde r)$ of his final reputation, plus $b$ if his candidate is hired. The payoff loss from an unsuccessful hire is

$$L(r) = v(r) - v\big(r - c(r)\big),$$

and the paper's standing Assumption (A1) is $L'(r) > 0$: an adviser with a higher reputation has more to lose. The solution concept is perfect Bayesian equilibrium with two tie-breaks: an indifferent firm hires the focal candidate, and an indifferent adviser does not recommend a low-skilled candidate.

In equilibrium a low-skilled adviser lies (recommends) exactly when his bias exceeds a threshold $b^* \in (0,1]$, and the firm's belief after a recommendation is

$$s_R(b^*) = \frac{p\,s_H + (1-p)(1-Z(b^*))\,s_L}{p + (1-p)(1-Z(b^*))}.$$

The largest possible benefit from lying is $\bar B = [F(s_H) - F(s_L)]/F(s_H)$. A market is top-heavy if $f$ is strictly increasing, and bottom-heavy if $f$ is strictly decreasing.

Formalization targets

Goal: Proposition 3 (i)–(ii)

Let $E_r[F(s_m)]$ be the ex-ante probability that the firm hires the focal candidate in an equilibrium at reputation $r$. For all $0 < r \le r'$ and all equilibria at $r$ and $r'$:

$$\text{top-heavy: } E_r[F(s_m)] \le E_{r'}[F(s_m)], \qquad \text{bottom-heavy: } E_{r'}[F(s_m)] \le E_r[F(s_m)],$$

and both inequalities are strict when $r < r'$ and $L(r) < \bar B$. Part (iii) of the proposition, assortative matching, is (i)–(ii) restated.

Milestones

1. Eq. (11): Bayes' rule gives $s_R(b^*)$, which is strictly increasing and continuous in $b^*$.
2. Eq. (9): the low-skilled adviser's lying condition $b\,[F(s_R) - F(s_{NR})]/F(s_R) > L(r)$.
3. Eqs. (12)–(13): the benefit from lying at the threshold is strictly increasing, with maximum $\bar B$, and the interior threshold is unique.
4. Proposition 1: existence, uniqueness and threshold form of the equilibrium.
5. Proposition 2 (first sentence): the probability of lying decreases in $r$.
6. Eq. (14): the message is a fair gamble on beliefs with mean $\hat s$, and $E[F(s_m)]$ is its expected value under $F$.
7. Top-heavy implies $F$ strictly convex; bottom-heavy implies $F$ strictly concave.
8. A mean-preserving spread of the fair gamble raises $E[F(s_m)]$ under strictly convex $F$ and lowers it under strictly concave $F$.

Significance

The result separates two notions of a firm's "strength" that are often conflated: the average quality of its outside options and the shape of their distribution. Two firms with the same average outside candidate can respond in opposite ways to an adviser's reputation. Firms with access to many strong outside candidates (top-heavy) favor candidates of high-reputation advisers; firms whose outside options are concentrated at the bottom favor candidates of low-reputation advisers. The paper uses this to explain assortative matching between strong advisers and strong firms without assuming it, and connects it to the persuasion literature, where the convexity of the sender's payoff in the receiver's posterior determines how much information the sender wants to reveal (Kamenica and Gentzkow 2011).

All results here are proved in the paper, in Appendix A. None of them has a machine-checked proof. A formal development makes precise several points the prose leaves implicit: what "increasing" means where the adviser's behavior stops responding to reputation, that the comparison holds for every equilibrium and not only for a constructed profile, and which regularity of $F$ the shape definitions need.

Difficulty

The obvious argument treats the threshold $b^*$ as a known function of $r$ and differentiates. Two steps break this. First, $b^*$ is defined implicitly by a fixed-point condition that couples the adviser's incentive with the firm's Bayesian belief, which itself depends on $b^*$; existence and uniqueness of the equilibrium, and the threshold form of every equilibrium (not merely of one candidate profile), have to be established before any comparative static makes sense. Second, the hiring probability is not monotone in $b^*$ for every $F$: a higher threshold makes a recommendation more persuasive but rarer, and the two effects cancel exactly for linear $F$. The sign is decided only by the curvature of $F$, which enters through its density, so the definition of top- and bottom-heavy markets has to be related to convexity of the CDF on the support. A further subtlety is that the hiring probability is constant for reputations at which the adviser never lies, so the monotonicity is strict only from reputations with $L(r) < \bar B$.

Formalization scope

All quantities are real numbers. The laws of the bias and of the outside option are probability measures $\mu_B$, $\mu_X$ on $\mathbb R$ with mass one on $[0,1]$, no atoms and strictly increasing CDFs on $[0,1]$; $Z$ and $F$ are their CDFs, $F$ is $C^1$ on $[0,1]$ (not on all of $\mathbb R$, which would force $f(1) = 0$ and rule out top-heavy markets), and $f$ is the derivative of $F$ on $(0,1)$. The functions $v$, $g$, $c$ are differentiable on $(0,\infty)$, and (A1) is stated as $L' > 0$ there.

Strategies are pure and Boolean-valued: $\sigma_A(b, s)$ for the adviser and $\sigma_F(x, m)$ for the firm, as in the paper's footnotes 15–16. They are required to be measurable, which the paper leaves implicit; message and hiring probabilities are measures of the corresponding sets. Best responses are imposed for every bias in $[0,1]$ and every outside value in $[0,1]$, so uniqueness in Proposition 1 is on those supports. Beliefs lie in $[s_L, s_H]$ and follow Bayes' rule after every message sent with positive probability. The adviser's expected utilities are eqs. (6)–(8), with $v(r + g(r))$ in (7); the sentence leading into (7) misprints it as $v(1 + g(r))$.

"Increasing in $r$" in Propositions 2 and 3 is formalized as weakly monotone on $(0,\infty)$ together with strict monotonicity from every $r$ with $L(r) < \bar B$; strict monotonicity on all of $(0,\infty)$ is false. The goal quantifies over arbitrary equilibrium profiles at both reputations: a statement about the threshold $b^*(r)$ or about a profile the theorem itself constructs would reduce the goal to milestones 1, 5 and 8 and is ruled out. The standing assumptions are satisfiable together with a top-heavy market (for instance $F(x) = x^2$ on $[0,1]$ with uniform bias).

The development needs only Mathlib's measure theory (CDFs from measures), one-variable calculus (monotonicity from the sign of a derivative, convexity from a monotone derivative) and slope inequalities for convex functions. The general facts in milestones 7 and 8 are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Proposition 1.

Not formalized here: the second sentence of Proposition 2 (the firm's ex-ante payoff increases in $r$), Proposition 4 (the low-reputation trap), Propositions 5 and 6, and the extensions of §5.

Selected references

• O. Câmara, N. Jia, J. Raffiee, Reputation, Competition, and Lies in Labor Market Recommendations, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4654 (cited from the authors' manuscript of September 26, 2022)
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590

Motivation

Many combinatorial optimization problems are linear programs over a polytope with exponentially many facets, and one way to solve them by a polynomial-size linear program is to write the polytope as the projection of a higher-dimensional polytope with few facets. The minimum number of facets needed is the extension complexity of the polytope. It is now understood for most textbook polytopes: flows, matchings (Rothvoß 2017), arborescences, travelling-salesman tours and stable sets (Fiorini et al. 2015). Matroids are a notable exception.

For a matroid $M$, the independence polytope $P(M)$ is the convex hull of the characteristic vectors of the independent sets. Rothvoß showed by a counting argument that many matroids have independence polytopes of exponential extension complexity (Math. Program. 2013), so a polynomial bound can only hold for special classes. Regular matroids, those representable over every field, are the natural class: they contain the graphic and cographic matroids, and Seymour's decomposition theorem describes all of them.

Timeline:

• 1980, 1991. Wong (Proc. IEEE Int. Conf. Circuits and Computers, 1980) and Martin (Oper. Res. Lett. 1991) give extended formulations of size $O(|V(G)|\cdot|E(G)|)$ for the spanning tree polytope of a graph $G$. This gives $\mathrm{xc}(P(M)) = O(n^2)$ for graphic and cographic matroids on $n$ elements.
• 1980. Seymour (J. Combin. Theory Ser. B) proves that every regular matroid is built by 1-, 2- and 3-sums from graphic matroids, cographic matroids and copies of a 10-element matroid $R_{10}$.
• 2017. Two preprints claim an $O(n^2)$ and an $O(r\cdot n)$ bound for all regular matroids (e.g. Gurjar and Vishnoi, arXiv:1701.00538); both were withdrawn.
• 2019. Aprile and Fiorini (arXiv:1909.08539) prove the first polynomial bound, $O(n^6)$.

Setting

A matroid $M$ has a finite ground set $E(M)$ and a family $\mathcal I(M)$ of independent sets; $n = |E(M)|$. For $I \subseteq E(M)$, $\chi^I \in \{0,1\}^{E(M)}$ is its characteristic vector, and

$$P(M) = \operatorname{conv}\{\chi^I \mid I \in \mathcal I(M)\} \subseteq \mathbb R^{E(M)} .$$

An extended formulation of a set $P \subseteq \mathbb R^d$ of size $r$ is a system $E^{=}x + F^{=}y = g^{=}$, $E^{\le}x + F^{\le}y \le g^{\le}$ with exactly $r$ inequalities such that $x \in P$ if and only if some $y$ satisfies the system. The extension complexity $\mathrm{xc}(P)$ is the least such $r$. The paper defines $\mathrm{xc}(P)$ as the minimum number of facets of a polytope projecting onto $P$, and on p. 1 it gives the extended-formulation form as an equivalent definition.

A matroid is regular if it is represented over $\mathbb R$ by a totally unimodular matrix $A$: a set is independent exactly when the corresponding columns of $A$ are linearly independent. It is binary if it is represented over $\mathrm{GF}(2)$. It is graphic if it is the cycle matroid $M(G)$ of a multigraph $G$ (independent sets are forests) and cographic if its dual is graphic. A cycle is a disjoint union of circuits. For binary $M_1, M_2$, the sum $M_1 \Delta M_2$ has ground set $E(M_1) \Delta E(M_2)$, and its cycles are the sets $C_1 \Delta C_2$, with $C_i$ a cycle of $M_i$, that lie in that ground set. This sum is a 1-, 2- or 3-sum when the two ground sets share zero, one or three elements, under the side conditions of p. 3. In the 3-sum case the shared set is a triangle, a 3-element circuit of both parts. A matroid is 3-connected if it is neither a 1-sum nor a 2-sum.

Formalization targets

Goal: Theorem 1

$$\exists\, c_0\ \ \forall M \text{ regular on } n \text{ elements}:\qquad \mathrm{xc}(P(M)) \le c_0 \cdot n^6 .$$

The constant is not fixed; the exponent is the paper's. Section 8 of the paper sketches an improvement to $O(n^{6-\varepsilon})$ without proof, so the goal keeps the proved exponent.

Milestones

• the graphic/cographic base case $\mathrm{xc}(P(M)) = O(n^2)$ (Wong, Martin) and the trivial bound $\mathrm{xc}(P(M)) \le 2^n$;
• Lemma 3: $\mathrm{xc}(P(M_1 \oplus_t M_2)) \le \mathrm{xc}(P(M_1)) + \mathrm{xc}(P(M_2))$ for $t \in \{1, 2\}$;
• Lemma 8 (an inequality for convex functions) and Lemma 7 (a balanced node in a weighted tree);
• Theorem 6: a 3-connected regular matroid other than $R_{10}$ is a tree of 3-sums of graphic and cographic matroids;
• Proposition 27: the tree can be chosen without bad nodes, so that every triangle of a cographic, non-graphic label $M^*(G_v)$ is the set of edges at a degree-3 node of $G_v$;
• Lemma 4: such a matroid has a star decomposition $M \overset{\star}{=} M_0 \oplus_3 M_1 \oplus_3 \cdots \oplus_3 M_k$ with $M_0$ graphic or cographic, $1 \le k \le n/4$ and $|E(M_i)| \le n/2 + 3$;
• Proposition 12: $\mathrm{xc}(\operatorname{conv}\bigcup_i P_i) \le \sum_i \mathrm{xc}(P_i)$ for polytopes of dimension at least 1;
• Proposition 15: $\mathrm{xc}(P(M)) \le \mathrm{xc}(P_{T_1,\dots,T_k}(M_0), Q_{T_1,\dots,T_k}(M_0)) + 16 \sum_{i=1}^k \mathrm{xc}(P(M_i))$, where $P_{T_1,\dots,T_k}(M_0) \subseteq Q_{T_1,\dots,T_k}(M_0)$ are two polytopes attached to the centre $M_0$ and its triangles (p. 7), and the extension complexity of the pair is the least $\mathrm{xc}(R)$ over polytopes $R$ between them;
• Propositions 16 and 18: that pair has extension complexity $O(|V(G)|\cdot|E(G)|)$ when $M_0 = M(G)$ is graphic, and when $M_0 = M^*(G)$ is cographic with every triangle the set of edges at a degree-3 node;
• Lemma 5: $\mathrm{xc}(P(M)) \le c_1 |E(M_0)|^2 + 16 \sum_{i=1}^k \mathrm{xc}(P(M_i))$ for a star decomposition.

Significance

The result. Theorem 1 shows that linear optimization over the independent sets of any regular matroid is a linear program of size polynomial in $n$, written down without any algorithm. Regular matroids are the largest classical matroid class for which such a bound was in question, and the bound separates them from general binary matroids. The proof also gives an $O(n^2)$ extended formulation for the circuit dominant of a regular matroid, a separate result that this mission does not include.

Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs a Lean theory of matroid sums (1-, 2- and 3-sums defined through cycle spaces), decompositions of regular matroids along trees, and extended formulations, with explicit bounds on how the size of an extended formulation behaves under products, intersections with hyperplanes and convex hulls of unions. Seymour's decomposition theorem enters only through Theorem 6, which can be taken as a black box while the polyhedral part is formalized.

Difficulty

The obvious induction fails at 3-sums. For 1- and 2-sums, the extension complexities of the parts add (Lemma 3), and an induction gives a polynomial bound. For a 3-sum, the best known symmetric formulation for $P(M_1 \oplus_3 M_2)$ has size $c\,(\mathrm{xc}(P(M_1)) + \mathrm{xc}(P(M_2)))$ with $c = 4$ (p. 4). A constant larger than 1 compounded over a decomposition tree of logarithmic depth only gives a quasi-polynomial bound, and over an unbalanced tree an exponential one. So the parts of a 3-sum have to be treated differently, and the decomposition tree has to be rebalanced into a star whose leaves have at most about half the elements.

The cographic centre is a second obstacle: the formulation of the centre's part is known only when every triangle shared with a leaf is the set of edges at a degree-3 node of the underlying graph, and getting there requires the decomposition tree of Proposition 27.

Formalization scope

• Matroids are Mathlib Matroid α over one ambient type $\alpha$; the parts of a sum share elements of $\alpha$ (the triangle elements) that are not in $E(M)$. Statements that construct decompositions (Theorem 6, Proposition 27, Lemma 4) take $\alpha$ infinite, so that fresh elements exist; otherwise "not a 2-sum" could hold for want of room.
• $P(M)$ lives in $\mathbb R^{E(M)}$, coordinates indexed by the subtype of the ground set; $n$ is the number of elements of $E(M)$.
• Extended formulations and extension complexity are the published platform definitions IsEFOfSize and extensionComplexity (size = number of inequalities, equations free). Every upper bound is the existence of an extended formulation of the stated size, and bounds in terms of the parts quantify over extended formulations of the parts. This rules out the trivializing reading $\mathrm{xc}(P) \le B$ with $\mathrm{xc}$ an infimum that is $0$ on sets with no extended formulation.
• Regular means represented over $\mathbb R$ by a totally unimodular matrix; graphic means represented by the oriented incidence matrix of a finite multigraph (loops and parallel edges allowed); cographic means the dual is graphic. $R_{10}$ is not printed in the paper; it is fixed as the column matroid over $\mathrm{GF}(2)$ of $[I_5 \mid A]$ with $A$ the circulant with rows $11001, 11100, 01110, 00111, 10011$, and "is $R_{10}$" means isomorphic to it.
• Sums are defined through cycles exactly as on p. 3, with every side condition (binary parts, sizes at least 3 or 7, no loops or coloops at the 2-sum element, the triangle a circuit of both parts and containing no cocircuit). "3-connected" is "neither a 1-sum nor a 2-sum".
• The pair polytopes live in $\mathbb R^{E_0} \times \mathbb R^{T_1} \times \mathbb R^{T_1} \times \cdots \times \mathbb R^{T_k} \times \mathbb R^{T_k}$, with the elements of each triangle named $\alpha_i, \beta_i, \gamma_i$ as in the paper. The bound of the pair is stated as the existence of a set between the two polytopes together with an extended formulation of the stated size. Propositions 16 and 18 take the graph as a finite vertex type with a tail and a head for every element.
• Lemma 4 carries one clause that the printed statement does not have: if $M_0$ is not graphic, each triangle is the set of edges at a degree-3 node of a connected graph $G$ with $M_0 = M^*(G)$. Section 6 assumes this and justifies it by Proposition 27; Lemma 5 is stated under the same clause and under the paper's standing assumption that matroids have no loops. The goal itself allows loops.
• Needed infrastructure, reusable beyond this mission: matroid sums and their cycle spaces; the independence polytope and its behaviour under sums; extended formulations of products, of intersections with affine subspaces and of convex hulls of unions; a flow formulation of the spanning tree polytope. Contributions of proofs of any milestone, and of the parts of the paper not posed here (Propositions 13 and 14, the set description (3) in Proposition 15, the polytopes $R_{T_1,\dots,T_k}(M_0)$ of Sections 5 and 6, Lemma 17), are welcome.

Selected references

• M. Aprile and S. Fiorini, Regular matroids have polynomial extension complexity, arXiv:1909.08539v2, 2019; Mathematics of Operations Research 47(1), 2022. https://arxiv.org/abs/1909.08539
• P. D. Seymour, Decomposition of regular matroids, Journal of Combinatorial Theory, Series B 28(3), 305–359, 1980. https://doi.org/10.1016/0095-8956(80)90075-1
• R. K. Martin, Using separation algorithms to generate mixed integer model reformulations, Operations Research Letters 10(3), 119–128, 1991. https://doi.org/10.1016/0167-6377(91)90028-N
• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary and R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, Journal of the ACM 62(2), Article 17, 2015. https://doi.org/10.1145/2716307
• T. Rothvoß, The matching polytope has exponential extension complexity, Journal of the ACM 64(6), Article 41, 2017. https://doi.org/10.1145/3127497
• T. Rothvoß, Some 0/1 polytopes need exponential size extended formulations, Mathematical Programming 142(1–2), 255–268, 2013. https://doi.org/10.1007/s10107-012-0574-3
• R. T. Wong, Integer programming formulations of the traveling salesman problem, Proceedings of the IEEE International Conference of Circuits and Computers, 149–152, 1980 (no DOI).