All missions

Motivation

Whether a customer joins a queue depends on how congested she believes it is. Classical strategic queueing studies two extremes. In the visible queue of Naor (1969) every arrival sees the queue length and joins exactly when her net payoff is nonnegative; in the invisible queue of Edelson and Hildebrand (1975) arrivals see nothing and act on the stationary distribution alone. Many service systems sit between the two: a call centre announces nothing, a restaurant can be inspected only at some effort, an online service shows a vague busy indicator. Customers there can learn about congestion, but learning costs time and attention.

Canyakmaz and Boyacı model this middle ground with rational inattention (Sims 2003; Matějka and McKay 2015): each customer chooses what to learn about the number of customers in the system, paying a cost proportional to the mutual information between what she learns and the true state, and then joins or balks. Because every customer's prior is the steady-state distribution generated by everyone else's joining behaviour, the model has a fixed-point structure, and the basic question is whether a consistent pattern of beliefs and behaviour exists and whether it is unique. Theorem 1 of the paper answers both questions affirmatively for every positive information cost. The paper's later results (comparative statics, revenue-maximizing prices, the limits of a visible and an invisible queue) are all statements about this unique equilibrium.

Setting

Customers arrive to a single-server first-come-first-served queue as a Poisson process with rate $\lambda>0$; service times are exponential with rate $\mu>0$; $\rho=\lambda/\mu$. A served customer receives the reward $R$, pays the price $p$, and pays $C>0$ per unit of waiting time. A customer who finds $n$ customers in the system and joins gets the expected payoff

$$v_n = R - p - \frac{C}{\mu}\,n ,$$

and it is assumed that $R>p$, so $v_0>0$. Balking is worth $0$.

The customer does not see $n$; she holds a prior $g=(g_n)_{n\ge0}$ on it and pays $\theta>0$ per unit of mutual information acquired. The paper reduces her problem to a choice of the unconditional joining probability $\bar\pi\in[0,1]$:

$$\max_{\bar\pi\in[0,1]}\ \theta\sum_{n\ge0} g_n \log\big(\bar\pi e^{v_n/\theta}+1-\bar\pi\big), \tag{9}$$

after which she joins in state $n$ with probability given by the generalized multinomial logit formula

$$\pi_n(\bar\pi)=\frac{\bar\pi e^{v_n/\theta}}{1-\bar\pi+\bar\pi e^{v_n/\theta}} .$$

If all customers use $\pi_n(q)$, the queue is a birth–death process with arrival rates $\lambda\pi_n(q)$ and service rate $\mu$. Its unnormalized weights are $a_k(q)=\rho^k\pi_0(q)\cdots\pi_{k-1}(q)$, $a_0=1$; when $\sum_k a_k(q)<\infty$ ($q$ is admissible) the stationary law is $g_n(q)=a_n(q)/\sum_k a_k(q)$.

An equilibrium (Definition 1) is an admissible $\tilde\pi$ such that, with $\tilde g=g(\tilde\pi)$ and $\tilde\pi_n=\pi_n(\tilde\pi)$, the consistency equation $\tilde\pi=\sum_n\tilde\pi_n\tilde g(n)$ holds and $\tilde\pi$ solves (9) under the prior $\tilde g$.

Formalization targets

Goal: Theorem 1

For all parameters with $\lambda,\mu,C,\theta>0$ and $R>p$,

$$\exists!\ \tilde\pi\in[0,1]:\ \tilde\pi \text{ is an equilibrium in the sense of Definition 1.}$$

No relation between $\lambda$ and $\mu$ is assumed: when $\lambda\ge\mu$ the equilibrium joining probability is strictly below one.

Milestones

The milestones follow the paper's proof of Theorem 1 and its Lemmas 1 and 2:

1. the stationary law exists for every $q<1$, and for $q=1$ exactly when $\lambda<\mu$;
2. Lemma 1: the first-order conditions (10)–(13) characterize the solutions of (9) for any prior with finite mean;
3. at a solution of (9) the consistency equation (5) holds automatically;
4. for admissible $q$, the objective $f(\cdot;q)$ of (24) is concave and (23) has a unique solution $\bar\pi(q)$;
5. $\bar\pi(0)=1$;
6. $q\mapsto\bar\pi(q)$ is continuous on the admissible set;
7. Lemma 2: $g_n(q_2)-g_n(q_1)$ changes sign once, from negative to positive, for $q_1<q_2$;
8. $\varphi_n(x;\theta)=(e^{v_n/\theta}-1)/(xe^{v_n/\theta}+1-x)$ of (25) is decreasing in $n$;
9. $\bar\pi(q)$ is decreasing in $q$.

Significance

Existence and uniqueness are what make the model usable. The paper's comparative statics in $R$, $\mu$, $p$, $C$ (Proposition 1), its unimodal revenue curve (Proposition 2), and the limits $\theta\to0$ and $\theta\to\infty$ recovering Naor's and Edelson–Hildebrand's equilibria (Corollary 1) are all statements about "the" equilibrium; without Theorem 1 they would have no object. The result also shows that information frictions do not create multiplicity here, in contrast to many congestion games with strategic complementarities.

The result is proved in the paper; nothing in it is open. As far as a search of the Prove2Me library shows, none of it is formalized: there is no machine-checked treatment of rational-inattention choice in queues, of the reduced problem (9), or of the monotone comparative statics of birth–death stationary laws in a joining parameter used here. A formalization would produce reusable pieces for strategic queueing (product-form laws with state-dependent arrival rates, single-crossing of stationary distributions) and for rational inattention (the first-order characterization of binary choice with Shannon cost).

Difficulty

The obvious argument — the best response $\bar\pi(q)$ is continuous, starts at $\bar\pi(0)=1$ and ends at $\bar\pi(1)\le1$, so it crosses the diagonal — fails at the right endpoint when $\lambda\ge\mu$: then $q=1$ is not admissible, the stationary law does not exist there, and the inequality $\bar\pi(1)\le 1$ that the paper's intermediate-value argument uses is not available. The behaviour of the best response as $q\uparrow1$ has to be controlled by an argument the paper does not give.

The uniqueness step of the paper compares first-order conditions under two priors. Turning that comparison into a statement about maximizers requires handling the boundary solutions $\bar\pi\in\{0,1\}$ of (9), where the first-order condition is an inequality, and the endpoint $x=1$, where $\varphi_n(1;\theta)=1-e^{-v_n/\theta}$ is unbounded below and the derivative series may diverge.

All series are infinite: interchanging differentiation and summation, and continuity of $g(q)$ in $q$, need domination arguments that the paper does not spell out.

Formalization scope

Everything is in OpaqueQueue.Equilibrium. Parameters form a structure Params with fields lam, mu, R, p, C, θ; the standing assumptions $\lambda,\mu,C,\theta>0$ and $p<R$ are the predicate Params.Standing. Values are real; states are natural numbers; the logarithm is natural. joinProb P q n is $\pi_n(q)$, weight P q k is $a_k(q)$, Admissible P q is $q\in[0,1]$ together with summability of $a(q)$, stat P q n is $g_n(q)$, obj P g x is the objective of (9) for a prior g, IsOptimal P g x says $x$ solves (9), and IsEquilibrium P q is Definition 1. stat divides by a series that Lean evaluates to $0$ when it diverges; every statement about it therefore assumes admissibility.

IsEquilibrium requires optimality of $\tilde\pi$ in (9) under the equilibrium prior, besides the printed equations (14)–(15). Those equations alone are satisfied by $\tilde\pi=0$ for every parameter value (and by $\tilde\pi=1$ whenever $\lambda<\mu$), so reading Definition 1 without optimality would make Theorem 1 false. The paper's own proof uses the optimizer of (23) as the best response. Stating the goal as the existence of a unique fixed point of an arbitrary or choice-based best-response function would also be unfaithful and is ruled out.

Lemma 1 is stated for priors with finite mean, under which (9) is finite on all of $[0,1]$. The paper states it for the joining policy of problem (6); the mission states it for problem (9), to which the paper reduces (6). The reduction itself (Matějka and McKay 2015; Caplin, Dean and Leahy 2016), Corollary 1, Propositions 1–4, Theorems 2–3 and the numerical sections are outside this mission.

A complete development needs: summability and continuity of parameter-dependent series, concave maximization on an interval with one-sided derivatives, and single-crossing and stochastic-dominance arguments for laws on $\mathbb N$. Proofs of individual milestones, alternative arguments, and general lemmas on product-form birth–death laws are all welcome.

Selected references

• C. Canyakmaz and T. Boyacı, Opaque Queues: Service Systems with Rationally Inattentive Customers, ESMT Working Paper 18-04, 2018; published as Queueing Systems with Rationally Inattentive Customers, Manufacturing & Service Operations Management 25(2), 2023. https://doi.org/10.1287/msom.2021.1032
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 15–24, 1969. https://doi.org/10.2307/1909200
• N. M. Edelson and D. K. Hildebrand, Congestion Tolls for Poisson Queuing Processes, Econometrica 43(1), 81–92, 1975. https://doi.org/10.2307/1913415
• C. A. Sims, Implications of Rational Inattention, Journal of Monetary Economics 50(3), 665–690, 2003. https://doi.org/10.1016/S0304-3932(03)00029-1
• F. Matějka and A. McKay, Rational Inattention to Discrete Choices: A New Foundation for the Multinomial Logit Model, American Economic Review 105(1), 272–298, 2015. https://doi.org/10.1257/aer.20130047
• A. Caplin, M. Dean and J. Leahy, Rational Inattention, Optimal Consideration Sets, and Stochastic Choice, Review of Economic Studies 86(3), 1061–1094, 2019 (NBER WP 23652, 2016). https://doi.org/10.1093/restud/rdy037

Motivation

Sell-side analysts are ranked against each other. Published rankings, such as Institutional Investor's annual "All-Star" ranking cited in the paper, and the career outcomes tied to them, reward an analyst for being more accurate than peers, not only for being accurate. A common intuition holds that such competition disciplines analysts and makes their forecasts more informative for investors. Sanjay Banerjee's paper Does Competition Improve Analysts' Forecast Informativeness? (working paper, Alberta School of Business Research Paper No. 2017-311, 2017; later published in Management Science, doi:10.1287/mnsc.2019.3544) asks whether that intuition survives a model in which analysts best-respond to each other strategically.

The paper places itself next to the multi-sender cheap-talk literature (Krishna and Morgan 2001, Battaglini 2002). There, several senders typically reveal more than one. Two features separate this model: forecasts are scored against the realised state, and analysts' private signals are correlated conditional on the state. Its main result identifies exactly when competition makes forecasts less informative.

Setting

A state $\omega\in\{H,L\}$ has prior $\Pr(H)=q\in(0,1)$; for measuring information, $H=1$ and $L=0$, so $\mathrm{Var}(\omega)=q(1-q)$. Two risk-neutral analysts each observe a private signal $s_i\in\{h,l\}$ of precision $\gamma=\Pr(s_i=\omega\mid\omega)\in(\tfrac12,1)$. Given the state, the signals have correlation $\rho\in[0,1]$. With $\chi=\rho\gamma(1-\gamma)$, each ordered pair of signals has conditional probability $\gamma^2+\chi$ if both equal the state, $(1-\gamma)^2+\chi$ if both differ from it, and $\gamma(1-\gamma)-\chi$ if they disagree.

Each analyst forecasts $m_i\in\{\hat h,\hat l\}$. A symmetric strategy is $\sigma=(\sigma^h,\sigma^l)$, with $\sigma^h=\Pr(\hat h\mid h)$ and $\sigma^l=\Pr(\hat l\mid l)$. Under competition, an analyst whose forecast alone matches the state earns $w_1$, the other earns $w_2$, and identical forecasts earn $w_0$ each, with $w_1>w_0>w_2$. The payoff convexity is

$$\varphi=\frac{w_1-w_0}{w_0-w_2},$$

and the payoff is convex if $\varphi>1$, concave if $\varphi<1$. In the benchmark, an analyst is paid for his own accuracy only.

A symmetric equilibrium is a $\sigma\in[0,1]^2$ with $\sigma^h\ge1-\sigma^l$ such that, for each signal, the prescribed probability of a truthful forecast maximises the analyst's expected payoff, computed by Bayes' rule, when the other analyst plays $\sigma$. It is pooling if $\sigma^h=1-\sigma^l$ and separating if $\sigma=(1,1)$. A most informative equilibrium is an equilibrium that is coordinatewise at least every other equilibrium of the same game. Forecast informativeness is the posterior precision normalised by the prior precision,

$$\Pi(\sigma)=\frac{\mathrm{Var}(\omega)}{E_{m_i,m_j}\big[\mathrm{Var}(\omega\mid m_i,m_j)\big]}-1 .$$

Finally, the separation threshold of the rank game is

$$\check q_{\min}=\gamma-\chi\,\frac{\varphi-1}{(1-\gamma)\varphi+\gamma}.$$

Formalization targets

Goal: Proposition 5 (B.1), corrected

Fix $\gamma\in(\tfrac12,1)$, $\rho\in[0,1]$ and $w_1>w_0>w_2$ with $\varphi\ne1$, and restrict to $q\ge\tfrac12$, as the paper does ("Results for $q<\frac12$ are symmetric"). Let $\sigma$ and $\sigma_B$ be most informative equilibria of the rank game and of the benchmark at $q$. Then

$$\Pi(\sigma)<\Pi(\sigma_B)\ \Longrightarrow\ \varphi>1,\ \rho>0,\ \check q_{\min}<q\le\gamma,$$

and conversely, if $\varphi>1$ and $\rho>0$, then for every $q\in[\tfrac12,1)\cap(\check q_{\min},\gamma]$ both most informative equilibria exist and every such pair satisfies $\Pi(\sigma)<\Pi(\sigma_B)$.

The paper prints "$q<\gamma$". At $q=\gamma$ informativeness still drops (for $\gamma=0.7$, $\rho=0.4$, $\varphi=3$: $\Pi=0.147<\Pi_B=0.232$). On $[\tfrac12,\check q_{\min}]$ it does not drop, because the separating profile remains an equilibrium. The interval $(\check q_{\min},\gamma]$ is the paper's own reading: "$\Pi_{\varphi>1}<\Pi_B$ at $q\in(\check q_{\min},\gamma]$" (p. 26).

Milestones

The milestones are the paper's numbered results that the proof uses:

• the benchmark's equilibria (Lemma 1, with the interval corrected to $[1-\gamma,\gamma]$);
• the separation threshold (Claim 1);
• the comparative statics of the net payoffs (Claim 2);
• the comparison function $g_l-g_h$ (Claim 3);
• the exclusion of fully mixed and semi-separating equilibria (Claims 4–5);
• the characterisation of the most informative equilibrium without and with correlation (Proposition 2 (A), Proposition 3 (A.1)–(A.2));
• the monotonicity of $\Pi$ (Claim 7).

Significance

The result. Proposition 5 (B.1) is the paper's main counterintuitive finding. Convex rank incentives combined with correlated information make analysts understate their private signals in order to differentiate themselves, and the market learns less than it would from two analysts who ignore each other. The conditions are sharp: with uncorrelated signals or a concave payoff, competition never lowers informativeness at $q\ge\frac12$. This is relevant to the design of analyst rankings and of tournament incentives for forecasters more generally.

Formalizing it. The result is proved on paper through seven claims and a case analysis over regimes of $(\rho,\varphi,q)$. The case analysis contains slips, such as the empty interval in Lemma 1, a sign error in (B.28), and boundary cases $\varphi=\bar\varphi$ and $q=\gamma$ assigned to the wrong regime. A machine-checked proof would settle the exact statement. To the best of our knowledge none of these results has been formalized; the mission produces the first formal model of this game.

Difficulty

Each analyst's best response depends on the other's strategy through a conditional law of the other's forecast, which is affine in $\sigma$, and through Bayesian posteriors, which are ratios of such terms. The equilibrium conditions are therefore piecewise-affine inequalities whose sign pattern changes with $(\rho,\varphi,q)$. The obvious argument would compute a single equilibrium and compare informativeness. It fails because the goal speaks of the most informative equilibrium. One must show that no other equilibrium dominates it coordinatewise, and in the high-convexity, high-correlation regime the relevant equilibrium is fully mixed and is defined through an implicit root ($\ddot\sigma^l$). The "only if" half requires excluding a decrease in every other regime, including $q>\gamma$, where the benchmark pools and one needs $\Pi\ge0$.

Formalization scope

States, signals and forecasts are Bool (true = H, h, ĥ). A strategy is a pair σ : ℝ × ℝ, and the equilibrium set carries the restriction $\sigma^h\ge1-\sigma^l$ of p. 9. Expected payoffs are conditional expectations of the rank payoff (3) under the joint signal law and Bayes' rule. The equilibrium condition is that the prescribed mixing probability maximises the expected payoff over all of $[0,1]$. The benchmark pays $1$ for a correct forecast, a positive rescaling of the paper's $\pi_a=W$. A forecast pair of probability zero contributes zero to the expected posterior variance. The paper's standing restriction $q\ge\frac12$ is part of the goal: below one half the decrease occurs on the mirror interval $[1-\gamma,1-\check q_{\min})$, and the condition $q\le\gamma$ would be vacuous.

The trivializing formalizations are ruled out. The net payoffs $\Delta U$ and informativeness $\Pi$ are computed from the primitives, never from the paper's closed forms (A.13)–(A.14) or Lemma 3. The "if" half asserts that the most informative equilibrium exists. The benchmark value is the benchmark game's own most informative equilibrium, not $\Pi(1,1)$ written into the statement.

The "Furthermore, the decrease in information revelation increases with payoff convexity" clause is not part of the goal. Neither are Proposition 5 (A) and (B.2), Propositions 2 (B) and 3 (B), Lemmas 2–3, Proposition 4, Claim 6 and Appendix C. Corrected milestones are labelled in their titles:

• Lemma 1: the interval is $[1-\gamma,\gamma]$;
• Claim 3 (B.2) and Proposition 3 (A.2): $\varphi>\bar\varphi$;
• Proposition 3 (A.2): on $[1-\bar q,\bar q]$, the fully mixed formula's coordinates lie in $(0,1)$ strictly inside the interval, and one of them equals $1$ at each endpoint;
• Proposition 3 (A.1): extended to $\varphi\le\bar\varphi$;
• Claim 3 (C): restricted to $\sigma^h\ge1-\sigma^l$.

A complete development needs:

• finite sums over Bool;
• real field arithmetic for rational functions of $(q,\gamma,\rho,\varphi,\sigma)$;
• an intermediate value argument for the root $\ddot\sigma^l$;
• the concavity fact that posterior variance does not exceed prior variance on average.

The finite Bayesian-game layer (symmetric equilibria of a two-player game with binary types) is reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.

Selected references

• S. Banerjee, Does Competition Improve Analysts' Forecast Informativeness?, Alberta School of Business Research Paper No. 2017-311 (13 Nov 2017), the version formalized here; published in Management Science, 2020. https://doi.org/10.1287/mnsc.2019.3544
• V. Krishna and J. Morgan, A Model of Expertise, Quarterly Journal of Economics 116(2), 2001. https://doi.org/10.1162/00335530151144159
• M. Battaglini, Multiple Referrals and Multidimensional Cheap Talk, Econometrica 70(4), 2002. https://doi.org/10.1111/1468-0262.00335
• V. P. Crawford and J. Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390

Motivation

Naive Bayes is one of the oldest and cheapest classifiers for text and count data: given word counts for documents in two classes, it fits one multinomial distribution per class by maximum likelihood and classifies by the likelihood ratio. Its cost is a single pass over the data. In high-dimensional applications (text, genomics) one also wants the classifier to depend on few features, both for interpretability and to discard noise. Imposing that the two class distributions differ in at most $k$ coordinates turns maximum-likelihood fitting into a cardinality-constrained, nonconvex problem.

Askari, d'Aspremont and El Ghaoui (arXiv:1905.09884, Mathematics of Operations Research, 2024) show that the Lagrangian dual of this sparse problem is a one-dimensional convex problem solvable by bisection at essentially the cost of naive Bayes itself, and that its value is within a shift of four features of the true optimum. The shift comes from a duality-gap bound for separable problems in the line of Aubin and Ekeland (1976) and Ekeland and Temam, based on the Shapley–Folkman lemma.

Setting

There are $m$ features. A nonnegative data matrix with labels $\pm1$ enters only through the class sums $f^+,f^-\in\mathbb R^m$ (the total count of each feature in each class), assumed entrywise positive. Write $g=f^++f^-$ and $S=\mathbf 1^\top g$.

The sparse multinomial naive Bayes problem (SMNB) at sparsity level $k$ is

$$\phi(k)=\max_{\theta^+,\theta^-\in[0,1]^m}\ f^{+\top}\log\theta^++f^{-\top}\log\theta^-\quad\text{s.t.}\quad \mathbf 1^\top\theta^+=\mathbf 1^\top\theta^-=1,\quad \|\theta^+-\theta^-\|_0\le k,$$

where $\|\theta^+-\theta^-\|_0$ counts the coordinates in which the two class distributions differ. Without the last constraint the problem is ordinary naive Bayes.

For a vector $c$, $s_k(c)$ is the sum of its $k$ largest entries. Let

$$\tilde C=f^+\circ\log f^++f^-\circ\log f^--g\circ\log g,\qquad h(\alpha)=\tilde C-f^+\log\alpha-f^-\log(1-\alpha)\quad(0<\alpha<1),$$

and $C=g^\top\log g-S\log S$. The relaxation (USMNB) has value

$$\psi(k)=C+\min_{\alpha\in(0,1)}s_k\big(h(\alpha)\big).$$

It is a convex problem in one variable. Its dual (D) is a concave maximization over $x\in[0,1]^m$ with $\mathbf 1^\top x\le k$, which plays the role of a fractional feature-selection vector.

Formalization targets

Goal: Theorem 3.6

For $4\le k<m$,

$$\psi(k-4)\le\phi(k)\le\psi(k)\le\phi(k+4).$$

The constant four does not depend on $m$, $k$ or the data. Numerically it is not tight (a shift of one suffices on random instances), but the goal keeps the paper's constant.

Milestones

1. Lemma 3.11: $s_k(c)=\min_{\lambda\ge0}\lambda k+\sum_i\max(0,c_i-\lambda)$ for $c\ge0$, the optimal multipliers, and the structure of solutions of the dual linear program (36).
2. §3.4: $w(\mu)\ge v(\mu)$ for $\mu>0$, the inequality behind the top-$k$ form.
3. §3.4: the Lagrangian dual of (SMNB) equals $-S+\min(17)$, which equals $\psi(k)$.
4. Theorem 3.2: $\phi(k)\le\psi(k)$.
5. Theorem 3.5: the duality-gap bound $h_P(\bar p)\le h_P(0)^{**}+(m+1)\max_i\rho(f_i)$ for separable problems.
6. The lack of convexity of $\mathbf 1_{x\ne y}$ on $[0,1]^2$ is one, its convex envelope being $|x-y|$.
7. Proposition 3.7: strong duality between (USMNB) and its dual (D).
8. Proposition 3.8: an optimal solution of (D) with $J$ fractional coordinates yields a feasible point of (SMNB) at level $k+|J|$ whose value lies between $\phi(k)$ and $\phi(k+|J|)$.
9. Proposition 3.9: (D) has an optimal solution with at most four fractional coordinates.

Milestones 1–6 follow the paper's proof of Theorem 3.6; milestones 7–9, on top of 1–4, are the paper's second, constructive route to the upper bound $\psi(k)\le\phi(k+4)$.

Significance

The theorem certifies that a convex problem of negligible cost brackets a nonconvex, combinatorial maximum-likelihood problem: the relaxation's value at $k$ lies between the true values at $k$ and $k+4$. Whenever $\psi$ varies slowly in $k$, which the paper observes past the "elbow" in the number of relevant features, the duality gap is small, and Propositions 3.8–3.9 turn the relaxation's solution into a sparse classifier with at most four extra features. The paper uses this to run feature selection on data sets with millions of features.

The results are proved in the paper (Theorem 3.5 is quoted from the literature). None is formalized. Formalizing them yields the perturbation-function duality-gap bound for separable nonconvex problems as a reusable statement, a verified variational formula for top-$k$ sums, and a check of a printed formula: the dual (D) as printed carries a spurious term $-(x^\top g)$, and the formal statement uses the corrected objective.

Difficulty

The lower and middle inequalities are weak duality once the dual is computed, and computing it is a separable calculation. The upper inequality $\psi(k)\le\phi(k+4)$ is the content: it bounds a duality gap, and nothing in the one-dimensional structure of (USMNB) gives it. The naive approach, rounding the fractional $x$ of (D) to its top $k$ coordinates, has no a priori control on the loss. Both of the paper's routes need a Shapley–Folkman type argument, in which the number of nonconvex contributions is bounded by the number of constraints plus one. The Shapley–Folkman lemma itself is not in Mathlib (it is an open goal on the platform), and Theorem 3.5 also requires conjugates of extended-valued functions and the convex envelope of a sum of separable terms.

Formalization scope

Features are indexed by Fin m, with fp fm : Fin m → ℝ entrywise positive. This positivity is stated on p. 7 and is needed because the formulas take $\log f^\pm$. The standing assumption $k<m$ of §3.1 is carried by every statement about (SMNB). The commitments are:

• $\phi(k)$ is a real supremum over $\theta^\pm\in(0,1]^m$. Strict positivity matches the paper's value ($f^\pm>0$ makes the objective $-\infty$ at any $\theta_i=0$) and avoids Lean's $\log0=0$.
• $s_k$ sums the largest $\min(k,m)$ entries, including for signed vectors. On the nonnegative vectors used by the relaxation, this equals the maximum over index sets of size at most $k$ from p. 6.
• $\psi(k)$ minimizes over the open interval $(0,1)$, where $h$ is defined, and the constant $C=g^\top\log g-S\log S$ of p. 8 is built in. Taking $C$ as a parameter, or defining $\psi$ as the Lagrangian dual, would make the goal false or turn milestone 3 into a definition; both are excluded.
• The Lagrangian dual's inner maximum is over $\theta^\pm\in(0,\infty)^m$, which is the problem the paper's closed forms solve. With the printed box $[0,1]^m$ the identity of milestone 3 fails on some instances.
• (D) is used in its corrected form, with $z=\mathbf 1-x$ eliminated.
• §3.6 uses EReal-valued functions on Fin d → ℝ. The conjugate is a supremum (p. 9 prints an infimum), and finiteness of each $\rho(g_{ji})$ is added in Theorem 3.5 so that $\bar p$ is a real vector.
• In the paper's proof of Theorem 3.6, the equality constraints of (25) are not of the form "$\le b+u$" required by (P). Because the objective is decreasing in $q$ and $r$, replacing them by inequalities leaves the values unchanged.

Proposition 3.8 is stated with the additional conclusion that the constructed point's value is at least the optimum of (D). Its proof establishes this, and without it the statement is met by a maximizer of $\phi(k)$ and says nothing about (D).

A complete development needs Lagrangian duality for a separable problem, the perspective of $x\log x$, top-$k$ sums and their LP dual, Fenchel conjugates of extended-valued functions, and a Shapley–Folkman lemma. The last three are reusable well beyond this mission, and contributions there are welcome.

Selected references

• A. Askari, A. d'Aspremont, L. El Ghaoui, Naive Feature Selection: A Nearly Tight Convex Relaxation for Sparse Naive Bayes, Mathematics of Operations Research, 2024. https://arxiv.org/abs/1905.09884 (v4 used here).
• J.-P. Aubin, I. Ekeland, Estimates of the duality gap in nonconvex optimization, Mathematics of Operations Research 1(3), 1976. https://doi.org/10.1287/moor.1.3.225
• I. Ekeland, R. Temam, Convex Analysis and Variational Problems, SIAM Classics in Applied Mathematics, 1999, Appendix I. https://doi.org/10.1137/1.9781611971088
• R. M. Starr, Quasi-equilibria in markets with non-convex preferences, Econometrica 37(1), 1969. https://doi.org/10.2307/1909201

Why pricing changes when consumers set goals

A seller of a product that gives immediate pleasure and delayed harm faces consumers who may plan to limit consumption and then consume more than planned. This setting applies to the paper's examples of cookies, soft drinks, cigarettes, and alcohol. A personal consumption goal is one way a consumer may restrain overconsumption. The question for the seller is whether that restraint calls for a lower or a higher price. In Amaldoss and Harutyunyan's model, both answers are possible: the direction changes with the harm from one unit of the product.

This mission formalizes the paper's comparison between the monopoly price when consumers set personal goals and the price when they have no goals. The comparison is Proposition 1 of the September 2022 SSRN version, p. 14 (PDF 15). The model is intentionally narrow. Consumers are identical, the seller has a single product, and all uncertainty is absent. These restrictions make it possible to isolate how a goal changes consumption and willingness to buy without attributing a price change to market heterogeneity or a change in production cost.

Consumer and seller setting

A unit mass of identical consumers obtains consumption value $vq-q^2/2$ from quantity $q\ge0$, where $v>0$ is the initial marginal value. Each unit causes delayed harm $h\ge0$. A unit costs $p\ge0$ to buy. The seller's marginal production cost is normalized to zero. At the consumption stage, consumers discount harm by a present-bias factor $\beta$ with $0<\beta<1$. Earlier, when deciding whether to buy and when choosing a goal, they count the harm without this discount. The quadratic coefficient is fixed at $1/2$, as in §3 of the paper, pp. 7–9 (PDF 8–10).

A consumer may choose a personal goal $G\ge0$. Consuming more than $G$ incurs goal disutility $\lambda(q-G)^2$, with $\lambda>0$; consuming no more than $G$ incurs none. Thus the benchmark utility when quantity is chosen is

$$U_4^B(p,q)=vq-\frac{q^2}{2}-\beta hq-pq,$$

and the utility with a goal is $U_4(G,p,q)=U_4^B(p,q)-\lambda(q-G)^2\mathbf 1_{q>G}$. The earlier planning-stage utility without a goal replaces $\beta hq$ by $hq$. With a goal, the same penalty is present at the goal-setting stage. These are the utilities in §4.1–4.2 of the paper, pp. 10–12 (PDF 11–13).

The sequence is price, purchase plan, personal-goal choice, quantity choice, and delayed harm. At the planning stage, a consumer correctly anticipates the subsequent goal and quantity choices. The consumer buys exactly when that anticipated utility is at least zero. Because the consumer mass is one, aggregate demand is the quantity purchased by one consumer. The seller chooses a nonnegative price that maximizes price times demand. The benchmark omits the goal and its penalty; the personal-goal regime includes both.

Formalization targets

The supporting targets characterize the consumer's optimal quantity without a goal, benchmark demand, and the benchmark monopoly price; then optimal quantity at a fixed goal, optimal goal, the personal-goal reservation price, demand, and the personal-goal monopoly price. Each is indexed to an equation or paragraph in §4.1–4.2 of the SSRN version, pp. 10–14 (PDF 11–15).

The goal is Proposition 1. Define the comparison threshold

$$h_1=\frac{v(1+2\lambda)}{4-3\beta+6\lambda-4\beta\lambda}.$$

For $0<h<v/(2-\beta)$, both monopoly problems have equilibrium prices. For any benchmark equilibrium price $p^B$ and personal-goal equilibrium price $p^*$, the target is

$$h>h_1\ \Longrightarrow\ p^*>p^B,\qquad 0<h<h_1\ \Longrightarrow\ p^*<p^B.$$

The comparison does not assert a strict ordering at $h=h_1$. The paper's statement describes more and less unhealthy products relative to $h_1$; its standing section range is $h\le v/(2-\beta)$ (Proposition 1 and preceding paragraph, p. 14, PDF 15). The formal goal uses a strict upper endpoint for the price-uniqueness reason explained below.

What the result establishes

The result identifies two opposing price outcomes under one behavioral change. A personal goal reduces the quantity purchased conditional on buying. It can also raise the price at which the consumer is willing to buy. Proposition 1 identifies which effect determines the monopoly price as harm varies. For a product below $h_1$, the goal regime has the lower price; above $h_1$, it has the higher price. The threshold is an explicit expression in valuation, present bias, and goal sensitivity, so the comparison is a parameter statement rather than a numerical illustration (Amaldoss and Harutyunyan, pp. 13–14, PDF 14–15).

The result is already proved in the paper, including a separate proof in the Web Appendix, pp. 2–4 (PDF 34–36). The proposed Lean statements have no machine-checked proofs yet. Formalizing this result would connect the paper's sequential consumer decisions to both monopoly optimization problems under one consistent set of definitions. The quantity, goal, participation, and price characterizations are useful beyond the final comparison: they state exactly where purchase on indifference and zero demand matter. They also provide a small reusable example of present-biased planning in a sequential pricing model.

Difficulty

The quantity choice changes formula at the goal: the goal penalty is active only above $G$. Goal choice therefore depends on an anticipated optimum of a piecewise utility, while purchase depends on the utility of the resulting choice. A price that maximizes revenue must account for a jump from positive demand to zero demand at the consumer's reservation price. The tempting intuition that reduced conditional quantity always lowers the seller's optimal price fails because the purchase threshold also changes. The paper's two price formulas each have separate parameter regimes, and the comparison reverses only at the stated $h_1$ (§4.2 and Web Appendix, Proof of Proposition 1, pp. 12–14 and WA pp. 2–4).

Formalization scope

All model quantities are real. Feasible purchase quantities, goals, and prices are nonnegative. The standing parameters satisfy $v>0$, $0<\beta<1$, $h\ge0$, and $\lambda>0$; Proposition 1 additionally assumes $h>0$. The cost normalization $c=0$ and satiation coefficient $1/2$ are fixed. The goal penalty uses the strict indicator $q>G$. A consumer buys when anticipated planning utility is nonnegative, including equality. This tie rule matters when the seller sets a reservation price.

The main comparison assumes $h<v/(2-\beta)$. The paper takes $h\le v/(2-\beta)$ in the remainder of the section, but at equality benchmark demand is zero at every nonnegative price, so every such price maximizes the same zero revenue. A comparison quantified over all equilibrium prices would then be false. The strict bound records this endpoint issue explicitly. Similar zero-consumption or zero-demand endpoints are excluded only where a milestone claims a unique goal or price.

The Lean definitions specify optimal quantities, optimal goals, demand, and monopoly prices through global maximization over the stated domains. Demand is derived from utility and the purchase rule. It is never defined by the closed-form equations that the milestones are meant to establish. This prevents the target from becoming true merely by defining prices to equal the paper's answers. The generic revenue-maximizer relation is a separate definition; the paper-specific model supplies its demand relations. A complete proof can use Mathlib's real-order and square-root theory together with reasoning about piecewise quadratic functions. Contributions that establish the consumer choices, purchase threshold, demand, or either price characterization are within scope.

Selected references

• W. Amaldoss and M. Harutyunyan, Pricing of Vice Goods for Goal-Driven Consumers, September 2022 SSRN working paper 4226237, main text and Web Appendix. SSRN; Management Science article DOI.

Motivation

Charity watchdogs rate nonprofits by their program expense ratio, the share of spending that goes to programs rather than to administration and fundraising, and donors reward a high ratio. Practitioners have long argued that this pressure produces a nonprofit starvation cycle: organizations underinvest in administration, the infrastructure that sustains their capacity to deliver services, and their capacity erodes (Goggins Gregory & Howard, Stanford Social Innovation Review, 2009). Whether a nonprofit that maximizes the needs it meets should in fact starve administration is an optimization question, and Kotsi, Aflaki, Aydin and Pedraza-Martinez pose it as a two-period budget-allocation problem (SSRN 3460795; later published in Manufacturing & Service Operations Management, DOI 10.1287/msom.2020.0660). Their main structural result, Proposition 1, says that the answer depends on the nonprofit's current capacity through two thresholds.

Setting

A nonprofit lives for two periods. In period $t$ it has budget $B_t$, needs $\psi_t$ and capacity $k_t$. Each program dollar meets $r+1$ dollars of needs, with $r>0$. Keeping capacity $k$ costs the required administration $m(k)$, convex and nondecreasing. Spending $a_t$ on discretionary administration raises next period's capacity to $k_{t+1}=k_t+\delta(a_t)$, where $\delta(0)=0$, $\delta$ is strictly concave and strictly increasing, and $\delta'(0^+)=\infty$. Spending $p_t$ on program, $a_t$ on discretionary administration and $f_t$ on fundraising raises the donations

$$D(p,a,f)=\phi\Big(\frac{p}{p+a+f}\Big)\,f,$$

where $\phi$ is concave and nondecreasing on $[0,1]$, with $\phi(0)=1$ and $\phi(x)>1$ for $x>0$. Donations depend on the program expense ratio $p/(p+a+f)$.

The second-period needs are a random variable $\Psi\ge 0$ with a density. The net budgets are $\hat B_1=B_1-m(k_1)$ and $\hat B_2=D(p_1,a_1,f_1)-m(k_2)$, and the program ceiling is $\theta=\min(\psi_1,k_1,(r+1)\hat B_1)$. Throughout, $B_1\ge 2m(k_1)$. Lemma 1 reduces the two-period dynamic program to problem (2):

$$\max_{p_1,a_1,f_1\ge 0}\ (r+1)p_1+\mathbb E_\Psi\big[\min\big(\Psi,(r+1)\hat B_2\big)\big]$$

subject to $p_1+a_1+f_1=\hat B_1$, $(r+1)p_1\le\theta$, $\hat B_2\ge 0$ and $(r+1)\hat B_2\le k_2$. The last constraint says the second-period budget never exceeds what the second-period capacity can use. The allocation exhausts capacity when that constraint binds, and leaves capacity unused when it is slack.

Formalization targets

Goal: Proposition 1

Fix all data except $k_1$. Problem (2) has an optimal allocation for every admissible $k_1$, and there are thresholds $k^l\le k^h$ such that every optimal allocation $(p_1^*,a_1^*,f_1^*)$ satisfies the following.

• If $k_1<k^l$, the nonprofit expands capacity and exhausts it:

$$a_1^*>0,\qquad (r+1)\hat B_2=k_2 .$$

• If $k^l\le k_1<k^h$, then $(r+1)\hat B_2=k_2$, and $a_1^*=0$ whenever $p_1^*<\theta/(r+1)$.
• If $k_1\ge k^h$, then $a_1^*=0$ and $(r+1)\hat B_2\le k_1$, strictly when $k_1>k^h$.

The thresholds are asserted to exist; no formula for them is part of the goal.

Milestones

The milestones follow the appendix proof:

• Lemma S.1 solves the last period, and Lemma 1 is the reduction to problem (2).
• Lemma S.2 shows that slack in the capacity constraint forces $a_1=0$.
• Lemmas S.3 and S.4 solve the resulting one-dimensional problem in $p_1$.
• Lemma S.5 shows that along the binding constraint, $a_1=\hat a(p_1)$ exists exactly on an interval $[p^+_l,p^+_u]$.
• Lemma S.6 and Proposition 5 solve that branch around a second threshold $\underline k$.

Significance

Proposition 1 gives the structure of the optimal policy. Spending on administration is optimal at low capacity. At moderate capacity, the nonprofit spends on administration only when the program ceiling binds. Starving administration while leaving capacity unused is optimal only at high capacity. This turns the starvation-cycle debate into a statement about where a given nonprofit sits relative to $k^l$ and $k^h$. The paper's case study and numerical sections build on this classification.

The paper proves the result by hand, with implicit-function calculus over several threshold functions of $k_1$. No machine-checked version exists. A formal proof would confirm the case analysis, including the boundary cases that the printed statement gets wrong (see Formalization scope). It would also produce reusable facts about the concave function $y\mapsto\mathbb E[\min(\Psi,y)]$ and about one-parameter families of concave programs.

Difficulty

Problem (2) is not concave in $(p_1,a_1,f_1)$, because the donation term divides by the total spending. So the Karush–Kuhn–Tucker conditions are neither necessary nor sufficient, and no general convexity argument applies. The proof splits on whether the capacity constraint binds. Each branch has its own maximizer and its own thresholds in $p_1$ ($p^0_u$, $p^+_l$, $p^+_u$), and these move with $k_1$. The goal then requires comparing the two branches uniformly in $k_1$. A threshold in $k_1$ exists only if certain differences of these maximizers are monotone in $k_1$, and that monotonicity comes from second-order implicit differentiation of the root $\hat a(p_1)$ of equation (4). A pointwise analysis at a fixed $k_1$ does not give the thresholds.

Formalization scope

All quantities are real. The data $(r,B_1,\psi_1,m,\delta,\phi,\mu)$ form a structure Params, and $\mu$ is the law of $\Psi$. The capacity $k_1$ is a separate argument, quantified over the paper's range $k_1\ge0$, $B_1\ge 2m(k_1)$. The expectation $\mathbb E_\Psi[\min(\Psi,y)]$ is an integral against $\mu$. An optimal allocation is a feasible point whose objective is at least that of every feasible point. The goal asserts existence separately and then quantifies over all optimal allocations.

Added hypotheses. The formalization adds the following to the page's assumptions:

• $\phi$ is strictly concave;
• $m$, $\delta$ and $\phi$ are continuous, and twice continuously differentiable in the interior;
• $m(0)\ge 0$, $B_1>0$ and $\psi_1\ge 0$;
• $\mu$ is a probability measure on $[0,\infty)$ that is absolutely continuous and gives positive mass to every $(x,\infty)$, $x\ge 0$.

Strictness and full support are needed for the uniqueness claims. Without them, $J_{nb}$ can be flat at its maximum, and optimal allocations can fall in two cases at once. Full support is how "Ψ can take any value in $[0,\infty)$" is read.

Repairs to the printed statements. Each is disclosed in the item concerned.

• Constraint (1e) is dropped in the last period, where the terminal value is zero.
• Part (c) of Proposition 1 is non-strict at $k_1=k^h$.
• The "case (i) ⇒ $a_1^*>0$" claim of Proposition 1(b) is not asserted, because it fails when $\theta/(r+1)=p^+_u$.
• In Lemma S.6, the boundary $k_1=\underline k$ moves to part (b).
• Lemma S.4(iii) is posed with a strict inequality.

The comparison "$k_1\le\bar k$" is stated as a condition on $k_1$, not as a defined number. The thresholds $p^+_l,p^+_u,p^0_u$, the root $\hat a$ and the maximizers $\tilde p_{nb},\tilde p_b$ enter as variables characterized by hypotheses.

Ruled out. The thresholds $k^l,k^h$ are chosen once for all admissible $k_1$, and the goal includes existence of an optimum. So the goal cannot hold vacuously, and it cannot be met by thresholds that depend on $k_1$.

Infrastructure. A complete development needs the following:

• concavity and differentiability of $y\mapsto\int\min(x,y)\,d\mu(x)$, with derivative $\mu((y,\infty))$;
• existence of maxima of continuous functions on compact feasible sets;
• the implicit-function theorem in one variable, with second derivatives;
• monotone comparative statics for threshold existence.

The first and last are reusable beyond this mission. Contributions toward any milestone, or toward these general lemmas, are welcome.

Selected references

• T. O. Kotsi, A. Aflaki, G. Aydin, A. J. Pedraza-Martinez, Allocation of nonprofit funds among program, fundraising, and administration, blinded MSOM submission, SSRN 3460795, 2019. https://ssrn.com/abstract=3460795
• T. O. Kotsi, A. Aflaki, G. Aydin, A. J. Pedraza-Martinez, Allocation of nonprofit funds among program, fundraising, and administration, Manufacturing & Service Operations Management (published version, not the basis of this mission's citations). https://doi.org/10.1287/msom.2020.0660
• A. Goggins Gregory, D. Howard, The nonprofit starvation cycle, Stanford Social Innovation Review 7(4), 2009. https://ssir.org/articles/entry/the_nonprofit_starvation_cycle

Why the sales allocation problem matters

A hog producer selling to both a meatpacker and an open market faces a weekly allocation choice. The meatpacker contracts for a fixed quantity, pays different rates for underweight and regular-weight hogs, and charges for any shortfall. The open market has separate prices for the two weight classes. Holding an underweight hog costs money now but makes it regular-weight next week. These features make a single “sell or hold” rule inadequate: fulfilling the contract changes the value of the next hog allocated to either market. Kouvelis, Liu, Qiu and Turcic model this setting and state a price-dependent, multiple-threshold sales policy in Proposition 1 of their March 6, 2023 preprint.

The stated policy is of direct interest for inventory decisions with quality upgrading and contractual penalties. It also provides a precise test case for dynamic programming with continuous stock decisions, stochastic prices, and a capacity-constrained contract. The mission concerns the mathematical policy statement, rather than the paper’s empirical estimates or numerical comparisons.

Setting and notation

At the start of period $t\in\{1,\ldots,t_M\}$, the producer observes $s_t=(s^1_t,s^2_t)$ underweight and regular-weight hogs and the price vector $P_t=(p^C_t,p^1_t,p^2_t,c^H_t,c^P_t)$. The contract requires $q$ hogs. A regular-weight hog sent to the contract earns $p^C_t$; an underweight one earns $(1-\alpha)p^C_t$. Open-market prices are $p^1_t\le p^2_t$. Holding costs $c^H_t$ per hog, and a contract shortfall costs $c^P_t$ per missing hog. The discount factor is $\beta$.

The decision is $y_t=(y^1_t,y^2_t)$ sent to the contract and $z_t=(z^1_t,z^2_t)$ held. Open-market sales are $x^i_t=s^i_t-y^i_t-z^i_t$. Every decision is nonnegative; $y^1_t+y^2_t\le q$ and $y^i_t+z^i_t\le s^i_t$. The immediate reward is

$$r_t=p^C_t\bigl(y^2_t+(1-\alpha)y^1_t\bigr) +\sum_{i=1}^{2}p^i_t(s^i_t-y^i_t-z^i_t) -c^H_t(z^1_t+z^2_t)-c^P_t(q-y^1_t-y^2_t).$$

Newly available hogs next period are $W_{t+1}=(W^1_{t+1},W^2_{t+1})$. Both classes of held hogs enter the regular-weight pool, so $S_{t+1}=(W^1_{t+1},W^2_{t+1}+z^1_t+z^2_t)$. The value function $V_t$ is the maximum expected discounted reward from periods $t$ through $t_M$, with $V_{t_M+1}=0$, as in equations (4) and (7a)–(7c) of the preprint.

For total holding $Z$, write $G_t(Z)=\beta\mathbb E_t[V_{t+1}(W^1_{t+1},W^2_{t+1}+Z)]-c^H_t Z$. Its increments are the holding margin. The fulfillment margins are $(1-\alpha)p^C_t+c^P_t$ and $p^C_t+c^P_t$; the spot margins are $p^1_t$ and $p^2_t$. A break-even level for margin $v$ is the least nonnegative $Z$ at which every forward increment of $G_t$ is no greater than $v$ times the increment. The mission uses this level truncated at $s^1_t+s^2_t$.

Formalization targets

The first targets are concavity of the value and action-value functions (Lemma 1), preservation of concavity in total holdings (Proposition 1, proof Step 1), and the holding-margin bound corresponding to Lemma 2(1). The one-period attainment result from Proposition 1, proof Step 2, connects those properties to the explicit actions. These are the four milestones.

The goal is the corrected part of Proposition 1, Cases 1(a), 1(b), 2(a), and 2(b). In each case, the indicated action must satisfy the feasibility constraints and attain the dynamic-programming value:

$$v_t(y_t,z_t;s_t,P_t)=V_t(s_t,P_t).$$

The cases split first on $p^2_t>p^C_t+c^P_t$ or $p^2_t\le p^C_t+c^P_t$, then on the underweight fulfillment and spot margins. The explicit quantities are in the goal theorem. Its thresholds are computed from $G_t$ and the observed stock and prices, so the target is a policy for the original dynamic program. Proposition 1 also prints Case 2(c), but its multi-period formula is false under the paper’s stated assumptions and the additional no-arbitrage bound below; this mission does not assert it.

What the result provides

The result identifies feasible, optimal contract, spot-market, and holding quantities in four observable price regimes. It gives a policy rather than an existence statement: a producer can determine the action from the current stock, prices, and three break-even levels. The holding thresholds are linked to the actual continuation value, which matters when future penalties or regular-weight prices change.

The preprint supplies a proof on paper; these particular Lean statements do not yet have verified proofs. Formalizing them would yield a checked dynamic program and reusable facts about a concave continuation value, a shared holding pool, and a linear contract capacity. The corrected statement also separates the regimes that the available numerical checks support from the printed Case 2(c), which has a concrete counterexample. The four milestones expose the mathematical obligations needed to complete the verified result.

Main difficulty

The continuation value depends on the sum $z^1_t+z^2_t$, while the two pools have different fulfillment and spot prices and share one contract capacity. A comparison of each pool’s holding and selling margins in isolation therefore does not settle the allocation: holding one pool changes the marginal value of holding the other. The dynamic value is also defined by a supremum over a continuous feasible polytope and an expectation over future data. The central difficulty is obtaining a well-defined, concave value function and then showing that each explicit threshold action attains it. The paper’s no-arbitrage assumption controls expected contract and spot price changes, but does not control a jump in the next period’s contract penalty; Lemma 2(1) fails without an additional bound.

Formalization scope

Lean uses real-valued stocks and decisions, a positive finite horizon, and a time-indexed Markov kernel on an exogenous information state $\omega$. Taking $\omega$ to include the observed history represents the paper’s general adapted price and supply process; the formalization imposes no independence between supply and prices. Prices and supplies are measurable, nonnegative, and uniformly bounded. These are disclosed well-posedness additions that keep the expectations integrable and the real supremum finite. It also assumes $0<\beta\le1$, $q>0$, $0<\alpha<1$, and $p^1_t\le p^2_t$.

Assumption 1 from page 14 is retained. The added condition A* bounds the discounted expected next-period maximum of the regular-weight fulfillment and spot margins by the present maximum plus holding cost. Without it, a two-period instance with next-week penalty $100$ makes the printed Lemma 2(1) policy worth $-80$ while holding is worth $8$. The corrected Case 1(b) holding quantity is the unsold underweight stock capped by its spot break-even level. Case 2 uses a regular-weight holding threshold net of already held underweight hogs. The printed Case 2(c) can yield $87$ when a feasible action yields $103$, so it is excluded. These departures are recorded item by item in the moderation notes.

The definition layer contains the reward, feasible actions, Bellman recursion, continuation value, and break-even levels. A complete proof also needs measurability and integrability of the recursively defined value, compact feasible sets, concavity under integration and partial maximization, and real infimum properties. Contributions to those reusable results, the four milestones, and the corrected goal are within scope. A formulation with free thresholds or a free value function would make the policy claim empty; both are computed from the model data here.

Selected references

• P. Kouvelis, Y. Liu, Y. Qiu and D. Turcic, Managing Operations of a Hog Farm Facing Volatile Markets: Inventory and Selling Strategies, SSRN preprint 3912801, March 6, 2023; subsequently Manufacturing & Service Operations Management, DOI 10.1287/msom.2023.1216. Preprint.

Motivation

When a financial institution fails, its counterparties on over-the-counter derivatives are exempt from the automatic stay of bankruptcy: they may terminate their contracts at once, accelerate what is owed to them, and seize posted collateral. Whether this exemption stabilizes or destabilizes the system has been debated since the 1990s, and the failure of Lehman Brothers in 2008 sharpened the question. Termination turns contingent contract values into immediate payment obligations, which can push further institutions into default. But it also brings cash into the system and frees collateral, which can let other obligations be met.

Ghamami, Glasserman and Young (Management Science, 2022) build a clearing model in which payments, collateral seizure, returned collateral and contract termination interact over successive rounds. They compare two policies. Under full termination the default of a node accelerates every derivative contract it is party to, in both directions. Under selective termination (creditor "cherry-picking") only the obligations of the defaulted node become due. Their headline comparison is that, under a bound on aggregate derivatives leverage, full termination leaves no larger system-wide payment shortfall than selective termination.

Setting

A finite set $\mathcal N$ of $N$ nodes. For nodes $i, j$: $\bar p_{ij} \ge 0$ is the payment due from $i$ to $j$, with total $\bar p_i = \sum_k \bar p_{ik}$; $c_i \ge 0$ is the cash of $i$; $m_{ij} \ge 0$ is the collateral posted by $i$ for its obligations to $j$; $v_{ij} \ge 0$ is the value to $j$ of its derivatives with $i$, owed by $i$ on termination, with $v_i = \sum_j v_{ij}$. Diagonals vanish and obligations are netted ($\bar p_{ij}\bar p_{ji} = v_{ij} v_{ji} = 0$). Collateral has constant value $1$.

Round 1. Given payments $p^{(1)}$, node $i$ has assets $A^{(1)}_i = c_i + \sum_k p^{(1)}_{ki}$ and defaults if $A^{(1)}_i < \bar p_i$; $D^{(1)}$ is the default set. A creditor $j$ of a defaulted $i$ first seizes $\Delta_{ij} = m_{ij} \wedge \bar p_{ij}$, and the rest of $i$'s assets is shared pro rata over the residual claims $[\bar p_{ij} - m_{ij}]^+$. Clearing payments are the nonnegative solutions of these fixed-point equations. Excess collateral is returned after Round 1: a defaulted node gets back what was not seized, a surviving node gets back what it had posted to defaulted nodes.

Proposition 2.1 also treats a Round 2 without derivative termination: remaining obligations are $\bar p_{ij}-p^{(1)}_{ij}$, paid from returned collateral and incoming payments. Its total-payment identity (15) is included.

Rounds $m = 2, \dots, N$ under full termination. A default in round $m-1$ creates the obligation $v_{ij}$ between the defaulted node and each counterparty that has survived; unpaid obligations carry over; two survivors owe each other nothing. A node's assets in round $m$ are its cash $c^{(m)}_i$, its returned collateral $r^{(m)}_i$ and the payments it receives; it defaults in round $m$ if they fall short of its round-$m$ obligations, and payments again solve a pro rata fixed-point equation. $D^f = \bigcup_l D^{(l)}$ is the full-termination default set.

Selective termination shares Round 1, and in Round 2 only defaulted nodes owe: $\bar q^{(2)}_{ij} = v_{ij} + \bar p_{ij} - p^{(1)}_{ij}$ for $i \in D^{(1)}$, else $0$. No node defaults after Round 1, and payments $q^{(2)}$ solve the Round-2 equation.

The payment shortfalls are

$$L^f = \sum_{i \in D^f} (v_i + \bar p_i - p_i), \qquad L^s = \sum_{i \in D^{(1)}} (v_i + \bar p_i - q_i),$$

with $p_i$ the total paid by $i$ over all rounds and $q_i$ its total over the two selective rounds. The net worth at the end of Round 1 is $e_i = c_i + r_i + \sum_k p^{(1)}_{ki} - \bar p_i$.

Formalization targets

Goal: Proposition 5.2 (i)

With constant collateral price, common first-round payments, and both models taken at their largest, or both at their smallest, second-round clearing payments ((37) or (38)), the aggregate derivatives leverage condition

$$\sum_{i \in D^f - D^{(1)}} v_i \;\le\; \sum_{i \in D^f - D^{(1)}} e_i \tag{40}$$

implies

$$L^f \le L^s .$$

Milestones

1. Existence and total-payment identity of the two-round freed-collateral model (Proposition 2.1), and existence of clearing payments in every round of full termination (Proposition 4.1).
2. No collateral is seized after Round 1: $\Delta^{(m)} = 0$ for $m \ge 2$.
3. Round-2 comparison of parameters: $\bar p^{(2)} \ge \bar q^{(2)}$ and $a^{(2)} \ge \hat a^{(2)}$; existence of extremal round-2 solutions in both models.
4. Lemma 5.1: $p^{(2)}_{ij} \ge q^{(2)}_{ij}$ at the largest, or at the smallest, solutions.
5. Freed-collateral Round 2 node totals; a node in $D^f - D^{(1)}$ pays at least $e_i$ after Round 1; the shortfall identity (67)–(68).

Significance

The result. Proposition 5.2 is the paper's formal answer to the policy question raised by the safe-harbor debate: it identifies a balance-sheet condition, derivatives liabilities bounded by equity in aggregate, under which the stay exemption does not worsen the total amount of unpaid obligations, even though full termination always produces at least as many defaults (Proposition 5.1). The paper's Example 5.1 shows that without such a condition the comparison can go either way and by arbitrary amounts.

Formalizing it. The paper gives proofs; none is machine-checked. A formalization fixes the accounting of a multi-round collateralized clearing model precisely. This matters here: read literally, the cash recursion of §4 drops unsold returned collateral, and with it Proposition 5.2 (i) fails on a four-node network. The mission states the repaired accounting under which the paper's argument goes through. It also produces reusable statements about extremal fixed points of Eisenberg–Noe-type clearing maps with collateral and their monotone comparison.

Difficulty

The two models are compared at fixed points of different maps, and fixed points need not be unique; a pointwise comparison of arbitrary solutions is false in general. The comparison has to be made at extremal fixed points, through monotone comparative statics in the parameters (obligations and pro rata proportions), and both the largest and the smallest cases are needed. Second, full termination runs up to $N$ rounds with new defaults in each; the shortfall bound requires tracking each node's cash, returned collateral and payments across rounds, and showing that a node defaulting after Round 1 has paid out at least its Round-1 net worth. The tempting shortcut, assuming that full termination creates no new defaults ($D^f = D^{(1)}$), turns the goal into Corollary 5.1, a different and weaker statement.

Formalization scope

All values are real numbers; nodes form a Fintype with decidable equality. One definitions file CollatNet.Termination.Model holds the network, its standing assumptions, Round 1, the §2.3 freed-collateral Round 2, a round state (cash, returned collateral, obligations, survivors), the full-termination round map, the selective Round 2, default sets, shortfalls and net worth. Conventions:

• The collateral price is $1$ throughout (case (i)); prices do not appear.
• Sums over $k \ne i$ are written over all $k$; zero diagonals make them equal.
• A pro rata proportion with zero denominator is $0$, as on the page.
• Clearing payments are nonnegative, i.e. lie in the box $[0, \bar p]$ of the paper's fixed-point argument; otherwise negative circular "payments" would solve the equations.
• Defaults are strict: assets $<$ obligations.
• The number of rounds is $R = \max(2, N)$; payment sequences are indexed by rounds $\ell \in \mathbb N$ and only $\ell = 1, \dots, R$ are used.
• Repaired cash recursion (disclosed): $c^{(m+1)}_i = c^{(m)}_i + r^{(m)}_i + \sum_k p^{(m)}_{ki} - \sum_k (p^{(m)}_{ik} - \Delta^{(m)}_{ik})$. Unsold returned collateral is carried as cash, and seized collateral is not paid out of cash.
• "Largest/smallest second-round payments" are IsGreatest/IsLeast in the componentwise order on each model's round-2 clearing set; later full-termination rounds may be any clearing payments.
• Selective termination is modelled through Round 2 only, as in the appendix's formula (64).

Case (ii) of Proposition 5.2 (illiquid collateral, no excess collateral) is not posed: it is false as printed, because returned collateral is sold below its Round-1 value.

The goal must keep (40) as its hypothesis. Replacing (40) by $D^f = D^{(1)}$, or dropping the later full-termination rounds (which forces $D^f = D^{(1)}$ by construction), would state Corollary 5.1 instead.

Needed infrastructure: Knaster–Tarski on boxes in $\mathbb R^{\mathcal N \times \mathcal N}$ (Mathlib's OrderHom.lfp/gfp), a monotone comparison of extremal fixed points, and finite-sum bookkeeping over rounds. The extremal-fixed-point comparison and the node-total property of pro rata clearing are reusable for other clearing models. Proofs of any milestone are welcome; the shortfall identity and the dominance of round-2 parameters are the most self-contained.

Selected references

• S. Ghamami, P. Glasserman, H. P. Young, Collateralized networks, Management Science 68(3):2202–2225, 2022. https://doi.org/10.1287/mnsc.2020.3938 (accepted manuscript: LSE Research Online 107496, https://eprints.lse.ac.uk/107496/)
• L. Eisenberg, T. H. Noe, Systemic risk in financial systems, Management Science 47(2):236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• P. Milgrom, J. Roberts, Comparing equilibria, American Economic Review 84(3):441–459, 1994. https://www.jstor.org/stable/2118061
• A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2):285–309, 1955. https://doi.org/10.2140/pjm.1955.5.285

Motivation

Firms that collaborate on research and development must share proprietary knowledge to make the collaboration work, yet the knowledge they share can later be used against them: a partner that has learned from the alliance can walk away and use what it learned on a rival project. Management research calls this the appropriability hazard of alliances. Arora, Belenzon and Patacconi (Management Science, 2021) model knowledge sharing as a property-rights problem in the tradition of Grossman–Hart and Hart and Moore (1990): knowledge sharing is an ex ante investment that shifts the partners' ex post outside options, and payoffs are fixed by bargaining after the investment is sunk.

The paper's main structural question is whether a firm can mitigate the hazard by organising its collaborations as a portfolio of alliances rather than as a single alliance. The answer it gives, Proposition 6, is that it can: there is a range of parameters in which a single alliance cannot sustain knowledge sharing while a portfolio of two alliances can.

Setting

Single alliance (§2). A focal firm $F$ and a partner $A$ each pay a private cost $\tfrac12 I$, with $I > 0$, to share knowledge. After sharing, implementing the project together creates value $V$; if the alliance is terminated prematurely, $F$ and $A$ obtain their ex post outside options $\pi_F$ and $\pi_A$. It is assumed that $V \ge \pi_F + \pi_A$. Bargaining follows the Nash solution with equal weights, so firm $i \in \{F, A\}$ obtains

$$\Pi_i = \pi_i + \tfrac12\,[V - \pi_F - \pi_A] - \tfrac12 I .$$

Firm $i$'s knowledge-sharing constraint is $\Pi_i \ge 0$. Knowledge sharing is efficient if $V \ge I$.

Alliance portfolio (§4.1). The focal firm now has two partners $A$ and $B$, on the player set $N = \{F, A, B\}$. The partners' outside options are normalised to $\pi_A = \pi_B = 0$. After knowledge sharing in both alliances, the value $v(S)$ created by a coalition $S$ that implements together while its alliances with outsiders are terminated is (Table 1)

$$v(FAB) = 2V + b,\qquad v(FA) = v(FB) = V + \pi_F + s^{Imp},\qquad v(AB) = 0,$$ $$v(F) = 2\pi_F - s^{RB},\qquad v(A) = v(B) = 0,$$

with $v(\emptyset) = 0$. The parameter $b \ge 0$ is the synergy between $A$ and $B$ in implementation, $s^{Imp} \in [0, V - \pi_F]$ measures substitutability in implementation and $s^{RB} \in [0, \pi_F]$ measures substitutability in rival benefits. Gross payoffs are the Shapley value

$$\varphi_i = \sum_{S \subseteq N\setminus\{i\}} \frac{|S|!\,(|N|-|S|-1)!}{|N|!}\bigl(v(S \cup \{i\}) - v(S)\bigr),$$

and since $F$ bears $\tfrac12 I$ in each of its two alliances, the net payoffs are $\Pi_F = \varphi_F - I$, $\Pi_A = \varphi_A - \tfrac12 I$ and $\Pi_B = \varphi_B - \tfrac12 I$. Knowledge sharing in a configuration is feasible when every firm's knowledge-sharing constraint holds.

Formalization targets

Goal: Proposition 6

Under the standing assumptions, suppose $V \ge I$. If

$$V - I \in \Bigl[\pi_F - \tfrac23 b + \tfrac13\bigl(s^{Imp} - s^{RB}\bigr),\ \pi_F\Bigr),$$

then knowledge sharing in the portfolio is feasible ($\Pi_F, \Pi_A, \Pi_B \ge 0$), while knowledge sharing in the single $F$–$A$ alliance (with $\pi_A = 0$) is not.

Milestones

1. Proposition 1 (p. 10): in a single alliance, both constraints hold if and only if $V - I \ge |\pi_F - \pi_A|$.
2. §4.1, p. 21: in the single $F$–$A$ alliance with $\pi_A = 0$, both constraints hold only if $V - I \ge \pi_F$.
3. Equation (9) (p. 23): $\varphi_F = V + \pi_F + \tfrac13 b + \tfrac13(s^{Imp} - s^{RB})$.
4. Equation (10) (p. 23): $\varphi_A = \varphi_B = \tfrac12(V - \pi_F) + \tfrac13 b - \tfrac16(s^{Imp} - s^{RB})$.
5. Equation (11) (p. 24): $\Pi_A, \Pi_B \ge 0$ if and only if $V - I - \pi_F + \tfrac23 b - \tfrac13(s^{Imp} - s^{RB}) \ge 0$.

Significance

The result. Proposition 1 shows that in a single alliance, efficiency ($V \ge I$) does not imply investment: shifts in bargaining positions, measured by $|\pi_F - \pi_A|$, create underinvestment. Proposition 6 identifies a structural remedy. A second partner changes the bargaining game: the synergy $b$ is created only when all three firms cooperate, and substitutability in rival benefits $s^{RB}$ weakens the focal firm's threat point, both of which raise the weak partners' Shapley payoffs. The paper uses this to argue that alliance portfolios with the right characteristics can sustain knowledge sharing that a dyadic alliance cannot, and that substitutability among partners is not uniformly harmful.

Formalizing it. The proofs are relegated to an online appendix that is not part of the source manuscript, so the mission produces the first complete, checked derivation of the portfolio result from the model's primitives: the Table 1 game, the Shapley value and the cost allocation. A search of the platform found none of these statements already formalized; the Shapley value itself is reused from an existing platform definition.

Difficulty

The computations are finite and elementary, so the difficulty lies in carrying out the Shapley sum over all coalitions of a three-player game honestly, rather than by quoting the closed forms (9)–(10), and in tracking the asymmetric cost allocation: the focal firm pays $I$, the partners $\tfrac12 I$ each. A second point is that the paper assumes the focal firm's constraint $\Pi_F \ge 0$ "to facilitate the comparison"; the formal goal concludes it from $V \ge I$ and the standing ranges, so it must be derived, not assumed.

Formalization scope

Players are Fin 3 with $F = 0$, $A = 1$, $B = 2$; all parameters are real numbers. The game game V b πF sImp sRB assigns $0$ to every coalition without $F$ and, to a coalition containing $F$, the Table 1 value determined by its size, with $v(\emptyset) = 0$. The gross payoffs are the platform's published Supermodularity.Cooperative.ShapleyValue applied to this game. Single-alliance payoffs follow eq. (1), and both notions of feasibility are defined from the payoffs: SingleFeasible is $\Pi_F \ge 0 \wedge \Pi_A \ge 0$, PortfolioFeasible is $\Pi_i \ge 0$ for every player. The standing assumptions $I > 0$, $b \ge 0$, $0 \le s^{Imp} \le V - \pi_F$ and $0 \le s^{RB} \le \pi_F$ are bundled in Standing. "Feasible" refers only to the knowledge-sharing constraints; the coordination problem of the investment game (footnote 10) is ignored, as in the paper.

A trivializing formalization would define $\varphi$ by the closed forms (9)–(10) or feasibility by the inequalities (5) or (11), which would make the milestones true by definition and the goal a linear inequality between its own hypotheses; the definitions here are the Shapley sum and the payoff constraints, so those closed forms must be proved.

No probability, measure theory or analysis is needed; a development needs finite sums over the powerset of Fin 3 and linear arithmetic over ℝ. A reusable by-product is a computation of the Shapley value for three-player games with a distinguished player, which recurs in property-rights models. Proofs of the milestones and of the goal, in any order, are welcome.

Selected references

• A. Arora, S. Belenzon, A. Patacconi, Knowledge sharing in alliances and alliance portfolios, Management Science, 2021 (author manuscript of January 24, 2020). https://doi.org/10.1287/mnsc.2020.3614
• O. Hart, J. Moore, Property rights and the nature of the firm, Journal of Political Economy 98(6), 1990. https://doi.org/10.1086/261729
• L. S. Shapley, A value for n-person games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953. https://doi.org/10.1515/9781400881970-018