Operations Research

Cryptocurrencies as platform memberships

A cryptocurrency launched through an initial coin offering is often sold before the platform it serves has users. Its value to a buyer then depends on who else buys: a token that gives access to a trading network is worth more when many households with large endowments join. Sockin and Xiong (preliminary draft, March 2018, later published in Management Science) build a tractable rational-expectations model of this complementarity, in which the price of the currency is pinned down jointly by households who buy memberships and by miners who supply them. The perfect-information benchmark of the paper, in which the platform fundamental and the mining-cost shock are publicly observed, already shows the central phenomenon: the market can have two self-confirming equilibria, one with a high price and broad adoption and one with a low price and narrow adoption, and they respond to fundamentals in opposite directions.

The model belongs to the literature on multiple equilibria from strategic complementarities (Morris and Shin 1998) and on search models of money (Kiyotaki and Wright 1993), applied to a market in which the supply side is a population of miners with heterogeneous costs.

Setting

There are two dates. A continuum of households has endowment exponents $A_i = A + \varepsilon_i$ with $\varepsilon_i \sim N(0, \tau_\varepsilon^{-1})$, where $A$ is the platform fundamental. At $t = 2$ a household is randomly matched with another; if both own the currency, they trade, and with Cobb–Douglas utility

$$U(C_i, C_j) = \Big(\frac{C_i}{1-\eta_c}\Big)^{1-\eta_c}\Big(\frac{C_j}{\eta_c}\Big)^{\eta_c}, \qquad \eta_c \in (0,1),$$

the competitive allocation of the matched pair gives household $i$ the realized utility $e^{(1-\eta_c)A_i + \eta_c A_j}$. A household that does not trade gets zero utility.

At $t = 1$ each household decides whether to buy one unit of the currency at price $P$. It buys exactly when its expected utility $E[U_i \mid \mathcal I_i]$, the expectation over its partner's $A_j = A + \varepsilon$ of $e^{(1-\eta_c)A_i + \eta_c A_j}$ on the event that the partner also buys, is at least $P$. Miners have productivity $\omega_i = \xi + e_i$ with $e_i \sim N(0, \tau_e^{-1})$, receive a share $1 - \rho_s \in (0,1)$ of the proceeds, and mine exactly when $(1-\rho_s)P \ge e^{-\omega_i}$. The developer keeps the share $\rho_s$, so its revenue is $\Pi_D = \rho_s P$ times the mass of buyers. The ex ante utility is $U_0 = E[\max\{E[U_i\mid\mathcal I_i] - P, 0\}]$.

An equilibrium at $(A, \xi)$ is a measurable purchase set $B$ of endowment exponents and a price $P > 0$ such that the households in $B$ are exactly those whose expected utility, computed with partners drawn from $B$, is at least $P$, and the $N(A, \tau_\varepsilon^{-1})$-mass of $B$ equals the mass of miners who mine at $P$. In the Lean development these are IsEquilibrium P A xi B price and equilibria P A xi, in the namespace CryptoMembership.PerfectInfo.

Formalization targets

Goal: Proposition 2

There is a threshold $K$ such that there are exactly two equilibria when $A + \xi > K$, one when $A + \xi = K$, and none when $A + \xi < K$. Moreover:

1. every equilibrium purchase set is a cutoff set $\{A_i \ge A^*\}$, and the cutoffs are exactly the solutions of

$$e^{(1-\eta_c+\sqrt{\tau_\varepsilon/\tau_e})(A^*-A)}\,\Phi\Big(\eta_c\tau_\varepsilon^{-1/2} - \frac{A^*-A}{\tau_\varepsilon^{-1/2}}\Big) = e^{-A-\xi-\frac12\eta_c^2\tau_\varepsilon^{-1}-\log(1-\rho_s)};$$

2. the price is log-linear, $\log P = \sqrt{\tau_\varepsilon/\tau_e}\,(A - A^*) - \xi - \log(1-\rho_s)$;
3. in the high-price equilibrium (lower cutoff) the price, $\Pi_D$, $U_0$ and the mass of buyers increase in $A$, and in the low-price equilibrium (higher cutoff) they decrease; the mass of buyers moves the same way in $\xi$;
4. no equilibrium exists when $A$ or $\xi$ is sufficiently small.

Milestones

The milestones follow the proof in Appendix A: the matched-pair allocation and utility of Proposition 1; the closed forms of $E[U_i\mid\mathcal I_i]$ and $U_0$; optimality of cutoff strategies; market clearing as equation (13); the reduction of equilibria to the roots of equation (15); the log-concave bell shape of the left side of (15); the two–one–none root count; and the opposite movement of the two roots as the right side falls.

Significance

Proposition 2 is the paper's characterization of adoption equilibria with observable fundamentals. It explains why a token market can sustain both a high-price, broad-adoption outcome and a low-price, narrow-adoption one, why the latter reacts perversely to good news about the platform, and why a platform below a fundamental threshold attracts no buyers at all. The later sections of the paper build the unobservable-fundamentals analysis on the same equation.

Formalizing it produces a complete, checked equilibrium analysis of a nonlinear rational-expectations model: the equilibrium is defined from optimization and market clearing over arbitrary measurable purchase sets, and the count of equilibria is stated as an exact trichotomy rather than "generically". As far as is known, no part of this paper has been formalized. The development also requires facts about the Gaussian distribution that are reusable elsewhere, notably strict log-concavity of the standard normal cdf and truncated Gaussian moment generating functions.

Difficulty

The reduction to a scalar equation is mechanical once one knows that equilibria are cutoff sets; that step must be proved for an arbitrary measurable purchase set rather than assumed, as the paper does when it announces the cutoff form as a conjecture on p. 15. The equilibrium count rests on strict log-concavity of $s \mapsto \log\Phi(c - \sqrt{\tau_\varepsilon}\,s)$, which is not in Mathlib, and on the tail behaviour of $\Phi$ against an exponential. The comparative statics of $U_0$ are not a direct consequence of the root statics: $U_0$ depends on both the price and the cutoff, and its monotonicity in the low-price equilibrium has to be established without the sign error in the paper's own derivative computation.

Formalization scope

All quantities are real. Normal laws are Mathlib's gaussianReal with variances $\tau_\varepsilon^{-1}$ and $\tau_e^{-1}$, and $\Phi$ is the cdf of gaussianReal 0 1. The standing assumptions $\eta_c \in (0,1)$, $\tau_\varepsilon > 0$, $\tau_e > 0$, $\rho_s \in (0,1)$ are bundled in Params.Standing. Ties are broken as on the page: a household buys when expected utility equals the price, and a miner mines when its revenue equals its cost. The mining cost is $e^{-(\xi + e_i)}$ as in (4); display (5) prints $e^{-\xi+e_i}$, which yields the same mass of miners. Prices are positive. Equilibria are counted with Set.encard over pairs (purchase set, price). The high- and low-price equilibria are the cutoff equilibria with the smallest and largest cutoff. "No household buys" is stated as "no equilibrium exists", since with a positive price the miner mass is positive and the empty purchase set cannot clear. Part 3 is stated as printed in the proposition, not as the proof's final display, which has the wrong sign for the low-price equilibrium.

The equilibrium is not defined as a root of equation (6): defining it that way would make part 1 empty. Purchase sets range over all measurable sets.

A complete development needs Gaussian integrals of exponentials over half-lines, strict log-concavity and tail limits of $\Phi$, and a two-root lemma for strictly log-concave functions vanishing at both ends. These are reusable beyond this mission. Contributions to any milestone, or to these Gaussian facts as separate lemmas, are welcome. The unobservable-fundamentals setting (Proposition 3) is not part of this mission.

Selected references

• M. Sockin and W. Xiong, A Model of Cryptocurrencies, preliminary draft, March 2018; published in Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4756
• N. Kiyotaki and R. Wright, A Search-Theoretic Approach to Monetary Economics, American Economic Review 83 (1993), 63–77. https://www.jstor.org/stable/2117496
• S. Morris and H. S. Shin, Unique Equilibrium in a Model of Self-Fulfilling Currency Attacks, American Economic Review 88 (1998), 587–597. https://www.jstor.org/stable/116850
• M. Bagnoli and T. Bergstrom, Log-concave probability and its applications, Economic Theory 26 (2005), 445–469. https://doi.org/10.1007/s00199-004-0514-4

Motivation

When a new durable product is launched, demand typically follows a diffusion curve. A few innovators buy on their own, and later buyers, the imitators, are drawn in by word of mouth from earlier adopters. Bass's diffusion model (Bass 1969) is the standard description of this process and is used throughout marketing and operations to forecast the sales of new products.

In a closed-loop supply chain the producer also collects products returned at the end of their use, remanufactures them and resells them, often at a higher unit margin than new items. Returns arrive only after units have been sold and used, so early in the life cycle there are few of them. Nadar, Kaya and Güler (MSOM 2021) ask whether a producer can gain by deliberately rejecting part of the demand early on. Rejection slows diffusion, but backlogged customers return later, when accumulated returns allow them to be served with higher-margin remanufactured units. Their Theorem 1 gives conditions under which this partial fulfillment is optimal, and conditions under which it is not.

This mission formalizes the second kind of condition, a sufficient condition for immediate fulfillment (meeting all demand in every period) to be optimal, together with the model it is stated in and the diffusion comparisons it rests on.

Setting

A producer sells over periods $t=1,\dots,T$. A sales plan chooses new-item sales $n_t$ and remanufactured-item sales $r_t$, with total sales $s_t=n_t+r_t$ and cumulative sales $S_1=0$, $S_t=\sum_{i<t}s_i$.

Diffusion. Only satisfied customers spread word of mouth. With market size $m$, coefficient of innovation $p$ and coefficient of imitation $q$, the diffusion demand in period $t$ is

$$d_t=\Bigl(p+\frac{qS_t}{m}\Bigr)(m-D_t),\qquad D_1=0,\quad D_t=\sum_{i<t}d_i .\tag{1}$$

When all demand is met, $S_t=D_t$ and (1) is the original Bass process $\widetilde d_t=(p+q\widetilde D_t/m)(m-\widetilde D_t)$.

Segments and backlogs. A fraction $\gamma_1=1-\gamma_2$ of arriving customers wants only new items. The remaining fraction $\gamma_2$ buys remanufactured items when available and new ones otherwise. A fraction $\alpha$ of unmet demand is backlogged one period and the rest is lost. The backlogs $b_{1t},b_{2t}$ of the two segments follow the two-case recursion (4) of the paper.

Returns. A fraction $\beta_i$ of the units sold in period $t$ comes back in period $t+i$. The return volume available for remanufacturing is $e_1=0$, $e_{t+1}=e_t-r_t+\sum_{i=1}^{t}\beta_is_{t+1-i}$ (6).

The producer's problem. Maximize $\sum_{t=1}^{T}[(p_n-c_n)n_t+(p_r-c_r)r_t]$ subject to

• $0\le s_t\le d_t+b_{1t}+b_{2t}$ (2);
• $0\le r_t\le\gamma_2d_t+b_{2t}$ (3);
• $0\le r_t\le e_t$ (5).

The standing assumptions are $p+q\le1$, $\sum_i\beta_i\le1$, $p_n>c_n$, $p_r>c_r$ and $p_r-c_r>p_n-c_n$.

Immediate fulfillment. The immediate-fulfillment plan meets all demand and serves remanufactured-item demand from returns as far as possible. Its return volume is $\widetilde e_t$, and it sells

$$\widetilde r_t=\min\{\widetilde e_t,\gamma_2\widetilde d_t\},\qquad \widetilde n_t=\widetilde d_t-\widetilde r_t .$$

Formalization targets

Goal: Theorem 1(a), first clause

If $\widetilde e_t\le\gamma_2\widetilde d_t$ for $t=1,\dots,T$, then $(\widetilde n,\widetilde r)$ is feasible, and every feasible plan $(n,r)$ satisfies

$$\sum_{t=1}^{T}\bigl[(p_n-c_n)n_t+(p_r-c_r)r_t\bigr]\le\sum_{t=1}^{T}\bigl[(p_n-c_n)\widetilde n_t+(p_r-c_r)\widetilde r_t\bigr].$$

The condition says that, under immediate fulfillment, returns never exceed remanufactured-item demand, so there is never a surplus of returns that delayed customers could absorb.

Milestones

1. §4.1, p. 7. The immediate-fulfillment plan is feasible, and run through (1)–(6) it gives $s_t=d_t=\widetilde d_t$, $S_t=D_t=\widetilde D_t$, zero backlogs and $\widetilde r_t=\min\{e_t,\gamma_2d_t\}$.
2. §4.1, p. 7. For a feasible class-(b) plan whose first rejection is before $T$, cumulative sales satisfy $S_t\le D_t$ through period $T+1$.
3. Lemma 2, p. 7. If a feasible plan first rejects demand in period $t_p<T$, then $D_t=\widetilde D_t$ for $t\le t_p+1$ and $D_t<\widetilde D_t$ afterwards, up to $T+1$; moreover, $D_T^-\ge D_T^+$.

Significance

The result separates the two forces in the paper. Lemma 2 says that rejection always costs diffusion, so its only possible benefit is a better use of returns. The goal shows that this benefit disappears when returns are scarce in every period. Theorem 1(b) and Corollary 1 then show that partial fulfillment can win when returns become abundant before the horizon ends. Together these results give a threshold structure that producers in fast-clockspeed industries, such as smartphones in the paper's numerical study, can check from the immediate-fulfillment trajectory alone.

The results are proved in the paper, with every proof in an online appendix. This mission produces machine-checked statements and, eventually, proofs of the fully posed part of Theorem 1 and of the diffusion comparisons beneath it. No part of this model has been formalized before. The discrete Bass process and the sales-dependent diffusion recursion are reusable for other diffusion-based sales-planning models.

Difficulty

The obvious argument compares profits period by period, and it fails. A feasible plan that rejects demand in some period can sell more than $\widetilde d_t$ in later periods, because backlogged customers return and because $D_T^+$ can be positive. Profit is therefore not dominated termwise. The comparison has to be made over cumulative quantities. One must control cumulative sales against the Bass trajectory along the whole horizon, through the nonlinear recursion (1). One must also control total remanufactured sales through the return recursion (6), whose lags $\beta_i$ couple every pair of periods. The backlog recursion (4) branches on the plan, which rules out a closed form.

Formalization scope

• Lean representation.
  • Parameters are a structure Params with real m p q alpha gamma2 pn cn pr cr, a horizon T : ℕ and beta : ℕ → ℝ. The standing assumptions are a predicate Standing.
  • A plan is a pair n r : ℕ → ℝ, read only on periods $1,\dots,T$.
  • $D$, $b$, $e$ and the immediate plan are defined by explicit recursions on the offset $k=t-1$. The original Bass process is its own definition module.
• Committed conventions.
  • $\gamma_1=1-\gamma_2$.
  • The second case of (4) is used as the "otherwise" branch. The two readings agree on plans satisfying (2)–(3).
  • The sign conditions $m>0$, $p>0$, $q>0$, $\alpha,\gamma_2\in[0,1]$ and $\beta_i\ge0$ are implicit in the paper and stated explicitly.
  • $n_t\ge0$ is not imposed, because the paper does not impose it.
  • Lemma 2's "otherwise" is read as $t_p+1<t\le T+1$.
  • $D_T^\pm$ sum over $t=1,\dots,T$.
• Ruled out.
  • The immediate-fulfillment plan and its profit are computed from the data, not taken as parameters.
  • The feasible set contains (5) and the backlog terms of (2)–(3).
  • Diffusion is driven by sales, not demand, and returns are computed from sales.
  • The goal asserts feasibility of the immediate plan, not only a profit inequality.
• Not formalized.
  • The second clause of Theorem 1(a), parts (b)–(c) and Proposition 1 depend on thresholds stated only in the paper's online appendix.
  • Lemma 1 concerns a case excluded by the standing assumptions.
  • Corollaries 1–5 concern model variants.
• Infrastructure needed. Finite sums over Finset.Icc/Finset.Ico, induction along the recursions, and monotonicity of $x\mapsto x+(p+qx/m)(m-x)$ on $[0,m]$. Contributions of auxiliary lemmas, such as nonnegativity of the Bass trajectory and $\widetilde D_t<m$, are welcome.

Selected references

• E. Nadar, B. E. Kaya, K. Güler, New-Product Diffusion in Closed-Loop Supply Chains, Manufacturing & Service Operations Management, Articles in Advance 2020 (issue 2021). https://doi.org/10.1287/msom.2019.0864
• F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969. https://doi.org/10.1287/mnsc.15.5.215

Motivation

Health insurers pay providers in one of a few ways, and the choice shapes what providers charge. Under variable payment (co-insurance) the patient pays a fixed fraction of the provider's price. Under reference pricing the insurer announces a cap $p^*$ for a procedure: the patient pays a fixed co-payment at any provider charging at most $p^*$, and in addition the whole excess above $p^*$ at a provider charging more. The authors motivate their model with the California Public Employees' Retirement System's reference-pricing program for knee and hip replacement (Nassiri, Adida and Mamani, 2022).

S. Nassiri, E. Adida and H. Mamani (Reference pricing for healthcare services, M&SOM 24(2), 2022; author manuscript SSRN 3176280) model the two payment systems as price games between competing providers whose patients choose by a multinomial logit rule, and compare the resulting equilibria. Their first comparison, Proposition 5, is about provider prices. Variable payment leads to higher prices than reference pricing exactly when the patient cost share is below a provider-specific threshold. This mission formalizes that result and the equilibrium characterizations it rests on.

Setting

Two providers, $j = 1, 2$, offer a procedure to $m > 0$ patients. Provider $j$ has a non-price attribute $a_j$, with $a_1 \le a_2$. Both providers have nonnegative treatment cost $c$, and every patient has price sensitivity $\gamma > 0$. The alternative to treatment has utility $u_0$. If the patient's out-of-pocket cost at provider $j$ is $o_j$, provider $j$'s market share is

$$S_j(P) = \frac{e^{a_j - \gamma o_j}}{e^{u_0} + \sum_{k=1}^{2} e^{a_k - \gamma o_k}},$$

where $P = (p_1, p_2)$ is the price vector. Provider $j$'s profit is $V_j(P) = m(p_j - c)S_j(P)$.

• Variable payment (VP) with cost share $\lambda \in (0,1]$: $o_j = \lambda p_j$.
• Reference pricing (RP) with reference price $p^*$ and co-payment $\tilde c < c$: $o_j = \tilde c + \max\{0, p_j - p^*\}$. Provider $j$ is value-based if $p_j \le p^*$.

Under each system the two providers choose prices simultaneously, and an equilibrium is a pure Nash equilibrium of that game: no provider can raise its own profit by changing only its own price. Each system also carries a standing assumption on best responses. Assumption 1 says that, as the rival's price tends to infinity, the limit $\bar S^{VP}_j$ of provider $j$'s share at its VP best response is at most $50\%$. Assumption 2 is the same condition under RP.

Formalization targets

Goal: Proposition 5

Assume, in addition, that the co-payment is below the reference price, $\tilde c < p^*$. Let $P^{RP}$ be an RP equilibrium. For each provider $j$ there is $\lambda^*_j \in (0,1]$ such that, for every $\lambda \in (0,1]$ and every VP equilibrium $P^{VP}(\lambda)$,

$$p^{VP}_j(\lambda) > p^{RP}_j \iff \lambda < \lambda^*_j .$$

The threshold is only claimed to exist; it is not given by a formula, and the statement fixes no constant.

Milestones

1. Theorem 1: the VP equilibrium is the unique solution of $1 - \gamma\lambda(p_j - c)(1 - S^{VP}_j(P)) = 0$, $j = 1,2$.
2. Lemma 2(a): VP equilibrium prices are strictly decreasing in $\lambda$.
3. As $\lambda \to 0$, VP equilibrium prices become arbitrarily large.
4. Proposition 2: a value-based provider prices at $p^*$.
5. Theorem 2: an RP equilibrium exists. Given its non-value-based set $\mathcal N$, it is the unique solution of $1 - \gamma(p_j - c)(1 - S^{RP}_j(P)) = 0$ on $\mathcal N$ with $p_i = p^*$ off $\mathcal N$.
6. Lemma 6: provider $j$ is value-based iff $1 - \gamma(p^* - c)(1 - S^{RP}_j(p_j = p^*, P_{-j})) \le 0$.
7. Proposition 3: if provider 1 is non-value-based, so is provider 2.
8. Case 1 of the proof of Proposition 5: if both providers are value-based under RP, then $p^{VP}_1 \le p^{VP}_2 < p^*$ at $\lambda = 1$.
9. Lemma 7 (final claim): for every $p_2 > c + 1/\gamma$, provider 1's RP best response to $p_2$ exceeds its VP best response at $\lambda = 1$.
10. At $\lambda = 1$, every VP equilibrium price is strictly below its RP counterpart.

Significance

The result. Proposition 5 sorts the two payment systems by cost share. When patients bear a small share of the price, co-insurance leaves providers free to charge more than they would under a reference-price cap. Above the threshold, co-insurance disciplines prices more than the cap does. The paper's later comparisons build on this price comparison: patient out-of-pocket and utility (Proposition 6), provider profit (Proposition 7) and insurer cost (Proposition 8). The equilibrium characterizations, Theorems 1 and 2, are also what the paper's numerical study computes with. Proposition 2 is the formal statement of shadow pricing: value-based providers charge exactly the cap.

The formalization. The result has a published proof but no machine-checked one. The paper cites external equilibrium results, leaves several inequalities to "some algebra", and does not separately state continuity of the VP equilibrium price in $\lambda$ (Nassiri, Adida and Mamani, Appendix D). A formal development pins down which hypotheses each step uses; the co-payment condition $\tilde c < p^*$ is one that the theorem's sentence omits. It also yields reusable facts about two-firm logit price competition.

Difficulty

The central difficulty is the comparison of equilibrium prices across two different games. Under RP, a provider's out-of-pocket charge changes formula at $p^*$, and its equilibrium status depends on the rival's price. Both providers may be value-based, both may be non-value-based, or only provider 2 may be non-value-based. In the second case, each best-response price depends on the other provider's price, so separate comparisons of the two providers' first-order conditions are insufficient. The VP equilibrium price must also vary continuously with $\lambda$ for the strict inequality to define a threshold; strict monotonicity alone does not establish that.

Formalization scope

All quantities are real numbers. Providers are Fin 2, and index 0 is the paper's provider 1. Prices range over $\mathbb R$ instead of the paper's $p_j > c$. This does not change the equilibria: an equilibrium price earns positive profit, and any price at or below $c$ earns non-positive profit. Equilibrium is the published generic pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every price set equal to $\mathbb R$. "Value-based" is read as $p_j \le p^*$, following Proposition 2. The standing assumptions are $m > 0$, $\gamma > 0$, and $c \ge 0$ (implicit in the paper), $a_1 \le a_2$ and $\tilde c < c$. The nonnegative cost bound is needed: negative treatment cost can make VP equilibrium prices rise with $\lambda$, contradicting Lemma 2(a). Assumptions 1 and 2 are encoded as follows: best responses exist, and along every best-response selection the share converges, as the rival's price tends to infinity, to a limit of at most $1/2$. The goal assumes Assumption 1 at every $\lambda \in (0,1]$, and it adds $\tilde c < p^*$, which the proof uses and without which the statement fails numerically. "As $\lambda$ approaches 1" in the proof is read as the value at $\lambda = 1$.

The goal is stated about the Nash equilibria of both games and quantifies over every VP equilibrium at every $\lambda$. A version about solutions of the first-order systems would bypass Theorems 1 and 2 and is not the target. Neither is "VP is higher for small $\lambda$ and lower at $\lambda = 1$", which is only milestones 3 and 10.

A complete development needs: derivative and quasi-concavity facts for logit shares in one's own price; existence of an equilibrium in a two-player game with continuous, quasi-concave payoffs on compact price intervals; uniqueness for the logit first-order system; implicit-function continuity of the equilibrium in $\lambda$; and the RP case analysis. The logit and quasi-concavity lemmas are reusable for any logit price competition model. Proofs of individual milestones, and alternative arguments, are welcome.

Selected references

• S. Nassiri, E. Adida, H. Mamani, Reference pricing for healthcare services, Manufacturing & Service Operations Management 24(2), 2022. Published article; author manuscript, SSRN 3176280.

Motivation

People receive both informative reports and messages that are unrelated to the truth. A standard question in social learning is whether sharing beliefs helps a population identify the correct state. The question changes when everyone knows misinformation exists but does not know its ideological direction. Mostagir and Siderius study this setting and show that the ranking of two learning rules changes with the amount of misinformation: Bayesian updating can be at least as reliable at low levels, while simple averaging is more reliable at sufficiently high levels under full support. Their result is stated as Theorem 1 of the SSRN working paper, later published in Management Science.

The comparison matters for models of collective decisions because the same population, news quality, and misinformation distribution can lead to different rates of wrong terminal actions solely because the agents process others' beliefs differently. The paper's question is therefore about the behavior of learning rules, not just the accuracy of any one message. The mission covers the paper's regime comparison; its separate results on hazard rates, polarization, and targeting are outside this target.

Setting

The unknown state $\theta$ is either $L$ or $R$. An organic message matches the state with probability $p>1/2$. A fraction $q<1/2$ of all messages consists of misinformation. Its split $r\in[0,1]$ is the fraction of misinformation advocating $R$; $r$ has distribution $F$ with density $f$. Agents start with heterogeneous prior probabilities $x\in[0,1]$ of state $R$, distributed according to a continuous law $H$. The paper assumes these priors and the split are independent. All comparisons concern the limit of a large population, where the observed fraction of each message type is determined by $\theta$ and $r$ (§2, pp. 4–6).

A DeGroot agent first updates on her own message while treating it as organic, using equations (1) and (2) of the paper. Thereafter agents average one another's beliefs. In the large-population model used by the proof, every agent reaches the same consensus $\pi_\infty(\theta,r)$: the $H$-average of the two face-value posteriors, weighted by the fractions of $R$ and $L$ messages. A Bayesian agent treats misinformation as possible and infers the message shares from the population's beliefs. The same observed share can be explained by the true state and split or by the other state with a different split. The posterior $\pi_B(\theta,r,x)$ weighs these two narratives according to their densities under $F$ and the agent's prior $x$ (proofs of Lemmas 1–2, pp. 18–19).

An agent's terminal action favors whichever state has posterior belief at least one half. A society mislearns at $(\theta,r)$ when a positive $H$-mass of agents favors the wrong state; for DeGroot agents, who share a consensus, this is a single belief comparison. Write $P_B(\theta)$ and $P_D(\theta)$ for the $F$-probabilities of Bayesian and DeGroot mislearning. The paper studies both true states; the formulas for $R$ mirror those for $L$.

Formalization targets

The main target is Theorem 1, p. 10. For every $1/2<p\leq1$, set

$$q^*=\frac{2p-1}{2p}.$$

For every continuous symmetric prior law $H$ on $[0,1]$ and every split law $F$ supplied by a density, the goal compares both states separately:

$$\begin{aligned} 0<q<q^*&\quad\Longrightarrow\quad P_B(\theta)\leq P_D(\theta),\\ q^*<q<\tfrac12,\quad H,F\text{ fully supported on }[0,1] &\quad\Longrightarrow\quad P_D(\theta)<P_B(\theta), \end{aligned} \qquad\theta\in\{L,R\}.$$

The first comparison is non-strict because both mislearning probabilities can be zero, although the preprint uses the word “lower.” The value of $q^*$ comes from the paper's proof, which states the result with an existential threshold. The five milestones state the DeGroot and Bayesian mislearning cutoffs, the necessary misinformation level for Bayesian mislearning, the cutoff difference, and the resulting full-support probability formulas. Their source text and page numbers accompany the individual items.

Significance

The theorem isolates a regime in which adding misinformation changes the relative performance of the two learning rules. Under full support, the high-misinformation conclusion is strict: some split realizations cause Bayesian society to mislearn even while DeGroot society learns. The low-misinformation conclusion gives a uniform comparison over every allowed distribution of the split, without requiring its full support (Theorem 1 and proof, pp. 10, 20). These are statements about society-level mistakes, not a claim that an individual averaging rule is always more accurate.

The result has a published mathematical proof. It does not yet have a machine-checked proof in this development. Formalizing it requires a reusable interface for two-state misinformation models: a law of heterogeneous priors, a density for the split, the two narrative splits, posterior beliefs, and mislearning events. Those objects can also support the paper's later questions about the distributional shape of misinformation and the choice of targeting policy.

Difficulty

The obvious comparison of the two update rules at a fixed message fails to settle the result. DeGroot agents act on an average of face-value posteriors; Bayesian agents act on an agent-specific posterior after considering competing explanations of the same population message share. Thus the two groups can be wrong for different split realizations, and a statement about one representative belief does not give a society-level mislearning probability. The comparison must also distinguish a pointwise mistake at the edge of the split support from an event of positive probability. A second issue is that the converse direction of the printed Lemma 2 assumes agents with beliefs arbitrarily close to the extremes, which requires full prior support on $[0,1]$ (Lemma 2 and proof, p. 19).

Formalization scope

Lean uses the paper's large-population formulas directly: $\pi_\infty$ is an integral over $H$, and $\pi_B$ is a density-weighted posterior over the two narrative splits. The Bayesian terminal belief is its period-two posterior; later observations add no information in this model. $H$ is a probability measure concentrated on $[0,1]$ with no atoms. $F$ is given by a measurable nonnegative real density whose integral is one and whose support lies in $[0,1]$. Full support on an interval means that the density is bounded below there by a positive constant and is zero outside. Symmetry means invariance of $H$ under $x\mapsto1-x$.

The formalized regime has $0<q<1/2$ so the cutoffs involving division by $q$ are defined as intended; the paper's misinformation-free case $q=0$ is an example outside this theorem. A belief of exactly $1/2$ counts as wrong, matching the weak cutoff inequalities. Mislearning for Bayesian society requires a positive $H$-mass of wrong agents, and the final probabilities are extended nonnegative real measures of split events. The real posterior's zero-denominator default can arise outside the split support, which carries zero $F$-mass; pointwise Bayesian milestones restrict $r$ to the support.

The model defines mislearning from posterior beliefs and the law of $r$, so the main theorem cannot be reduced to a comparison of cutoff formulas by definition. Solver contributions may establish measurability and integrability facts for the model, the cutoff lemmas, and the final comparison. The standing interval-support assumptions in the paper are narrowed to $[0,1]$ where the theorem needs them; the main comparison does not fix arbitrary smaller support intervals.

Selected references

• Mostagir, Mohamed, and James Siderius. Learning in a Post-Truth World. SSRN working paper 3879174, version of 2 July 2021; published in Management Science 68, 2022. SSRN preprint. The mission cites the preprint's page and theorem numbering.

Motivation

An advance market commitment (AMC) is a promise to pay for a product if it is developed and supplied. For vaccines intended for low-income countries, a donor may use an AMC to encourage a manufacturer to invest before demand is certain. The investment decision happens before the firm and donor negotiate actual purchases. This timing creates a hold-up problem: once capacity is sunk, the firm receives only its negotiated share of the benefit from using it. Kremer, Levin, and Snyder analyze which commitments change that incentive in Designing Advance Market Commitments for New Vaccines. This mission concerns their framework AMC, in which a donor puts money in an interest-bearing escrow fund that pays a subsidy per vaccine until exhausted.

The result is specific to a temporary subsidy and a monopoly firm. It explains why depositing money in an escrow can transfer value to the firm without raising its chosen capacity. The paper also studies perpetual subsidies, supply commitments, forcing contracts, competing firms, and products farther from development. Those are different designs or regimes; their results are outside this mission.

Setting

A country receives a flow health benefit $B(q)$ when $q$ citizens per period receive a vaccine. The benefit starts at $B(0)=0$, increases, and is strictly concave; its marginal benefit tends to zero as output grows. A donor values this benefit at fraction $\alpha\in(0,1)$ and pays for the vaccine. Its inverse demand is $P(q)=\alpha B'(q)$, with choke price $\bar p=P(0)$ and demand curve $D(p)$ at positive price $p$. Production costs $c>0$ per vaccine per period. The firm pays $KQ$ before trade to install capacity $Q$, and can produce at most $Q$ in any period. Everyone discounts future flows at rate $r>0$; write $\kappa=rK$ for the flow equivalent of unit capacity cost. The paper maintains $c+\kappa<\bar p$, so the integrated benchmark invests positive capacity. These assumptions and the interpretation of the donor and firm are from the BFI working-paper version, §§2–3.

After investment, the firm and donor bargain over vaccine purchases. Either can block trade, so both threat payoffs are zero. Efficient Nash bargaining chooses the output plan that maximizes their discounted joint surplus, and the firm receives fraction $\beta\in(0,1)$ of that surplus. The firm anticipates this bargain when it chooses capacity. Without an AMC, denote its equilibrium capacity by $Q^{\mathrm{NA}}$; with integrated control, denote the optimum by $Q^{\mathrm{IN}}$. The paper's first two propositions identify these benchmarks:

$$Q^{\mathrm{IN}}=D(c+\kappa),\qquad Q^{\mathrm{NA}}=D(c+\kappa/\beta)<Q^{\mathrm{IN}}.$$

Under the framework AMC, the donor fixes a subsidy $s>0$ and deposits $F>0$ in escrow before the firm chooses $Q$. The escrow earns interest at the same rate $r$ as the participants' discounting. A subsidy $s$ is paid for each vaccine during the AMC period. If output is $q^A$ and $sq^A>rF$, the fund is exhausted at a finite time $T$; afterwards there is no subsidy. The bargain chooses both AMC-period output $q^A$ and tail output $q^T$, each bounded by capacity. If $sq^A\leq rF$, the subsidy is perpetual at that output and there is no tail period. This branch matters when evaluating capacities the firm could have chosen instead.

Formalization targets

The core comparison is the paper's Proposition 3. For any framework AMC whose equilibrium subsidy is temporary,

$$Q^{\mathrm{TS}}=q^A=q^T=D(c+\kappa/\beta)=Q^{\mathrm{NA}}=q^{\mathrm{NA}}.$$

The goal covers every qualifying equilibrium. It also asserts that the displayed candidate is an equilibrium whenever $sD(c+\kappa/\beta)>rF$, so the claim cannot hold merely because no temporary-subsidy equilibrium exists. It fixes the policy terms but does not assume the firm's capacity or bargained outputs in advance.

The milestones establish the inverse-demand property (Lemma 1), the integrated and no-AMC benchmarks (Propositions 1–2), the fund accounting identity (6), the discounted joint-surplus identity (7), full capacity utilization in the temporary regime, and the firm's ex ante profit identity (8). The last identity identifies the fund's contribution as $\beta F$ on that regime. Their statements and numbering follow the December 2020 BFI working paper, with printed pages 6 and 10–13 and Appendix A, pages 37–38.

Significance

Proposition 2 measures the capacity lost to hold-up when a firm cannot keep all returns to investment. Proposition 3 then shows that this particular escrow design does not repair that loss when its subsidy is temporary: the fund changes the firm's payoff level while leaving the capacity choice at the no-AMC benchmark. That conclusion helps distinguish an AMC's payment amount from its effect on investment incentives. The paper's other contract designs address separate policy questions and should not be inferred from this result.

The formalization produces a reusable discounted-flow definition and a concrete capacity-and-bargaining game with an interest-bearing escrow. The source result has a paper proof; the Lean theorems here are proposed proof obligations, with no machine-checked proofs claimed. A complete development would verify the inverse-demand construction, existence and uniqueness of the relevant maxima, the escrow integral, and equilibrium optimality on both finite and perpetual subsidy branches.

Difficulty

The firm's value cannot be calculated by assigning full output at the outset. Bargaining chooses output after capacity is installed, and using fewer vaccines during the AMC period lengthens the subsidy period. Thus the escrow duration changes with the bargained output. The simple capacity comparison from the no-AMC benchmark only becomes applicable after the output and fund identities have been established. Moreover, the firm's alternative capacities can cross from a finite subsidy period to a perpetual one, so a statement proved only for the candidate equilibrium branch does not settle its investment choice.

Formalization scope

All amounts, times, and discounted values are real. Discounted flows are Lebesgue set integrals over positive time; an open interval $(0,T)$ represents the AMC period, with endpoint choices irrelevant to its integral. Demand is the real infimum of nonnegative quantities at which $P(q)\leq p$. Its value at nonpositive prices is a Lean default and is never used in a result. The firm's value is $\beta$ times the real supremum of feasible joint-surplus values minus $KQ$; feasible output intervals are nonempty for admissible capacities, and the intended values are bounded and attained. Capacity is chosen over $Q\geq0$.

The Lean benefit function is twice continuously differentiable on all of $\mathbb R$, extending the paper's half-line convention so derivatives at zero are unambiguous; its sign assumptions are only for $q\geq0$. Output is constant within the AMC and tail periods, following the paper's equation (A8) reduction. “Temporary” means $sq^A>rF$ at equilibrium. The model separately represents a perpetual subsidy for deviations. The framework profit is defined from bargained joint surplus and its discounted flows; equation (8) is a theorem target, and output is a bargain choice rather than a fixed capacity value. These choices keep the formal goal about the paper's investment game.

The development needs real derivatives, inverse functions, concavity, filters for the bargaining-weight limits, Lebesgue integrals of exponential flows, real suprema on compact feasible boxes, and optimization over nonnegative capacities. The discounted-flow and capacity-game infrastructure can be reused in other procurement models. Contributions that establish these interfaces or close any listed milestone support the goal.

Selected references

• Michael Kremer, Jonathan Levin, and Christopher M. Snyder, Designing Advance Market Commitments for New Vaccines, Becker Friedman Institute Working Paper No. 2020-175, December 2020; published in Management Science 68(6), 2022. DOI: 10.1287/mnsc.2021.4163. The mission's theorem labels and page numbers refer to the working-paper PDF.

Motivation

A manufacturer that sells through an independent retailer charges a wholesale price above cost, and the retailer then adds its own margin: the double marginalization problem of vertical contracting. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period monopoly chain the retailer can blunt this by buying more than it sells in the first period and carrying the excess into the second. This strategic inventory makes the retailer less dependent on the manufacturer's next wholesale price, which forces that price down, and in their model both firms gain.

Li, Li and Chen (SSRN 3003887; Manufacturing & Service Operations Management, 2021) ask whether the conclusion survives when two such chains compete. Their answer is that strategic inventory still arises, but under fierce enough competition it hurts every firm. The mission formalizes that result.

Setting

There are two supply chains $i \in \{1,2\}$; $j$ denotes the rival chain. Each consists of a manufacturer with zero production cost and an exclusive retailer. There are two periods $t = 1,2$. In period $t$ the demand for product $i$ is

$$D_{it} = 1 - p_{it} + \theta\,(p_{jt} - p_{it}),$$

where $p_{it}$ is retailer $i$'s price and $\theta > 0$ measures the intensity of chain-to-chain competition.

The game has four stages. In stage 1 each manufacturer sets a wholesale price $w_{i1}$. In stage 2 each retailer sets $p_{i1}$ and orders enough to cover demand plus a carryover $I_i \ge 0$, held into period 2 at unit holding cost $h \ge 0$. In stage 3 each manufacturer sets $w_{i2}$. In stage 4 each retailer sets $p_{i2}$ and orders whatever demand its carryover does not cover; unsold units are worthless.

Contracts are unobservable: firms of chain $j$ see neither $w_{it}$, nor the orders of chain $i$, nor $I_i$. The equilibrium is a perfect Bayesian equilibrium with passive beliefs. At every history of its own chain, a firm keeps believing that the rival charges its equilibrium-path prices $p_{j1}^*, p_{j2}^*$, and acts optimally given that belief and the continuation play of its own chain.

Two games are compared. In the SI game each chain may carry any $I_i \ge 0$. In the NI benchmark, "a manufacturer only delivers whatever its downstream retailer can sell", so $I_i = 0$. Manufacturer $i$'s profit is $\Pi_i = w_{i1}(D_{i1} + I_i) + w_{i2}(D_{i2} - I_i)^+$. Retailer $i$'s profit $\pi_i$ is its revenue minus its wholesale bills minus $h I_i$.

Formalization targets

Goal: Proposition 2

Let $0 \le h < 1/4$. There is $\theta_0 \ge 0$ with $\theta_0 < 1/h - 4$ such that for every $\theta_0 < \theta < 1/h - 4$, every SI equilibrium $E$ and every NI equilibrium $E'$ satisfy

$$\Pi_i(E) < \Pi_i(E') \quad\text{and}\quad \pi_i(E) < \pi_i(E') \qquad (i = 1,2),$$

and equilibria of both games exist. Conversely, if $h \ge 1/4$ or $\theta \ge 1/h - 4$, no strategic inventory is carried in any SI equilibrium. The goal leaves $\theta_0$ unspecified, as the paper does: it asserts the shape of the comparison, not a numerical threshold.

Milestones

1. §3.1 display, p. 10. When the retailer replenishes in period 2, its price response is $p_{i2} = (1 + \theta p_{j2} + (1+\theta) w_{i2})/(2(1+\theta))$, so $\partial D_{i2}/\partial w_{i2} = -\tfrac12(1+\theta)$.
2. Table 1, right column, p. 9. The NI equilibrium, which is also the SI equilibrium when $h > 1/(4+\theta)$: $w = 2/(4+\theta)$, $p = 3/(4+\theta)$, $\Pi_i = 4(1+\theta)/(4+\theta)^2$, $\pi_i = 2(1+\theta)/(4+\theta)^2$.
3. Table 1, left column, p. 9. The SI equilibrium for $h \le 1/(4+\theta)$, row by row. It includes $I_i = (1+\theta)(20+7\theta)(1-h(4+\theta))/((2+\theta)(68+19\theta))$ and the manufacturer's profit.
4. Proposition 1(i), p. 9. $I_i > 0$ in equilibrium if and only if $h < 1/(4+\theta)$.
5. Proposition 3(i), p. 15. The manufacturers' equilibrium profit is strictly increasing in $h$ on $[17(4-\theta)/(272+136\theta+21\theta^2),\ 1/(4+\theta)]$.
6. Proposition 3(ii), p. 15. The same holds for the retailers' profit on $[(1888+1424\theta+242\theta^2-35\theta^3)/(9728+11456\theta+5344\theta^2+1148\theta^3+98\theta^4),\ 1/(4+\theta)]$.

Significance

The result. Proposition 2 overturns the monopoly-chain conclusion. Carryover still lowers the second-period wholesale price, but under competition that lower price feeds a fiercer price war between the chains, and the gain from softened double marginalization is lost. Because contracts are unobservable, no chain can commit to holding no inventory, so the firms end up in a situation every one of them would prefer to avoid. Proposition 3 sharpens the point: near the threshold $h = 1/(4+\theta)$ a higher holding cost raises every firm's profit. A carrying cost, normally a pure loss, here acts as a commitment device.

Formalizing it. The paper's proofs are in an online appendix, which is not part of the source; the equilibrium notion is named on p. 8 but not written out. A machine-checked proof would supply both. It would pin down the equilibrium concept: what a passive-beliefs perfect Bayesian equilibrium of a two-chain, four-stage game is. It would establish that Table 1 is the unique equilibrium outcome, including against asymmetric profiles. It would derive the retailer's SI profit, which the page does not print. None of these results has a machine-checked proof.

Difficulty

Each stage payoff is piecewise quadratic, with kinks where demand reaches zero and where carryover covers period-2 demand. Table 1 must be shown optimal against all deviations, not only local ones, at every off-path history of a chain: a retailer that deviates in its carryover changes its own manufacturer's second-period price, and that response has to be the equilibrium one there too. The tempting shortcut is to solve the first-order conditions of a symmetric profile and stop. It establishes neither global optimality nor that asymmetric equilibria share Table 1's outcome. The goal quantifies over every equilibrium of both games, so both are needed.

Formalization scope

The model is a single definitions file, ChainCompSI.Backfire.Model. It has the following parts:

• demand, and sales $= \max(D, 0)$;
• own-chain histories Hist and pure profiles Profile with one strategy per stage;
• the stage payoffs;
• the equilibrium predicate IsEq θ h si E, where si : Fin 2 → Bool selects SI or NI per chain;
• the on-path accessors w1, p1, inv, w2', p2', D1, D2;
• the realized profits mfrProfit ($\Pi_i$) and retProfit ($\pi_i$).

Chains are Fin 2, with rival 1 - i. All quantities are real.

The formalization commits to the following conventions, each disclosed in the items:

• Wholesale and retail prices are nonnegative. With a negative first-period wholesale price the retailer would want unbounded carryover, and no equilibrium would exist.
• Sales are demand truncated at zero.
• The first-period order is placed against realized demand: the retailer chooses its carryover $I_i$ and orders $D_{i1}^+ + I_i$. This is the reading under which Table 1 is the equilibrium.
• Passive beliefs mean that, at every own history, the rival's prices are taken to be its on-path prices. Each stage is optimal at every own history: stage 4 and stage 3 at every history with $I_i \ge 0$, stage 2 at every $w_{i1} \ge 0$.
• Profits are realized profits at both chains' on-path prices, and the retailer's profit includes $h I_i$.
• The condition $\theta < 1/h - 4$ is written as $h(4+\theta) < 1$. This keeps the page's case $h = 0$, where the bound is $+\infty$; in Lean, $1/0 = 0$.

Every statement of the form "in equilibrium, …" also asserts that an equilibrium exists, so none holds vacuously. The goal is stated about equilibria of the games, not with Table 1's closed forms substituted. A version comparing the two columns' rational functions would be a lemma of the proof, not Proposition 2.

Not formalized:

• Proposition 1(ii) (the threshold $\hat\theta$) and Corollaries 1–3;
• Proposition 4, which needs the asymmetric SI/NI equilibrium of the unpublished appendix; the per-chain si flag leaves room to pose it later;
• the observable-contracts and quantity-competition variants of §5.

Contributions welcome:

• proofs of the milestones;
• a reusable lemma that a strictly concave piecewise-quadratic stage payoff has a unique maximizer;
• a contraction argument for uniqueness of the equilibrium outcome.

Selected references

• X. Li, Y. Li, Y.-J. Chen, Strategic Inventories under Supply Chain Competition, Manufacturing & Service Operations Management, 2021; author's copy SSRN 3003887. https://ssrn.com/abstract=3003887, doi:10.1287/msom.2020.0954
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1070.0767
• R. P. McAfee, M. Schwartz, Opportunism in Multilateral Vertical Contracting: Nondiscrimination, Exclusivity, and Uniformity, American Economic Review 84(1), 1994. https://www.jstor.org/stable/2117975
• T. W. McGuire, R. Staelin, An Industry Equilibrium Analysis of Downstream Vertical Integration, Marketing Science 2(2), 1983. https://doi.org/10.1287/mksc.2.2.161

Motivation

An online platform can know more about a product than a customer arriving for a short sales campaign. It sees earlier customers' purchase decisions and the messages it sent them, while a new customer sees only her own message and private assessment. Choosing what to disclose can raise immediate sales, but a customer's response can also reveal information that improves later messages. Küçükgül, Özer and Wang study this tension for a fixed-price campaign and reduce the platform's dynamic information-design problem to a linear program in their submission manuscript, §§3–4, pp. 7–18.

The mission concerns that reduction, stated as Proposition 5 and equations (9)–(11) of the November 2019 submission manuscript. Its original problem permits a message distribution that depends on the full private history. Its optimization variables after reformulation instead track an integer summary and three possible recommendations. The gap between those two descriptions is the main mathematical content that a formal proof must justify.

Setting

A time-locked sales campaign has $T$ customers arriving one after another at a fixed price $p\in(0,1)$. The product value $V$ is either $0$ or $1$, with common prior $\Pr(V=1)=v_0\in[0,1]$. Customer $t$ observes a private signal $S_t\in\{1,-1\}$; conditional on $V$, signals are independent, and $\Pr(S_t=1\mid V=1)=\Pr(S_t=-1\mid V=0)=q$ for $q\in(1/2,1]$. She receives one message $m_t$ from the platform, then buys when her posterior value reaches $p$, with equality resolved in favor of buying. These are the primitives of §3 and equations (1)–(2) of the manuscript.

An information provision policy $\sigma$ selects a distribution over messages using the platform's history $H_t=((m_s,a_s):s<t)$ of earlier messages and purchase decisions. The customer does not see that history. The platform's expected revenue is $R(\sigma)=p\sum_{t=1}^T\Pr_\sigma(a_t=1)$. The target value $\pi^\star$ is the best revenue over all such policies in equation (3), not a value assigned by the reduced program.

Two belief thresholds determine how a message affects buying: $v^*=p(1-q)/(p(1-q)+(1-p)q)$ and $v^{**}=pq/(pq+(1-p)(1-q))$. A recommendation policy uses messages $1$, $0$, and $-1$ to recommend buying, following the private signal, and declining. The net purchase position $N(H_t)$ counts purchases minus non-purchases among customers given the neutral recommendation. Section 4 defines $v_n=\Pr(V=1\mid N(H_t)=n)$ and $u_n=\Pr(S_t=1\mid N(H_t)=n)$. This turns the history distribution into masses $z_t(n)$ and the message probabilities into $r_t^i(n)$, where $i\in\{1,0,-1\}$. The linear-program variables are their products $y_t^i(n)=z_t(n)r_t^i(n)$; see Propositions 1–5, pp. 11–18.

Formalization targets

Original policy value and the reduced programs

For parameters in the paper's focus region $v^*\le v_0<v^{**}$, the goal states a common value for the original policy problem, recommendation formulation (9), and LP (11):

$$\sup_\sigma R(\sigma) =\max_{(r,z)\text{ feasible for (9)}}p\sum_{t=1}^T\sum_n z_t(n)\bigl(r_t^1(n)+u_nr_t^0(n)\bigr) =\max_{y\text{ feasible for (11)}}p\sum_{t=1}^T\sum_n\bigl(y_t^1(n)+u_ny_t^0(n)\bigr).$$

The goal also says that every LP optimum recovers an optimum of (9) through equation (10), taking any probability vector of recommendations where $z_t(n)=0$. The first two maxima include attainment. The original-policy value is expressed as a supremum because the manuscript's weak incentive inequalities permit endpoint ties that may change the customer's actual response under (2); this reading is disclosed in the paper's Proposition 5 and proof, pp. 18, 42–43.

The milestones trace the source's claims: Proposition 1 classifies buying behavior; Proposition 2 restricts attention to recommendations; Proposition 3 identifies the net purchase position as a sufficient statistic; equation (9) states the original-to-reduced value identity; and equations (B.17)–(B.18) express the two directions between (9) and (11). Proposition 4's random-walk identity remains in the definition of feasibility for (9) and (11), though it is not a separate milestone in this proposal.

Significance

Proposition 5 replaces a search over history-dependent information policies with a finite linear program whose variables have the interpretation of joint state-and-recommendation probabilities. For a fixed campaign length, the LP has $3T(2T-1)$ variables before redundant positions are removed. This gives the computational representation used in the paper's later numerical comparison and recommendation-policy examples; see §4.3, pp. 18–20.

The result is proved in the authors' manuscript. The local Lean files for this mission compile as statements with proof placeholders; they do not yet contain machine-checked proofs. Completing the mission would provide a checked bridge from a sequential Bayesian policy model to its reduced finite-state program and LP, with reusable definitions for the joint law, Bayesian response, and state evolution.

Difficulty

The change of variables $y_t^i(n)=z_t(n)r_t^i(n)$ is only the final step. The difficult claim is that optimizing over full proprietary histories and arbitrary messages gives the value of a program whose policy uses only three recommendations and the integer $N(H_t)$. A receiver's choice is endogenous: the message affects what she believes, her private signal affects whether she buys, and the platform observes the resulting decision. Defining customer behavior as automatic obedience would erase that difficulty. The paper's endpoint inequalities add another issue: at equality a nominal recommendation can differ from the purchase rule, so value comparison must keep the tie convention visible. These are the distinctions between equations (2), (3), (9), and (11) of the manuscript.

Formalization scope

The Lean model uses real probabilities, a Boolean product value, Boolean signals and purchase decisions, and SignType for the three recommendations. It builds the joint distribution of $V$ and the proprietary history one customer at a time. Every customer buys by the joint-probability form of rule (2), including a tie; obedience is a property checked on realized signal–message pairs. Histories of length $t$ precede paper customer $t+1$, while (9) and (11) keep the source's one-based time index. The state range is $n=-(T-1),\ldots,T-1$, with zero mass outside and zero boundary terms in the recursions.

The policy class has an arbitrary finite message type. This matches the sums over histories in Appendix B and includes the three-message policies. The assumptions retain $q=1$, $v_0=0$, and $T=0$ when allowed by the stated region; the definition of $v_n$ uses a two-sided product expression so a negative exponent never acts on zero. The reduced programs use exactly the four printed weak incentive inequalities. State masses are nonnegative, as required by their meaning as probabilities. Real-number maxima are stated with IsGreatest, and the original-policy supremum with IsLUB; no default value of a real sSup is used.

The original-policy value is taken over all information policies with Bayesian response, rather than being defined by (9). The source's correction at $v^*$, the interpretation of recommendation obedience, the finite-message restriction, and the supremum reading are explicit audit points. A full development needs finite probability calculations, conditional belief identities, and equivalence between histories and net positions. The model and these supporting lemmas can be reused for later formal work on sequential persuasion in the same paper.

Selected references

• C. Küçükgül, Ö. Özer, and S. Wang, Engineering Social Learning: Information Design of Time-Locked Sales Campaigns for Online Platforms, submission manuscript, November 2019; published in Management Science, 2022. DOI: 10.1287/mnsc.2021.4151.

Motivation

Many service providers can infer how long a customer's request will take when the customer shares personal information. A customer who withholds that information may instead enter a queue as an unidentified request. Hu, Momot, and Wang study the resulting conflict between an individual's choice to disclose and the waiting times experienced by the whole customer population in a single-server system. Their comparison asks whether giving customers control over disclosure improves total customer surplus relative to a rule requiring full disclosure. The answer depends on which jobs the provider gives priority, even though the provider keeps the same priority order among identified and unidentified requests. Hu, Momot, and Wang, §3–4

The manuscript distinguishes shortest-processing-time priority (SPT), where the identified high-priority type has a shorter mean service time, from longest-processing-time priority (LPT), where it has a longer one. This distinction makes privacy control a queueing question as well as an information-choice question: withholding changes a request's priority class, so it changes waiting times for other customers. Theorem 1 gives the direction of the population-level comparison in both regimes. Hu, Momot, and Wang, Theorem 1, p. 15

Setting

Requests reach one server according to a Poisson process of rate $\lambda$. A request has type $H$ with probability $\alpha$ and exponential mean service time $1/\mu$, or type $L$ with probability $1-\alpha$ and mean $1/(\sigma\mu)$. The rate parameter $\sigma$ is positive and differs from one. The average service rate of the combined population is $\bar\mu=\sigma\mu/(1+\alpha(\sigma-1))$, and stability requires $\lambda<\bar\mu$. The manuscript also assumes a service reward $R$ at least $c/\bar\mu$, where $c$ is the cost per unit of time spent in the system. These are the parameters of the two-type service model. Hu, Momot, and Wang, §3.2, p. 8

Each customer chooses whether to disclose before observing the request type. If the fraction that discloses is $\gamma\in[0,1]$, disclosed type-$H$ requests arrive at rate $\alpha\gamma\lambda$, disclosed type-$L$ requests at rate $(1-\alpha)\gamma\lambda$, and undisclosed requests at rate $(1-\gamma)\lambda$. The latter form a type-$N$ class with a mixture of the two service-time distributions. The server uses preemptive priority in the fixed order $H>N>L$. For each class, $W_H$, $W_N$, and $W_L$ denote its mean time in the system, including service. The values are determined by the three-class formulas in Online Appendix A.1. Hu, Momot, and Wang, §3.3–3.4 and Online Appendix A.1

An infinitesimal customer compares the utility of disclosure, $U_d(\gamma,\lambda)=R-c(\alpha W_H+(1-\alpha)W_L)$, with that of withholding, $U_w(\gamma,\lambda)=R-cW_N$. The total customer surplus at population strategy $\gamma$ is

$$CS(\gamma)=\lambda\bigl(\gamma U_d(\gamma,\lambda)+(1-\gamma)U_w(\gamma,\lambda)\bigr).$$

An equilibrium disclosure probability $\gamma^*$ is an endpoint supported by the appropriate strict utility comparison, or an interior point where the two utilities agree and their difference decreases nearby. The manuscript chooses the Pareto-dominant equilibrium when several exist. Hu, Momot, and Wang, Eq. (1), p. 10; equilibrium definition, p. 12; Eq. (9), Online Appendix p. 3

Formalization targets

Theorem 1: customer control versus full disclosure

Let $CS_{\rm control}=CS(\gamma^*)$ and $CS_{\rm discl}=CS(1)=\lambda U_d(1,\lambda)$. The target is

$$\sigma<1\Longrightarrow CS_{\rm control}\le CS_{\rm discl},\qquad \sigma>1\Longrightarrow CS_{\rm control}\ge CS_{\rm discl}.$$

When $\gamma^*<1$ and $\alpha>0$, the corresponding inequality is strict. The first regime is SPT and the second is LPT: under the fixed ranking $H>N>L$, type $H$ has the shorter mean service time exactly when $\sigma<1$. The comparison holds for any equilibrium satisfying the paper's equilibrium conditions, including its Pareto-dominant selection. Hu, Momot, and Wang, Theorem 1, p. 15

Supporting results

The mission includes Lemma 1's closed forms for $U_d$ and $U_w$, the closed form of $CS$ and the auxiliary function $\Gamma$ in the proof of Lemma 4, its derivative and denominator-sign statements, and Lemma 4's monotonicity of $CS$ on $[0,1]$. Those statements connect the queueing model to the social comparison without replacing the final claim by a special case. Hu, Momot, and Wang, Lemma 1, p. 12; Lemma 4, Online Appendix p. 3; proof of Lemma 4, Online Supplement p. 2

Significance

Theorem 1 identifies a precise direction for the welfare effect of control over request-type information in this model. Under SPT priority, giving customers control cannot raise total customer surplus above full disclosure; under LPT it cannot lower surplus below full disclosure. The result therefore ties the social effect of the same disclosure option to a service discipline and to the mix of request types. Its strict clauses identify when withholding produces a genuine difference rather than equality. Hu, Momot, and Wang, Theorem 1 and discussion, p. 15

The paper establishes the theorem and the supporting identities mathematically. Here the remaining task is to prove the Lean statements from the definitions of the queue's class parameters and mean times. The formal development can leave reusable algebraic interfaces for finite-class preemptive-priority queues and for checking stability and denominator conditions in rational queueing formulas. These definitions and statements currently compile as a local draft; they are not yet machine-checked proofs of the paper's results.

Difficulty

An individual disclosure choice moves a request between the middle priority class and one of the two extreme classes. The direct utility comparison does not by itself determine the direction of total surplus: each choice also changes the class workloads and the waiting times faced by other customers. Thus the endpoint comparison cannot be read off from the sign of $U_d-U_w$ at a single $\gamma$. The analysis must account for the full $\gamma$ dependence of $W_H$, $W_N$, and $W_L$, including the hyperexponential residual time of undisclosed requests. The algebra has several denominators whose sign matters, and a formula in the source proof has a boundary exception at $\gamma=1$. Hu, Momot, and Wang, Online Appendix A.1 and Online Supplement A.2

Formalization scope

Lean represents rates, costs, rewards, waits, disclosure probabilities, utilities, and surplus as real numbers. A generic three-class preemptive-priority interface stores mean service times, mean residual times, and workloads. The paper-specific model supplies the H, N, and L table from Online Appendix A.1, including the undisclosed class's hyperexponential residual time. It treats the resulting mean waiting times as formulas; it does not construct a stochastic queueing process. Lemma 1 then asserts genuine algebraic identities from those formulas, rather than following immediately from the definitions. Hu, Momot, and Wang, Online Appendix A.1

The standing assumptions retain $\sigma>0$, $\sigma\ne1$, $0\le\alpha\le1$, $\lambda<\bar\mu$, and $R\ge c/\bar\mu$ from §3.2. They state $\mu>0$, $\lambda>0$, and $c>0$ explicitly because these are rates and a marginal cost, and because zero values would erase the strict comparisons. The theorem items restrict $\gamma$ to $[0,1]$ whenever using the waiting-time formulas. The auxiliary closed-form, derivative, and bracket items exclude $\alpha(1+\sigma)=1$, where the source's displayed second fraction is undefined as a real quotient. Lemma 4 and the goal include that parameter value. The derivative of $\Gamma$ is strictly negative on $[0,1)$ and equals zero at $1$; its strict decrease across the whole interval is stated separately. Hu, Momot, and Wang, §3.2 and Online Supplement A.2

Strict monotonicity of surplus requires $0<\alpha<1$, since a population with only one service type has no type-mix effect. The goal's strict clause requires $\alpha>0$; at $\alpha=0$, a withholding equilibrium can have exactly the same surplus as full disclosure. The goal still quantifies over an equilibrium, rather than an arbitrary point of $[0,1]$. Contributions toward the queueing identities, rational-function sign conditions, monotonicity, and final comparison all serve this scope.

Selected references

• Hu, M., Momot, R., and Wang, J., Privacy Management in Service Systems, submitted manuscript, draft of 12 February 2022; published in Manufacturing & Service Operations Management 24(5), 2022. SSRN 3628751.

Motivation

Advertising pays for content that many readers receive without a direct subscription charge. An adblocker changes two parts of that arrangement: some readers see fewer ads, and the publisher may earn less from investing in content quality. Readers can benefit from the first change and lose from the second. A comparison of consumer surplus therefore has to account for the publisher's response, rather than hold quality fixed. Gritckevich, Katona, and Sarvary's Ad Blocking studies this question in a game where an adblocker can also obtain a payment from the publisher by threatening to block all ads for its users.

The paper's Proposition 3 says that the direction of the consumer-surplus comparison depends on heterogeneity in readers' sensitivity to advertising and content quality. It provides a reason why a tool that visibly removes an annoyance need not raise the total surplus of its users and other readers once the content market adjusts. The result is relevant to people assessing ad-supported publishing and adblocker policies, especially when a partial-blocking tool and its publisher payment are part of the business model.

Setting

One publisher chooses content quality $q\ge0$ at cost $cq^2$, where $c>0$, and earns a positive price $p_a$ for each advertising impression. The publisher later chooses advertising volume $A\ge0$. A unit mass of consumers differs in three independent characteristics. Their quality sensitivity $\vartheta$ is uniform on $[t,1]$, their ad sensitivity $\gamma$ is uniform on $[r,1]$, and their cost $\kappa$ of downloading an adblocker is uniform on $[0,\bar\kappa]$. The paper assumes $0\le t\le1$, $0<r\le1$, and that the upper download-cost bound $\bar\kappa$ is large enough for its equilibrium analysis. At $t=1$ or $r=1$, the corresponding characteristic is constant.

Without an adblocker, a consumer's utility is $\max\{\vartheta q-\gamma A,0\}$. A consumer visits when $\vartheta q-\gamma A\ge0$. With an adblocker available, the adblocker commits to a maximum ad volume $V\ge0$ for downloaders. A consumer who downloads pays $\kappa$ and, in the equilibrium studied here, sees ad volume $V$. The resulting utility is

$$U=\max\{\vartheta q-\gamma A,\;\vartheta q-\gamma V-\kappa,\;0\}.$$

The consumer downloads when the middle option strictly exceeds both alternatives. This tie convention affects only boundary consumers under a nondegenerate distribution, but it fixes a precise event for the formalization.

The adblocker sets $V$ after quality is chosen. It can threaten to block all ads to its downloaders during negotiation with the publisher. In the paper's basic model, the publisher accepts an offer when indifferent, so the adblocker receives all advertising revenue generated by downloaders. The publisher's retained revenue comes from readers who do not download. The paper shows that, when $\bar\kappa$ is large enough, the publisher's ad choice remains the benchmark-optimal $A$ even with the adblocker. Equilibrium here means that $A$ maximizes benchmark ad revenue at each quality, $V$ maximizes the adblocker's payment at each quality, and quality maximizes the publisher's resulting profit.

Formalization targets

The goal is Proposition 3 of the paper. Write $CS_{NA}$ for expected total consumer utility without an adblocker and $CS_{AB}$ for expected total consumer utility with one, each evaluated at equilibrium. There are positive tolerances $\varepsilon$ and $\delta$ such that, for all sufficiently large $\bar\kappa$,

$$\begin{aligned} 0<r<\varepsilon\ \text{or}\ 0\le t<\varepsilon &\quad\Longrightarrow\quad CS_{AB}<CS_{NA},\\ 1-\delta<r\le1\ \text{and}\ 1-\delta<t\le1 &\quad\Longrightarrow\quad CS_{AB}>CS_{NA}. \end{aligned}$$

The tolerances are uniform over positive $p_a$ and $c$. The point beyond which $\bar\kappa$ is large enough may depend on $p_a,c,r,t$. The inequalities apply to every equilibrium selection, so the target does not assume the paper's equilibrium formulas as inputs. The milestones, in attack order, are the benchmark optimum (Lemma 1), the download rule and the adblocker's payoff (6) at fixed quality, the adblocker's optimal limit (Proposition 1), the publisher's lost revenue (9), the publisher's quality response (Proposition 2), the fixed-quality consumer-surplus identity (11), the sign criterion used to compare the two regimes, and the strict inequality $C_\Delta(r,0)<C_0(r,0)G(r,0)$ that settles the case $t=0$.

Boundary lines

On the two edges of the parameter square the paper gives exact thresholds: for all large $\bar\kappa$,

$$t=1:\ CS_{AB}>CS_{NA}\iff r>\tfrac{\sqrt{141}-1}{14},\qquad r=1:\ CS_{AB}>CS_{NA}\iff t>\tfrac45,$$

with $CS_{AB}<CS_{NA}$ on the other side, threshold included. This is a sharper statement along the edges than the goal's "sufficiently high".

Significance

At fixed quality, downloaders can gain from seeing fewer ads, and the paper's surplus identity makes that gain positive. The equilibrium result determines when that gain outweighs the loss caused by lower publisher quality. Its low-heterogeneity region gives a precise setting in which total consumer surplus increases, while either sufficiently broad ad sensitivity or broad quality sensitivity makes the same intervention lower total consumer surplus. This is the distinction a fixed-quality comparison cannot make. The paper's separate total-welfare and extended bargaining results are not implied by this mission's goal.

A machine-checked development would connect an economic game's timing and best responses to explicit probability laws, integrals of consumer utility, and the resulting welfare comparison. The paper proves Proposition 3, but the Lean theorem and its supporting milestones are currently statements with open proofs. Completing them would also leave reusable formal components: a normalized interval law with point endpoints, a model of mixed discrete and continuous consumer types, and optimization statements for a staged publishing game. No machine-checked proof of this specific result is claimed here.

Difficulty

The immediate benefit to a downloader is easy to see only when the publisher's quality is held constant. That argument fails for total equilibrium consumer surplus because the adblocker captures downloader ad revenue, reducing the publisher's return to quality. The size of that quality response depends on the distribution of consumer sensitivities, while the direct benefit depends on who downloads and still consumes content. The case split at $t=r/(1+r)$ changes the benchmark ad formula; the general fixed-quality gain has no simple closed form in the paper. The endpoint cases $r=1$ and $t=1$ also require genuine point-mass distributions rather than formulas that divide by $1-r$ or $1-t$.

Formalization scope

Lean represents all prices, choices, utilities, and coefficients in $\mathbb R$. The three consumer characteristics have independent uniform laws, represented by iterated integrals. A point interval is represented by a Dirac law, preserving the source's $r=1$ and $t=1$ cases. Quality, ad volume, and the adblocker's limit are optimized over the nonnegative reals. Benchmark visits include a zero-utility tie; downloading requires a strict gain over both visiting without the tool and not visiting. The support bound $\bar\kappa$ is positive and sufficiently large wherever the paper's calculations require it.

The base game uses the paper's equilibrium convention that the publisher retains the benchmark-optimal ad volume with the adblocker present. Negotiation is represented in reduced form: the adblocker receives the entire ad revenue from downloaders, and the publisher keeps revenue from other visitors. Positivity of the ad price and quality-cost coefficient, implicit in the economic setup, is explicit in Lean. The source's phrase “$\kappa$ high enough” in Proposition 3 is read as “$\bar\kappa$ high enough,” since $\kappa$ is an individual's cost and $\bar\kappa$ sets its population range. A corrected normalization factor in the printed first branch of $C_0$ is recorded in the definition and moderation notes. Closed-form milestones such as (6) and (9) carry an explicit lower bound on $\bar\kappa$, namely the upper limit of the paper's $\kappa$-integral. The paper's weak inequality $C_\Delta(r,0)\le C_0(r,0)G(r,0)$ is stated strictly, which is true on $(0,1]$ and is what the goal needs.

The goal uses expected utility and best-response conditions, not values manufactured from the closed-form formulas. A proof therefore must establish that the modeled equilibria exist and satisfy the paper's formulas; otherwise a universal comparison over an empty set of equilibria would have no economic content. Contributions that prove the interval-law facts, measurable and integrable consumer events, benchmark and adblocker best responses, or the sign criterion all advance the same target.

Selected references

• Alexander Gritckevich, Zsolt Katona, and Miklos Sarvary, Ad Blocking, SSRN preprint 3100524, version of March 7, 2021; published in Management Science, 2021. SSRN preprint; journal DOI.