Algorithmic Game Theory

Motivation

Platform markets often feature a Superstar: a single complement whose presence moves consumers, such as a blockbuster game on a console or a star streamer on a video platform. Whether such a Superstar signs an exclusive deal with one platform or stays available on both is a recurring question for competition authorities and for platform managers. Empirical work documents both sides of the effect. Exclusive titles help small consoles challenge incumbents (Lee 2013). Superstar apps generate demand-discovery spillovers for small developers (Ershov 2020, NET Institute working paper). When a star streamer switched platforms, viewers followed and other content producers repositioned (Förderer & Gutt 2021, working paper).

Carroni, Madio & Shekhar (Management Science, 2024) build a two-sided Hotelling model with three groups of agents: consumers, a fringe of small complementors, and the Superstar. The model asks how Superstar exclusivity changes prices, participation and welfare. This mission formalizes the paper's analysis of the complementor side under vertical separation. The analysis runs through the equilibrium prices (Lemmas 1–3) and the sorting of complementors into multihomers, singlehomers and inactive firms (Proposition 1). It ends in the welfare result that exclusivity raises complementors' total surplus (Proposition 3).

Setting

Two platforms $1$ and $2$ sit at the ends of a Hotelling line. A unit mass of consumers has types $m\in[-\bar m,\bar m]$, distributed with cumulative distribution function $F$ and density $f$. The type $m$ measures the preference for platform $2$ over platform $1$. The Superstar is worth $\phi$ to a consumer of a platform that hosts it, and $g_i\in\{0,1\}$ records its presence on platform $i$. A consumer of type $m$ joins platform $1$ rather than $2$ when

$$m\le \tilde m=\phi(g_1-g_2)-(p_1-p_2)+\theta(N_1-N_2),$$

where $p_i$ are the consumer prices, $N_i$ the masses of complementors on the platforms, and $\theta>0$ the value of a unit mass of complementors to a consumer. Platform $1$'s consumer share is $D=F(\tilde m)$ and platform $2$'s is $1-D$.

Complementors have an opportunity cost $k\ge0$ of joining each platform, distributed with mass function $\Lambda$ and density $\lambda$. A complementor receives $\gamma>0$ per unit mass of consumers, so it joins platform $i$ if and only if $k\le\gamma D_i$, and $N_i=\Lambda(\gamma D_i)$. A complementor that joins both platforms pays $k$ twice.

Expectations are fulfilled: the share $D$ solves the fixed-point equation

$$D=F\bigl(\phi(g_1-g_2)-(p_1-p_2)+\theta[\Lambda(\gamma D)-\Lambda(\gamma(1-D))]\bigr).$$

Platforms choose prices simultaneously to maximise gross profit $p_iD_i$. Under exclusivity the Superstar is on platform $1$ only ($g=(1,0)$); under non-exclusivity it is on both ($g=(1,1)$). The paper's standing assumptions are smoothness and symmetry of $F$, a positive nondecreasing density $\lambda$, and Assumption 3: $f\gamma\theta[\lambda(\gamma F)+\lambda(\gamma(1-F))]<1$, which keeps cross-group externalities below the differentiation parameter. The complementors' total surplus at shares $(D_1,D_2)$ is

$$FS(D_1,D_2)=\int_0^{\gamma D_1}(\gamma D_1-k)\lambda(k)\,dk+\int_0^{\gamma D_2}(\gamma D_2-k)\lambda(k)\,dk .$$

Formalization targets

Goal: Proposition 3

For $\phi>0$, let $D(\phi)$ be platform $1$'s share in the selected exclusivity equilibrium and $E$ the share in the symmetric non-exclusive equilibrium. Then

$$FS\bigl(E,1-E\bigr)<FS\bigl(D(\phi),1-D(\phi)\bigr).$$

The statement fixes no functional forms and no constants. It holds for every model satisfying the assumptions and every $\phi>0$.

Milestones

1. Lemma 1. At every interior equilibrium, $p_1=F(m^\star)\{1/f(m^\star)-\gamma\theta[\lambda(\gamma D_1)+\lambda(\gamma D_2)]\}$, and $p_2$ is the same expression with $1-F(m^\star)$ in place of $F(m^\star)$.
2. Lemma 2. Under non-exclusivity at equal prices, $D=\tfrac12$, $m^\star=0$ and $p=1/(2f(0))-\gamma\theta\lambda(\gamma/2)$. All active complementors multihome.
3. Lemma 3 (demand and complementor part). Under exclusivity, $D^\star_1(1,0)>D^\star_2(0,1)$ and $\Lambda(\gamma D^\star_1)>\Lambda(\gamma D^\star_2)$.
4. Proposition 1. Under exclusivity, complementors with $k\in(0,\gamma D^\star_2]$ multihome, those with $k\in(\gamma D^\star_2,\gamma D^\star_1]$ singlehome on platform $1$, and the rest are inactive. More complementors are active than under non-exclusivity.
5. Decomposition of $\Delta FS$ (Section 4.3) into the contributions of multihomers, of switchers from multihoming to singlehoming, and of entrants.

Significance

The result says that a Superstar's exclusive contract, usually discussed as a tool of foreclosure against the rival platform, benefits the fringe of complementors taken as a whole. Some complementors stop paying for a second platform. Others, inactive without exclusivity, enter on the favoured platform. The comparison feeds into the paper's welfare analysis (consumer surplus, Proposition 4) and into its account of when the Superstar chooses exclusivity (Proposition 5). It supplies a theoretical counterpart to the empirical spillover findings cited above.

The paper's proofs are informal in places that matter. Equilibrium selection under fulfilled expectations is described in words only, and the derivative argument for Lemma 3 tracks an equilibrium as a function of $\phi$ without saying which one. A formal development has to fix these choices, and this mission fixes them explicitly (see Formalization scope). None of these results has been machine-checked before. The fixed-point and first-order machinery for two-sided fulfilled-expectations demand would also serve other platform-competition models in the Armstrong (2006) tradition.

Difficulty

The surplus comparison itself is elementary once the equilibrium shares are known. The work lies in the equilibrium shares. Fulfilled-expectations demand is defined by a fixed point that can have several solutions, so neither the share at a deviation price nor the equilibrium share is a priori a function of prices. The obvious first step, "impose symmetry", does not prove that the non-exclusive share is $\tfrac12$. One must show that $\tfrac12$ is the only interior fixed point at equal prices. Likewise, the exclusive share exceeds $\tfrac12$ only for the equilibrium reached continuously from the symmetric one. Coordination on the disfavoured platform is a fulfilled-expectations outcome the model does not exclude. Lemma 1 needs a differentiable local branch of the fixed point at a deviation, which is where Assumption 3 enters.

Formalization scope

Everything is real-valued. The model is a structure with $\bar m,\gamma,\theta>0$, functions $F,f,\Lambda,\lambda:\mathbb R\to\mathbb R$, and the following hypotheses:

• $F$ is continuous and monotone, $0$ left of $-\bar m$ and $1$ right of $\bar m$, $C^2$ with $F'=f>0$ on $(-\bar m,\bar m)$, and symmetric, $F(-x)=1-F(x)$;
• $\Lambda(0)=0$, $\Lambda$ is $C^2$ with $\Lambda'=\lambda$, and $\lambda>0$ is nondecreasing on $[0,\gamma]$;
• Assumption 3 holds on $(-\bar m,\bar m)$.

Several conventions depart from the paper's wording:

• The paper asks for $\lambda>0$, $\lambda'\ge0$ on all of $[0,\infty)$ for a distribution function $\Lambda$, which no distribution satisfies. These conditions are imposed on $[0,\gamma]$, the only range on which $\Lambda$ is evaluated.
• The bounds on $f'$ in Assumption 2 are dropped, which only strengthens the statements.
• "$\bar m$ large enough" is replaced by interiority ($0<D<1$) of every equilibrium considered.
• The standalone value $v$ cancels and is omitted.

Fulfilled-expectations demand is a relation, not a chosen function. A price equilibrium is a Nash equilibrium in prices in which no deviation is profitable for any fulfilled-expectations share it induces. Lemma 1's formulas are a theorem about this equilibrium, not its definition. The symmetric non-exclusive outcome is the interior equilibrium at equal prices. The exclusive outcome is the end point, at value $\phi$, of a continuous path of interior equilibria of the games with Superstar value $t\in[0,\phi]$, starting from equal prices at $t=0$. Platform $2$'s share is always $1-D$.

The goal must not be posed with $D(\phi)>\tfrac12$, $D(\phi)\ne\tfrac12$ or $E=\tfrac12$ as a hypothesis: since $D\mapsto FS(D,1-D)$ is strictly convex and symmetric about $\tfrac12$, any of these would reduce it to a calculus exercise. The price ranking in Lemma 3 is not part of the mission. Its proof rests on bounds on $f'$ that the paper states only as functions of unspecified equilibrium arguments.

The needed infrastructure is the implicit function theorem in one variable, interval integrals of continuous functions, and the intermediate value theorem. Contributions are welcome on any milestone, on alternative proofs of the goal, and on reusable lemmas about uniqueness of fulfilled-expectations fixed points.

Selected references

• Carroni, E., Madio, L., Shekhar, S., Superstar Exclusivity in Two-Sided Markets, Management Science 70(2):991–1011, 2024; accepted manuscript at IRIS Bologna. https://doi.org/10.1287/mnsc.2023.4720, http://hdl.handle.net/11585/922035
• Armstrong, M., Competition in Two-Sided Markets, RAND Journal of Economics 37(3):668–691, 2006. https://doi.org/10.1111/j.1756-2171.2006.tb00037.x
• Fudenberg, D., Tirole, J., Customer Poaching and Brand Switching, RAND Journal of Economics 31(4):634–657, 2000. https://doi.org/10.2307/2696352
• Lee, R. S., Vertical Integration and Exclusivity in Platform and Two-Sided Markets, American Economic Review 103(7):2960–3000, 2013. https://doi.org/10.1257/aer.103.7.2960
• Ershov, D., Competing with Superstars in the Mobile App Market, NET Institute Working Paper, 2020.
• Förderer, J., Gutt, D., The Effects of Platform Superstars on Content Production: Evidence from Ninja, working paper, 2021.

Motivation

Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.

Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega) \subseteq \mathbb{R}^{\Omega}$ the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior $\mu^* \in \Delta(\Omega)$. The receiver chooses an action from a finite nonempty set $A$. Her utility is an arbitrary function $\rho : \Delta(\Omega) \times A \to \mathbb{R}$; the sender's utility is $v : \Omega \times A \to \mathbb{R}$.

For each action $a$, the beliefs at which $a$ is optimal for the receiver form the set

$$P_a = \{\mu \in \Delta(\Omega) : a \in \arg\max_{a' \in A} \rho(\mu, a')\}.$$

The paper assumes throughout (Assumption 1) that every $P_a$ is closed.

A signaling scheme consists of a measurable signal space $S$ and a probability measure $\pi$ on $\Omega \times S$ whose $\Omega$-marginal is $\mu^*$. After signal $s$ the receiver holds the posterior $\mu_s \in \Delta(\Omega)$ given by Bayes' rule, and plays an optimal strategy $a(\cdot)$, with $a(s) \in \arg\max_a \rho(\mu_s, a)$, that is $\mu_s \in P_{a(s)}$. The sender's persuasion problem (3) is to maximize $\mathbb{E}_\pi[v(\bar\omega, a(\bar s))]$ over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.

A probability measure $\eta$ on $\Delta(\Omega)$ is Bayes-plausible if its mean is the prior: $\mathbb{E}_\eta[\bar s] = \mu^*$.

Formalization targets

Goal: Theorem 1

The sender's problem (3) can be optimized by solving the convex program

$$\max_{\{t_a : a \in A\}} \sum_{\omega \in \Omega} \sum_{a \in A} t_a(\omega)\, v(\omega,a) \quad \text{s.t.} \quad \sum_{a \in A} t_a(\omega) = \mu^*(\omega)\ (\omega \in \Omega), \qquad t_a \in \operatorname{Conv}(P_a \cup \{0\})\ (a \in A). \qquad (7)$$

It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.

Milestones

1. Lemma 1 (Aumann–Maschler, Kamenica–Gentzkow): schemes whose signals are beliefs and satisfy $\mu_s = s$ correspond to Bayes-plausible measures.
2. Lemma 5: the belief-recommendation problem (4) is equivalent to problem (14) over Bayes-plausible measures.
3. Lemma 2: a Bayes-plausible measure and an optimal strategy give action probabilities $b_a \in [0,1]$ and mean-posteriors $m_a \in \operatorname{Conv}(P_a)$ with $\sum_a b_a m_a = \mu^*$ and the same sender value; the converse also holds.

Further result: Theorem 2

Let $\Upsilon_a$ be the states at which $a$ is sender-optimal, assume these sets partition $\Omega$, and set $t^*_a = \mu^* \mathbb{1}_{\Upsilon_a}$. Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if $t^*$ is feasible for (7), i.e. $t^*_a \in \operatorname{Conv}(P_a \cup \{0\})$ for all $a$.

Significance

The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has $|A|$ vector variables in $\mathbb{R}^{\Omega}$, each in a convex set that depends only on the receiver's utility. Its variable $t_a(\omega)$ is the joint probability of state $\omega$ and action $a$. The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing $\operatorname{Conv}(P_a \cup \{0\})$ by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each $P_a$ is convex, and (7) reduces to the familiar obedience-constrained linear program.

Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).

Difficulty

The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in $P_a$ can produce a belief outside $P_a$, since $P_a$ need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex $P_a$ to a finite-dimensional variable in $\operatorname{Conv}(P_a \cup \{0\})$. The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.

Formalization scope

• Representation. $\Omega$ and $A$ are Fintypes, $A$ nonempty, and $\Omega$ carries a measurable space in which singletons are measurable. Beliefs are functions $\Omega \to \mathbb{R}$ in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, $\operatorname{Conv}$ is convexHull ℝ, and $0$ is the zero function. $\rho$ is a function on $\mathbb{R}^{\Omega}$, used only on the simplex.
• Signal spaces in (3) range over all measurable types. A scheme is a probability measure on $\Omega \times S$ with $\pi(\{\omega\} \times S) = \mu^*(\omega)$.
• Posteriors are any version of Bayes' rule: simplex-valued for every signal, measurable, and satisfying $\pi(\{\omega\} \times B) = \int_B \mu_s(\omega)\,\pi_S(ds)$. Quotients $\pi(\omega,s)/\sum_{\omega'} \pi(\omega',s)$ with Lean's $x/0 = 0$ are not used. "$\mu_s = s$" (Lemmas 1 and 5) means the identity is such a version, an almost-sure statement; the paper's "for all $s$" in Lemma 1's converse is proved only almost surely.
• Strategies are measurable (each event $\{a(\bar s) = b\}$ is measurable) and optimal at every signal. The sender's value is not computed with a fixed tie-breaking rule, so sender-preferred selection is kept.
• Assumption 1 is a hypothesis of every statement that involves $\rho$.
• Corrections to Lemma 2. If some $P_a$ is empty, $\operatorname{Conv}(P_a)$ is empty and the printed forward direction fails, so $m_a$ is left free there; then $b_a = 0$ necessarily. The printed converse fails for pure strategies when two actions must share a posterior, so it is stated for optimal mixed strategies, which the paper allows on p. 11.
• Ruled out: quantifying (3) only over belief signals with $\mu_s = s$ would turn Theorem 1 into Lemmas 5 and 2 and drop the coalescence step. The goal therefore quantifies over arbitrary signal spaces. Stating only "the optimal values are equal" through a real supremum would also be weaker, and is not done.
• Infrastructure needed: means of probability measures on compact sets in $\mathbb{R}^n$ lying in the convex hull (Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on $\Omega \times S$, and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.

Selected references

• J. Anunrojwong, K. Iyer, D. Lingenbrink, Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2208.03758v3
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Bergemann, S. Morris, Bayes Correlated Equilibrium and the Comparison of Information Structures in Games, Theoretical Economics 11(2), 2016. https://doi.org/10.3982/TE1808

Motivation

In Bayesian persuasion a sender who observes the state of the world commits to a signaling scheme, a receiver updates her belief by Bayes' rule and acts, and the sender chooses the scheme that maximizes her own expected payoff (Kamenica and Gentzkow 2011). The classical theory assumes the receiver maximizes expected utility, so her payoff is linear in her belief. Many applications violate this: a customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold, a commuter who values route reliability, a buyer who dislikes uncertainty about a product. Anunrojwong, Iyer and Lingenbrink (arXiv:2208.03758v3) call such receivers risk-conscious: the receiver's utility $\rho(\mu,a)$ of action $a$ at belief $\mu$ is an arbitrary function of $\mu$.

The paper's first result reduces the sender's problem, an optimization over distributions of posteriors, to a finite-dimensional convex program (program (7)). This mission concerns its second main result: in the practically important binary persuasion setting (two actions, the sender always weakly prefers action $1$), when the region of beliefs at which the receiver rejects action $1$ is convex, program (7) collapses further to a linear program whose feasible region is the convex hull of finitely many explicit beliefs.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega)\subseteq\mathbb R^{\Omega}$ the simplex of beliefs, with the Euclidean topology. For $\omega\in\Omega$, $e_\omega$ is the point-mass belief at $\omega$; states are identified with their point masses. The prior is $\mu^*\in\Delta(\Omega)$. The receiver has actions $A=\{0,1\}$ and utility $\rho(\mu,a)$. The optimality regions are

$$P_a=\{\mu\in\Delta(\Omega):\ a\in\arg\max_{a'\in A}\rho(\mu,a')\},$$

and the differential utility is $\hat\rho(\mu)=\rho(\mu,1)-\rho(\mu,0)$, so $P_1=\{\hat\rho\ge 0\}$ and $P_0=\{\hat\rho\le 0\}$ inside $\Delta(\Omega)$. The sender's utility is $v(\omega,a)$ with $v(\omega,1)\ge v(\omega,0)$ for every $\omega$.

Two assumptions are used.

• Assumption 1 (standing throughout the paper): $P_0$ and $P_1$ are closed.
• Assumption 2: the non-adoption region $P_1^c=\{\mu\in\Delta(\Omega):\hat\rho(\mu)<0\}$ is convex.

From these data the paper builds finitely many beliefs. $K_1=\{\omega: e_\omega\in P_1\}$ and $K_0=\{\omega:e_\omega\in P_0\}$ are the states where action $1$, respectively $0$, is optimal under full information, and $L_0=K_0\setminus K_1$ the states where action $0$ is uniquely optimal. For $\omega_0\in L_0$ and $\omega_1\in K_1$,

$$\gamma(\omega_0,\omega_1)=\sup\{g\in[0,1]:\ g e_{\omega_0}+(1-g)e_{\omega_1}\in P_1\},\qquad \chi(\omega_0,\omega_1)=\gamma(\omega_0,\omega_1)e_{\omega_0}+(1-\gamma(\omega_0,\omega_1))e_{\omega_1},$$

the mixture of $\omega_0$ and $\omega_1$ with the most weight on $\omega_0$ at which action $1$ is still optimal, and $K_{01}=\{\chi(\omega_0,\omega_1):\omega_0\in L_0,\ \omega_1\in K_1\}$.

A candidate solution is a pair $t=(t_0,t_1)$ of vectors in $\mathbb R^{\Omega}$, with $t_a(\omega)$ the joint probability of state $\omega$ and action $a$. The sender's objective is $\sum_\omega v(\omega,1)t_1(\omega)+v(\omega,0)t_0(\omega)$. Program (7) maximizes it subject to $t_0+t_1=\mu^*$ and $t_a\in\operatorname{Conv}(P_a\cup\{0\})$; program (10) subject to $t_0+t_1=\mu^*$, $t_1\in\operatorname{Conv}(K_1\cup K_{01}\cup\{0\})$ and $t_0\in\operatorname{Conv}(L_0\cup\{0\})$.

Formalization targets

Goal: Theorem 3

Under Assumptions 1 and 2, with $v(\omega,1)\ge v(\omega,0)$ for all $\omega$:

$$\text{(i)}\ \ t \text{ feasible for (10)} \Rightarrow t \text{ feasible for (7)};\qquad \text{(ii)}\ \ t \text{ feasible for (7)} \Rightarrow \exists\, t' \text{ feasible for (10)},\ \ \text{obj}(t)\le\text{obj}(t').$$

Together these say that (7) and (10) have the same optimal value and every optimal solution of (10) is optimal for (7): (7) "can be optimized by solving" (10).

Milestones

1. $\chi(\omega_0,\omega_1)\in P_0\cap P_1$ for $\omega_0\in L_0$, $\omega_1\in K_1$ (Section 5.1, under Assumption 1).
2. Lemma 6: $\Delta(\Omega)=\operatorname{Conv}(L_0\cup K_{01})\cup\operatorname{Conv}(K_1\cup K_{01})$, with no assumption on $\rho$.
3. Lemma 7: under Assumption 2, $\operatorname{Conv}(P_1)=\operatorname{Conv}(K_1\cup K_{01})$.

Further results on the same objects

• Lemma 3: if $\hat\rho$ is quasiconvex on $\Delta(\Omega)$, Assumption 2 holds.
• Proposition 3: if $v(\omega,1)-v(\omega,0)=\bar v>0$ for all $\omega$ and a strict total order $\prec$ satisfies the monotonicity Assumption 3, every optimal solution of (10) has a threshold $\omega_0\in L_0$ with $t_1(\omega)=\mu^*(\omega)$ for $\omega\prec\omega_0$ and $t_1(\omega)=0$ for $\omega_0\prec\omega$.
• With strict preference $v(\omega,1)>v(\omega,0)$ for all $\omega$, every optimal solution of (7) is feasible for (10).

Significance

Theorem 3 replaces an optimization over a convex set described only implicitly through $\rho$ by a linear program over an explicit polytope. It identifies a canonical signal set: irrespective of the prior, an optimal scheme only needs to induce beliefs in $\Omega\cup K_{01}$, that is, either reveal the state or leave the receiver uncertain between one state of $L_0$ and one of $K_1$. Lemma 7 gives a simple full-persuasion test, $\mu^*\in\operatorname{Conv}(K_1\cup K_{01})$, and Proposition 3 a threshold structure of the induced actions that the paper uses in its queueing application. For expected-utility receivers the corresponding statements reduce to classical facts about concavification; the content here is that they survive non-linear utilities under a single convexity condition.

On the formal side, the results are proved in the paper and nothing about them is machine-checked. A complete development would give a verified reduction of a family of non-linear persuasion problems to linear programs, and a reusable library of convex-hull facts on the simplex (decompositions of the simplex into hulls of point masses and segment points). The formalization also corrects the paper at one point: the proof of Theorem 3 asserts that every optimal solution of (7) is feasible for (10), which fails when the sender is indifferent between actions in some state; the goal is stated in the form the proof establishes.

Difficulty

The inclusion of (10)'s feasible region in (7)'s is immediate once $K_{01}\subseteq P_1$. The content lies in the converse: $P_1$ is an arbitrary closed set whose complement in the simplex is convex, and one must show that every point of $P_1$ is a convex combination of point masses in $K_1$ and the boundary points $\chi(\omega_0,\omega_1)$ on the edges of the simplex. The natural first idea, to argue with extreme points of $\operatorname{Conv}(P_1)$, does not work directly: $P_1$ need not be convex, its convex hull need not be closed a priori, and the extreme points of $P_1$ are not in general on edges of the simplex. Assumption 2 constrains only the complement of $P_1$, so it has to be transported to a statement about $P_1$ itself. A second difficulty is that $t_0$ in a solution of (7) may put weight on states in $K_0\cap K_1$ or on interior beliefs, and it must be moved to $t_1$ without lowering the objective.

Formalization scope

• Beliefs are functions Ω → ℝ with [Fintype Ω] [DecidableEq Ω]; $\Delta(\Omega)$ is Mathlib's stdSimplex ℝ Ω; $e_\omega$ is Pi.single ω 1; actions are Fin 2; $\operatorname{Conv}$ is convexHull ℝ; $0$ is the zero vector.
• The receiver's utility is ρ : (Ω → ℝ) → Fin 2 → ℝ, and $P_a$ is defined from it by Eq. (1), intersected with the simplex; values of ρ off the simplex are irrelevant. Assumption 1 is IsClosed (P ρ a) for both actions.
• $K_0,K_1,L_0$ are sets of states; they enter convex hulls through their images under $e$. $\gamma$ is a real sSup, used only for $\omega_0\in L_0$, $\omega_1\in K_1$, where the set contains $0$ and is bounded by $1$.
• Programs (7) and (10) are feasibility predicates on t : Fin 2 → Ω → ℝ with a common objective. Theorem 3 is stated as (i) and (ii) above, never through a supremum of objective values. A formalization in which (10) only needs to have some feasible point, or in which the supremum of an empty or unbounded set of values is compared, would be trivial or meaningless and is not the target.
• Proposition 3 takes the order of Assumption 3 as a relation given with the data, and assumes $L_0\neq\emptyset$, which the paper uses implicitly.
• Needed infrastructure: convex hulls of finite sets of point masses in the simplex, Carathéodory-type finite decompositions (available in Mathlib), and the decomposition of a convex combination along a segment. Proofs of the milestones, alternative proofs of Lemma 7 (for example by a separation argument), and proofs of the further results are all welcome.

Selected references

• Anunrojwong, J., Iyer, K., Lingenbrink, D., Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023 (journal version: Operations Research, 2024). https://arxiv.org/abs/2208.03758v3
• Kamenica, E., Gentzkow, M., Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590

Motivation

Ride-hailing platforms such as Uber and Lyft match riders with self-scheduling drivers who decide for themselves whether to work. Two features make capacity planning on such a platform different from classical fleet management. Demand is spatially imbalanced: more trips start in some locations than end there, so cars accumulate where they are not needed unless they drive back empty. And capacity is endogenous: the number of participating drivers depends on what drivers expect to earn, which in turn depends on how the platform uses them.

Afèche, Liu and Maglaras (MSOM 2023) study how much a platform gains from two operational controls under these conditions: admission control (rejecting some ride requests, depending on destination) and centralized repositioning (directing idle drivers to move empty between locations). The benchmark of their comparison is the regime in which the platform has both controls, called centralized control (regime $C$). This mission formalizes the paper's characterization of that benchmark: how a fixed number of drivers should be allocated, what each driver then earns, and why the resulting driver equilibrium is the platform's optimum.

Setting

There are two locations and four routes $lk$, $l,k\in\{1,2\}$. Route $lk$ has potential demand rate $\Lambda_{lk}$ and travel time $t_{lk}>0$. The price is $p$ per unit of travel time; the platform keeps a share $\gamma\in(0,1)$ and drivers keep $\bar\gamma p$, with $\bar\gamma=1-\gamma$, while paying a driving cost rate $c$, with $\bar\gamma p-c>0$. Demand is imbalanced: $0<\Lambda_{12}<\Lambda_{21}$ (Assumption 1). Repositioning is profitable: $c\,t_{12}<t_{21}(\bar\gamma p-c)$ and $c\,t_{21}<t_{12}(\bar\gamma p-c)$ (Assumption 2).

A pool of $N$ potential drivers has opportunity cost rates drawn from a continuous distribution with CDF $F$, strictly increasing on $[0,\bar c_o]$ with $\bar c_o\ge p-c$, $F(0)=0$ and $F(\bar c_o)=1$ (Assumption 3). If drivers expect a profit rate $\pi$, then $n=NF(\pi)$ of them participate.

In steady state the platform splits a driver capacity $n$ into service capacity $s_{lk}\le S_{lk}:=\Lambda_{lk}t_{lk}$ on each route, repositioning capacity $r_{12},r_{21}$ (empty driving) and queueing capacity $q_1,q_2$ (idle drivers). With totals $\bar s$, $\bar r$, $\bar q$ and $\bar S=\sum_{lk}S_{lk}$, the set $\mathcal C_C(n)$ of feasible allocations is

$$\frac{s_{12}+r_{12}}{t_{12}}=\frac{s_{21}+r_{21}}{t_{21}},\qquad \bar s+\bar r+\bar q=n,\qquad 0\le s\le S,\ r\ge0,\ q\ge0 .$$

The first equation balances the flows of cars between the locations. The platform earns $\Pi(s)=\gamma p\bar s$; each driver earns

$$\pi(s,r,n)=\frac{(\bar\gamma p-c)\bar s-c\bar r}{n}.$$

The platform's problem (13) maximizes $\Pi(s)$ over $(s,r,q,n)$ with $(s,r,q)\in\mathcal C_C(n)$ and the participation equation $n=NF(\pi(s,r,n))$; its value is $\Pi^*_C$.

The paper solves (13) in two steps. Step 1 fixes $n$, computes the maximal revenue $\Pi_C(n)$ over $\mathcal C_C(n)$, and among the revenue-maximizing allocations selects one that maximizes $\pi$, giving the per-driver profit $\pi_C(n)$. Step 2 solves $n_C=NF(\pi_C(n_C))$. The constants

$$n^C_1:=\bar S-(\Lambda_{21}-\Lambda_{12})t_{21},\qquad n^C_2:=\bar S+(\Lambda_{21}-\Lambda_{12})t_{12}$$

split capacities into scarce, moderate and ample zones.

Formalization targets

Goal: Corollary 1

$$\pi_C \text{ continuous and nonincreasing on }(0,\infty),\ \text{strictly decreasing on }(n^C_1,\infty);\qquad \exists!\,n_C>0:\ n_C=NF(\pi_C(n_C));$$ $$\pi_C(n)=\max_{(s,r,q)\in\mathcal C_C(n)}\pi(s,r,n)\quad(0<n\le N);\qquad \Pi^*_C=\Pi_C(n_C),\ \text{attained by the two-step tuple at } n_C .$$

Milestones

1. Proposition 1(1)–(3): the selected optimal allocation in each zone — $\bar s=n$, $r=q=0$ for $n\le n^C_1$; $\bar s+r_{12}=n$ with $r_{12}=\frac{t_{12}}{t_{12}+t_{21}}(n-n^C_1)$, $r_{21}=0$, $q=0$ for $n^C_1<n\le n^C_2$; $\bar s=\bar S$, $r_{12}=n^C_2-\bar S$, $r_{21}=0$, $\bar q=n-n^C_2$ for $n>n^C_2$.
2. Display (18): the closed form of $\pi_C(n)$ in the three zones.
3. Lemma 1 at $X=C$: if $\pi_C$ is driver-optimal (16) and nonincreasing, the two-step solution solves (13).

Significance

The corollary is what makes centralized control a usable benchmark. It says the platform's joint problem, which couples a linear program with a fixed-point equation in $n$, decomposes: the platform can optimize a fixed capacity and then let drivers settle, with no loss. Under the other regimes of the paper this alignment of platform and driver incentives can fail, and the paper's comparisons of regimes (value of admission control, value of repositioning) are measured against the regime-$C$ optimum characterized here. Proposition 1 also makes explicit that a centralized platform keeps drivers idle only when all demand is served.

The paper's proofs are in its e-companion, which is not part of the source this mission cites; no machine-checked version of these results exists. The mission produces a checked parametric solution of a small linear program, a checked closed form of the per-driver profit, and a checked equilibrium-and-optimality argument, with every standing assumption made explicit.

Difficulty

Proposition 1 is a parametric linear program in eight variables, but stating its solution is not enough: each zone needs an upper bound on $\bar s$ valid on all of $\mathcal C_C(n)$, and a second optimization (per-driver profit) over the set of revenue maximizers, which is not a singleton. Driver-optimality (16) is a separate claim about a different objective over the full set $\mathcal C_C(n)$; it holds only because Assumption 2 makes the capacity used for excess cross-location demand still profitable for drivers. Finally, Lemma 1 compares tuples of (13) at different capacities, which requires monotonicity of $\Pi_C$ and $\pi_C$ in $n$ and the participation equation at both capacities. The natural reading of "$n^*_C=n_C$" as uniqueness of the optimal capacity is false when $n_C>n^C_2$, since wasteful repositioning can keep revenue $\gamma p\bar S$ at a smaller capacity; the targets assert attainment instead.

Formalization scope

All objects live in the namespace RideHailing.Central, in one definition file. Routes are named fields (Λ11 … Λ22, t11 … t22), not indexed. $F$ is ProbabilityTheory.cdf μ of a measure μ on $\mathbb R$. The standing hypothesis Model.Standing bundles $0<\gamma<1$, $\bar\gamma p-c>0$, Assumptions 1–3 as printed, and the paper's implicit conventions, made explicit: $t_{lk}>0$, $\Lambda_{11},\Lambda_{22}\ge0$, $p>0$, $N>0$, $c>0$, $\mu$ a probability measure with continuous CDF.

$\Pi_C(n)$ and $\pi_C(n)$ are defined as suprema over the allocation problem; every target states attainment with IsGreatest or with membership in the selected set, so no conclusion rests on a supremum convention. Capacities in (13) and (16) are strictly positive, because (12d) divides by $n$.

Trivializing formalizations are ruled out: $\pi_C$ is defined through the two-step selection, never by its closed form (18); "max" is never an unattained supremum; feasibility for (13) includes the participation equation and $n>0$; and $n_C$ is characterized by $\exists!$ and then quantified over, never chosen.

Regimes $M$ and $A$ of the paper, which need objects defined only in the e-companion, are out of scope, as are the reformulation of §2.4 and Remark 2. Proofs of any milestone, and lemmas on monotonicity of $\Pi_C$ or attainment of linear programs over $\mathcal C_C(n)$, are welcome.

Selected references

• P. Afèche, Z. Liu, C. Maglaras, Ride-Hailing Networks with Strategic Drivers: The Impact of Platform Control Capabilities on Performance, Manufacturing & Service Operations Management, Articles in Advance, 2023. https://doi.org/10.1287/msom.2023.1221

Motivation

The European Union's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers privacy rights over the personal data that firms collect: data may be collected only with explicit consent (opt-in), consent is separated from the purchase itself, and a consumer may later have her data deleted (erasure, the "right to be forgotten"). The same regulations carry a data security mandate, because data held by a firm is exposed to breaches. Regulators, firms and economists want to know how these rights change what data is collected, what prices are charged, and who gains.

Ke and Sudhir (SSRN 3643979; published in Management Science, 2022, doi:10.1287/mnsc.2022.4614) build a two-period model in which a firm sells a basic good, may collect a consumer's data with her consent, and uses the data to sell a personalized good in the second period. Consumers trade off the personalization benefit against the expected cost of a data breach. This mission formalizes the paper's first main result, Proposition 1: the equilibrium of the monopoly market with privacy rights. The companion mission (number 2 of this series) formalizes the benchmark without privacy rights.

Setting

A monopolist faces a unit mass of consumers whose valuation $v$ of the basic good is uniform on $[0,1]$. A consumer values the personalized good at $(1+\kappa)v$, where $\kappa\in\{\kappa_L,\kappa_H\}$ with probability $1/2$ each and $\kappa_H>\kappa_L>0$. Write

$$\mu=\frac{\kappa_H+\kappa_L}{2},\qquad \sigma=\frac{\kappa_H-\kappa_L}{2}.$$

A consumer learns her $\kappa$ only after the first period, and the firm never learns it. Both sides discount the second period by $\delta\in(0,1]$. Each period in which the firm holds a consumer's data costs her an expected breach cost $c\ge0$.

Period 1. The firm posts a price $p_1$. Each consumer chooses among not buying, buying without opting in, and buying and opting in. Opting in reveals $v$ to the firm and costs $c$.

Period 2. The firm posts a basic price $p_2$ and offers each opted-in consumer a personalized price $r(v)$. A consumer who did not opt in buys the basic good iff $v\ge p_2$; she never opts in in the last period. An opted-in consumer either keeps her data and buys the personalized good, with utility $(1+\kappa)v-r(v)-c$, or erases her data and takes $\max\{v-p_2,0\}$.

An equilibrium is a profile $(p_1,\ p_2(\cdot),\ r(\cdot,\cdot),\ \text{choice}(\cdot,\cdot))$ in which every personalized price $r(v,q)$ maximizes the expected revenue from consumer $v$ at basic price $q$; after every first-period price $p_1$, the basic price $p_2(p_1)$ maximizes the firm's second-period profit; after every $p_1$, every consumer's first-period action is optimal; and $p_1$ maximizes the firm's total profit over all real prices. The paper also imposes Assumption 1:

$$\mu\ \ge\ \max\Big\{(3+\delta)\sigma,\ \tfrac12+(2+\delta)\sigma\Big\}.$$

Formalization targets

Goal: Proposition 1

Under Assumption 1, an equilibrium exists with the following outcome in each regime. The constants $v_1^*$ and $P_1^*$ are those of the paper's appendix.

• A. $0\le c\le\delta\sigma/2$: $p^*_{1M}=P_1^*$ and $p^*_{2M}=1$. Consumers with $v\ge v_1^*$ opt in and then buy the personalized good at $(1+\mu-\sigma)v-c$. Consumers with $v<v_1^*$ never buy.
• B. $\delta\sigma/2<c\le\delta\sigma/\sqrt2$: $p^*_{1M}=1/2$ and $p^*_{2M}=1$. Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(1+\mu-\sigma)v-c$. Those with $1/2\le v<c/(\delta\sigma)$ buy only in period 1. The rest never buy.
• C. $\delta\sigma/\sqrt2<c<\delta\sigma$: $p^*_{1M}=p^*_{2M}=1/2$. Consumers with $v\ge c/(\delta\sigma)$ opt in and pay $(\mu-\sigma)v+1/2-c$. Those with $1/2\le v<c/(\delta\sigma)$ buy the basic good in both periods. The rest never buy.
• D. $c\ge\delta\sigma$: no one opts in, $p^*_{1M}=p^*_{2M}=1/2$, and a consumer buys in each period iff $v\ge1/2$.

Milestones

The equilibrium personalized price, eqs. (1)–(2):

$$r^*_M(v,p_2)=(\mu-\sigma)v+\min\{v,p_2\}-c,$$

which is optimal whenever $2(\kappa_Lv-c)\ge\kappa_Hv-c\ge0$, a condition Assumption 1 guarantees above the opt-in threshold.

The opt-in threshold, eq. (4):

$$v^*_M(p_1)=\max\Big\{\frac{c}{\delta\sigma},\frac{p_1+c}{1+\delta\sigma}\Big\}.$$

The second-period basic price, eq. (3): $p^*_{2M}(p_1)=1/2$ if $v^*_M(p_1)\ge1/\sqrt2$, and $1$ otherwise.

The remaining milestones are the identification of the firm's profit with the reduced first-period profit of p. 15, and the three cases of the appendix proof that locate its maximizer.

Significance

Proposition 1 is the basis of the paper's comparative statics and policy conclusions. The comparison with the benchmark (Proposition 2) shows when privacy rights raise or lower opt-in, profits and consumer surplus. Corollary 3 shows that under privacy rights, opt-in and profit fall strictly with the breach cost. In the paper's interpretation, the result explains how data-security investment and the rights themselves interact: privacy rights let consumers avoid the hold-up problem of sharing data before knowing its value to them.

The result is proved on paper in the appendix, by reducing the game to a piecewise-quadratic maximization. It has not been machine-checked. A formal proof adds a fully specified equilibrium concept with optimality at every history and an explicit treatment of tie-breaking and knife-edge regimes. It also corrects one misprint in the SSRN text (the price in case B(i)). This is the platform's first two-period data-market game with opt-in and erasure; existing privacy items are one-shot models.

Difficulty

The difficulty is that the goal is a statement about a game, not about the closed forms. A solver must exhibit strategies at every history, including first-period prices far from equilibrium and arbitrary basic prices. They must then show that the consumers' choices form a threshold set whose measure and integrals are the ones the reduced profit assumes.

The tempting shortcut is to read eq. (2) as the firm's personalized price everywhere. Eq. (1) shows it is optimal only in case (i); for small $v$ the firm prefers to price only to the high type or to let both types erase. The equilibrium survives because no such consumer opts in, which must be shown from the consumers' side. The global maximization of the first-period profit over all real $p_1$ involves a function with kinks at $p_1=c/(\delta\sigma)$, at the price where $v^*_M(p_1)=1/\sqrt2$, and where $v^*_M(p_1)$ reaches $1$. Both halves of Assumption 1 are used in comparing its pieces.

Formalization scope

Parameters are a structure Params with fields kL, kH, d ($\delta$) and c; $\mu$, $\sigma$, the standing assumptions ($0<\kappa_L<\kappa_H$, $0<\delta\le1$, $0\le c$) and Assumption 1 are definitions, and every theorem carries both predicates as hypotheses. Consumers are $v\in[0,1]$ with Lebesgue measure. Expectations over $\kappa$ are averages of the two types. All quantities are real numbers, and prices range over all of $\mathbb R$.

Committed conventions:

• An indifferent consumer buys.
• An opted-in consumer keeps her data on a tie.
• "No basic good is offered" is the basic price $1$.
• The goal asserts existence of an equilibrium with the stated outcome, not uniqueness, which the paper does not claim.
• The knife-edge $c=\delta\sigma/\sqrt2$ belongs to B, as in the proposition.
• In B(i) the formal statement uses the price $(1+\mu-\sigma)v-c$ that eq. (2) gives when no basic good is sold; the SSRN text prints C's price there.

Profits are integrals over the sets of consumers defined by the profile's own choices. A formalization that defined profits by the paper's closed forms would be trivial and is excluded. So are optimality checked only on the equilibrium path, a dropped Assumption 1, a missing bullet of the proposition, and a uniqueness claim. A sorry-free check confirms that the hypotheses are satisfiable at the paper's figure point $\kappa_L=4$, $\kappa_H=6$, $\delta=0.8$.

The development needs interval integrals and Lebesgue measure of intervals on $\mathbb R$, and elementary real inequalities with square roots. The reduced-profit identity (consumers' optimal choices form threshold sets up to null sets) is the reusable core and would serve the benchmark mission too. Proofs of individual milestones are welcome independently.

Selected references

• T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, SSRN working paper 3643979 (pdfTeX build 2022-09-14). https://ssrn.com/abstract=3643979
• T. Tony Ke and K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4614
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

Personal data lets a firm tailor its product to each customer, and the same data exposes the customer to the risk of a breach. The EU's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers rights over that data. Data collection must be opted into separately from the purchase, and stored data must be erased on request. Ke and Sudhir (SSRN 3643979; Management Science 2022, doi:10.1287/mnsc.2022.4614) build a two-period model of a data-driven market to ask what these rights do to prices, purchases, profits and consumer surplus.

To isolate the effect of privacy rights, the paper needs the equilibrium of the same market without them. That equilibrium is its Proposition 2, the benchmark of §3.2. Every comparison in §3.3 (segmentation, prices, profit, consumer surplus, Corollaries 1–3) contrasts it with the equilibrium under privacy rights (Proposition 1, the companion mission of this series).

Setting

A monopolist sells a basic good over two periods. A unit mass of consumers has valuations $v$ uniform on $[0,1]$, and the outside option is worth $0$ in each period. Firm and consumers discount the second period by $\delta\in(0,1]$. A consumer values a personalized good at $(1+\kappa)v$, where $\kappa$ equals $\kappa_L$ or $\kappa_H$ with probability $1/2$ each, $\kappa_H>\kappa_L>0$. She learns her $\kappa$ only at the start of period 2, and the firm never observes it. Write

$$\mu=\frac{\kappa_H+\kappa_L}{2},\qquad \sigma=\frac{\kappa_H-\kappa_L}{2}.$$

The paper keeps Assumption 1, $\mu\ge\max\{(3+\delta)\sigma,\ \tfrac12+(2+\delta)\sigma\}$, throughout.

No privacy rights. A first-period purchase reveals $v$ to the firm, and the consumer bears an expected breach cost $c\ge0$ in every period the firm holds her data. The data cannot be erased, so a first-period buyer bears $c$ in period 2 as well, whatever she does then. In period 2 the firm offers each past buyer the personalized good at a price $r(v)$ tailored to her valuation, and offers the basic good at a price $p_2$ to those who did not buy in period 1. A non-buyer who buys the basic good in period 2 also bears $c$.

The firm chooses $p_1$, then $p_2$ as a function of $p_1$, and $r(v)$. Consumers choose whether to buy in period 1, anticipating the second-period prices. An equilibrium satisfies four conditions:

1. $r(v)$ maximizes the expected revenue from a past buyer of valuation $v$;
2. after every first-period price, $p_2$ maximizes second-period profit given who bought in period 1;
3. after every first-period price, each consumer's first-period choice is optimal;
4. $p_1$ maximizes the firm's discounted profit over all real prices.

Formalization targets

Goal: Proposition 2

Let

$$T_1=\frac{2-\delta+2\delta\sigma}{2-\delta+2\delta\mu+2\delta\sigma},\qquad T_2=1+\frac{\delta}{1+\delta}\,\mu .$$

Under the standing assumptions and Assumption 1 there is an equilibrium with the following outcome in each regime.

• A, $0\le c\le T_1$: $p_1=P_1^B$. Consumers with $v\ge\overline v_1^B$ buy in period 1 and then buy the personalized good at $r^B_M(v)=(1+\mu-\sigma)v$. Those with $\overline v_1^B>v\ge\underline v_1^B$ buy only the basic good in period 2, at $p^B_{2M}=[P_1^B+\delta(1-\sigma)c]/(2-\delta+2\delta\sigma)$. The rest never buy.
• B, $T_1<c<T_2$: $p_1=P_2^B$. Consumers with $v\ge v_2^B$ buy in period 1 and then buy the personalized good at $(1+\mu-\sigma)v$. Nobody else ever buys.
• C, $c\ge T_2$: nobody buys in either period.

The closed forms $P_1^B$, $\overline v_1^B$, $\underline v_1^B$, $P_2^B$, $v_2^B$ are the paper's (pp. 49–51).

Milestones

The appendix proof (pp. 48–51) supplies the steps, in order:

1. the optimal personalized price $r^B_M(v)=(1+\kappa_L)v$;
2. the second-period basic price (5), $p^B_{2M}(p_1)=(v^B_M(p_1)-c)/2$;
3. the first-period threshold (6) and its fixed point with (5);
4. the first-period price (7);
5. the regime without second-period sales and its price (8);
6. the conditions separating the regimes;
7. the corner regime at $p_1=\delta(\sigma-1)c$, which merges with (8) into $P_2^B$, $v_2^B$.

Significance

Proposition 2 describes how a data market behaves when the firm owns the data. A consumer who buys is locked in: the firm extracts the low type's full valuation of personalization, and both types keep buying. Consumers anticipate this hold-up, so first-period demand shrinks. Once $c>T_1$, the firm no longer sells the basic good in period 2, and the market becomes "now or never". Once $c\ge T_2$ it closes. The paper's comparisons of segmentation, prices, profit and consumer surplus with and without GDPR rights all start from these regimes.

Formalizing it gives the platform a two-period equilibrium with data lock-in. That equilibrium has its own fixed point: the consumers' threshold depends on the second-period price, and that price depends on the threshold. The result is proved in the paper, partly by first-order conditions ("It is easy to verify that the second-order optimality condition is satisfied"). It has not been machine-checked. Formalizing it also fixes a typo in eq. (7), which prints a stray $\kappa$ in the numerator of $P_1^B$.

Difficulty

The obvious argument is the paper's: guess threshold strategies, solve the first-order conditions, read off the regimes. Each step is calculus, but an equilibrium must hold at every history, not only along the guessed path. The solver must exhibit $p_2$ and the consumers' choices after every first-period price, including prices at which nobody or everybody buys. It must show that the consumers' threshold and the firm's $p_2$ are a fixed point at each such price. It must then prove that the firm's first-period price is a global maximizer of a piecewise objective with a kink at $p_1=\delta(\sigma-1)c$. On each side of the kink the objective is a different quadratic, and on the far sides the threshold leaves $[0,1]$. The first-order conditions alone show none of this.

Formalization scope

The Lean development lives in the namespace GDPRDataMarkets.Benchmark. Its conventions:

• Parameters. All quantities are real. The standing assumptions $0<\kappa_L<\kappa_H$, $0<\delta\le1$ and $c\ge0$ are Params.Standing, and Assumption 1 is Params.Assumption1. The goal carries both as hypotheses.
• Consumers and κ. Masses are the Lebesgue measure of subsets of $[0,1]$. Expectations over $\kappa$ are averages of the two types.
• Ties. An indifferent consumer buys: the personalized good iff $r(v)\le(1+\kappa)v$, the basic good iff $v-p_2-c\ge0$, and in period 1 the profile may choose either side at the single indifferent valuation.
• Profits. The firm's profits are integrals and Lebesgue measures over the consumers' own choices. The paper's reduced closed forms appear only in the milestones.
• Strategies. The firm's second-period price is a function of $p_1$.
• Existence only. Proposition 2 asserts existence of an equilibrium with the stated outcome, as the paper does; uniqueness is not posed.

A formalization in which the profits are the paper's closed forms rather than integrals over the consumers' optimal choices would make the goal calculus. So would one in which the second-period price or the consumers' choices are optimal only on the equilibrium path, or one that drops Assumption 1 or a bullet of the proposition. The statements here do none of these.

Assumption 1 enters the proof only through $\mu\ge3\sigma-1$ (p. 49), which makes $(1+\kappa_L)v$ the optimal personalized price. The milestone for that step assumes exactly this weaker condition.

Infrastructure needed: interval integrals of linear functions, Lebesgue measure of intervals, and maximization of concave quadratics. The equilibrium predicate is reusable for variants of this model, such as other breach-cost structures. Proofs of the milestones in any order are welcome.

Selected references

• T. Tony Ke, K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, SSRN working paper 3643979 (pdfTeX build 2022-09-14). https://ssrn.com/abstract=3643979
• T. Tony Ke, K. Sudhir, Privacy Rights and Data Security: GDPR and Personal Data Markets, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4614
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.

Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.

Setting

There are $4m$ manufacturers, $m\ge 2$. Manufacturer $i$ has a horizontal type $q_i\in\{A,B\}$ and a vertical type $\xi_i\in\{h,l\}$; each of the four type classes has exactly $m$ members. Joining the blockchain costs manufacturer $i$ an amount $\chi_i>0$; $a_i\in\{0,1\}$ records the decision. A unit mass of consumers values a matching product at $H$ and a mismatched one at $L$, with $0\le L<H$, plus a vendor quality $h>l\ge 0$; the high-quality vendor has marginal cost $\gamma>0$. Each consumer $k$ also has an outside option $\phi_k$, drawn from a continuous distribution $G$ supported on $[0,\infty)$. The parameter of interest is the horizontal differentiation $\Delta=H-L$; $L$ is held fixed and $H=L+\Delta$.

Under full adoption, a consumer who has access to the blockchain's information finds a best product utility $\Delta+L+h-\gamma$; without access, only $\Delta/2+L+h-\gamma$. A system of transfers $(\kappa,\{\tau_i\}_{i\in M})$ charges each consumer who wants access a fee $\kappa$ and pays manufacturer $i$ an amount $\tau_i\ge 0$. A consumer pays ($b_k=1$) when

$$\max\{\Delta+L+h-\gamma,\phi_k\}-\kappa\ \ge\ \max\Big\{\tfrac{\Delta}{2}+L+h-\gamma,\phi_k\Big\},$$

and $\mu_\kappa$ denotes the mass of paying consumers. The system is self-financing if

$$\kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i. \tag{14}$$

Manufacturer $i$ earns $\Pi(a_i,a_{-i})-\chi_i a_i+\tau_i a_i$ (15), where the gross profit $\Pi$ is zero because of price competition. The system overcomes adoption failures if full adoption ($a_i=1$ for all $i$) is an equilibrium of this game.

The proof of Proposition 4.9 uses the fee $\kappa=\sum_i\chi_i/G(\phi)$ and the gain from access

$$h(\phi_k;\phi)=\max\{\Delta+L+h-\gamma,\phi_k\}-\frac{\sum_{i\in M}\chi_i}{G(\phi)}-\max\Big\{\frac{\Delta}{2}+L+h-\gamma,\phi_k\Big\}.$$

Formalization targets

Goal: Proposition 4.9 (p. 21)

$$\exists\,\Delta_0\ \forall\,\Delta>\Delta_0\ \exists\,\kappa,\{\tau_i\}:\quad \tau_i\ge 0,\quad \kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i,\quad a\equiv 1\ \text{is an equilibrium of (15)}.$$

The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.

Milestones: Lemma B.1 (p. 38)

(a) For $\Delta>0$ and every $\phi$, $\phi_k\mapsto h(\phi_k;\phi)$ is continuous and weakly decreasing on $[0,\infty)$.

(b) For all sufficiently large $\Delta$ there is $\phi^*\ge 0$ with

$$h(\phi^*;\phi^*)=0,\qquad h(\phi_k;\phi^*)\ge 0\iff \phi_k\le\phi^*\quad(\phi_k\ge 0),$$

so that at the fee $\sum_i\chi_i/G(\phi^*)$ exactly the consumers with $\phi_k\le\phi^*$ pay.

Significance

Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme ($\tau_i=\chi_i$, $\kappa=\sum_i\chi_i/G(\phi^*)$) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.

The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.

Difficulty

The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point $h(\phi^*;\phi^*)=0$, and the delicate points are positivity of $G$ at the relevant arguments (so that the fee is finite), the three-piece shape of $h(\cdot;\phi)$, and choosing $\Delta$ large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.

Formalization scope

• Reduced form. The paper's full model is a signal game with Bertrand pricing whose equilibrium concept is not defined precisely; its proofs work with the closed-form outcome of Proposition A.1. The formalization does the same: consumer utilities are those computed in the proof of 4.9 ($\Delta+L+h-\gamma$ with access, $\Delta/2+L+h-\gamma$ without), gross profit $\Pi$ is the constant $0$ in every profile (pp. 37–38, also for a deviating manufacturer), and "equilibrium" is a pure Nash equilibrium over unilateral switches of $a_i\in\{0,1\}$. Signal accuracy is $\alpha=1/2$, as in the paper's main text.
• Encoding. Manufacturers are Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. $G$ is ProbabilityTheory.cdf μ for a measure μ on ℝ. $\Delta$ is an argument of every object, with $H=L+\Delta$.
• Standing assumptions (one predicate Model.Standing): $m\ge 2$, $0\le L$, $0\le l<h$, $\gamma>0$, $\chi_i>0$; $\mu$ a probability measure without atoms, $\mu((-\infty,0))=0$, and $\mu((a,b))>0$ for $0\le a<b$ (support $[0,\infty)$). No cost function $c_l$, no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes $\Delta>0$, the model's $L<H$.
• Ties in the access decision go to paying, as in the proof's "$b_k=1$ iff $h\ge 0$".
• Ruled out. $\mu_\kappa$ is the $\mu$-measure of the paying consumers, not a free number in $[0,1]$; the equilibrium predicate and $\Pi$ are defined, not assumed; transfers are nonnegative; and no statement relies on Lean's value $0$ for a division by $G(\phi)=0$.
• Not formalized. The non-uniqueness clause of Lemma B.1(b) and Example B.1 (p. 40); the purchase-stage claims of the proof of 4.9 (market shares under transfers); Appendix C's symmetric-cost variant.
• Infrastructure. Only Mathlib's measure theory and ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on $[0,\infty)$ are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532