Operations Research

Motivation

A secretary problem asks a decision maker to choose one candidate from a sequence, without being able to recall a rejected candidate. Each arrival reveals how the candidate compares with those seen earlier, but the decision maker does not know the candidate's final rank. A classifier can provide an additional Yes or No signal about whether the current candidate is the best overall. The natural performance question is how much this signal improves the chance of selecting the best candidate when the number of arrivals grows. Dütting, Lattanzi, Paes Leme and Vassilvitskii give an exact finite linear program for this setting and an explicit asymptotic value. This mission makes the limit and its finite prerequisites precise.

The classifier's quality has two parameters with different meanings. Recall $p$ is the probability of a Yes signal for the top candidate. Specificity $p'$ is the probability of a No signal for any other candidate. Both lie in $[1/2,1]$, as in Example 5 of the paper. At $p=p'=1/2$ the signal conveys no information, while $p=p'=1$ is perfect advice. These endpoints matter to the statement rather than being omitted as special cases. Example 5, pp. 7–8.

Setting

There are $n\ge1$ arrivals, indexed by $i=1,\ldots,n$. Their ranks form a uniformly random permutation; the maximum rank is the candidate to select. At each arrival, the observer sees the relative ranking of candidates already seen and a signal $s\in\{Y,N\}$ from the classifier. An admissible decision can depend on this observed history and may use a stopping probability. It cannot inspect a candidate's hidden final rank. The paper shows that, for this signal model, the optimal stopping probability is characterized by a finite primal linear program. Sections 2 and 6.

For each round and signal, $z_i^s\in[0,1]$ is a primal variable. Put $\bar z_j=(1-p')z_j^Y+p'z_j^N$. The program has constraints $z_i^s\le1-\sum_{j<i}\bar z_j/j$, and its objective is $\sum_{i=1}^n[pz_i^Y+(1-p)z_i^N]/n$. Write $\operatorname{Opt}(n,p,p')$ for its optimal value. The constraints account for the chance that an earlier candidate has already been selected; the objective weights winning selections by the signal probabilities of the top candidate. This is the $\operatorname{Opt}$ of Section 6, rather than a value defined by an asymptotic formula. Section 6, p. 20.

The paper also considers a rescaled dual with variables $w_i^Y,w_i^N$ and an associated pair of thresholds $t_Y,t_N$. The thresholds are the first rounds at which the corresponding greedy dual coordinate is positive. In the finite formalization, $n+1$ records a signal whose coordinate is never positive. Proof of Theorem 20, p. 21.

Formalization targets

The main target is the limiting primal optimum for every $p,p'\in[1/2,1]$:

$$\lim_{n\to\infty}\operatorname{Opt}(n,p,p') =\left(\frac{1-p'}p\right)^{(1-p')/p'} \exp\left(\frac{p-1}{p'}\right).$$

The finite milestones identify the primal optimum with the greedy dual objective, give the exact late dual coordinates and the exact range of the early $Y$ recursion, and establish $t_Y\le t_N$. The asymptotic milestones state

$$\frac{t_N}{n}\longrightarrow \exp\left(\frac{p-1}{p'}\right),\qquad \frac{t_Y}{n}\longrightarrow \left(\frac{1-p'}p\right)^{1/p'}\exp\left(\frac{p-1}{p'}\right).$$

A separate companion target gives the finite lower bound $\operatorname{Opt}(n,p,p')\ge L(p,p')$, where $L$ denotes the displayed limit. Theorem 20 states the corresponding infimum inequality but does not separately prove it. Theorem 20 and its proof, pp. 20–22.

Significance

The limit quantifies the benefit of advice across the whole parameter square, including asymmetric classifiers. It recovers the classical value $e^{-1}$ when $p=p'=1/2$, and gives value $1$ for perfect advice. The two threshold limits say when each signal begins to justify stopping as the horizon grows. Thus the result specifies both the achievable success probability and the scale of the optimal decisions. Theorem 20, p. 20.

The paper already proves threshold optimality through its linear program and presents the limit calculation. The formalization work here is to establish a full Lean limit theorem from an exact finite LP, including the two endpoint regimes and a finite dual characterization. The nearby classical secretary threshold limit on Prove2Me uses a different rank-based model; it does not state this classifier result. Definitions of the primal feasible set and the backward dual sequence can support later results about other advice distributions.

Difficulty

The source uses approximations throughout its asymptotic argument and explicitly omits terms that vanish as $n$ grows. Those omissions cannot be carried into an exact finite statement: the $Y$ recursion, for example, fails at the round immediately before the $N$ threshold because the next $N$ dual coordinate is then present. A complete argument has to keep the discrete threshold boundaries and the harmonic sums under control while passing to a limit. The source's displayed theorem also contains an exponent inconsistent with the last equation of its proof; the corrected expression must be checked uniformly, including zero base at $p'=1$. Proof of Theorem 20, pp. 21–22.

Formalization scope

Lean represents time by natural numbers $1,\ldots,n$, matching the paper's displayed LP, and signals by Bool, with true meaning $Y$. The primal optimum is the real supremum of objective values over exactly the feasible LP variables. For $n\ge1$ and $p,p'\in[1/2,1]$, the zero assignment is feasible and the objective is bounded, so this supremum has its ordinary optimization meaning. Values of a variable array outside $1,\ldots,n$ are ignored. The greedy dual is a backward finite recursion, not the definition of $\operatorname{Opt}$; otherwise the central LP-to-dual milestone would disappear.

The formal thresholds are first positive greedy dual coordinates. If there is no positive $N$ coordinate, $t_N=n+1$; this occurs when $p=1$ and has the same normalized limit as the paper's informal $t_N=n$ convention at perfect advice. Real powers use Lean's $0^0=1$, yielding the correct $p'=1$ endpoint. All theorems quantify explicitly over $n\ge1$ where finite rounds are used, and over $p,p'\in[1/2,1]$. The limit uses Filter.Tendsto at infinity. The chapter does not formalize the algorithmic running time, Figures 3 and 7, or the policy-level threshold optimality addressed by the series' preceding mission. Contributions to finite LP duality, harmonic asymptotics, and endpoint analysis are within scope. Sections 6 and Appendix C.

Selected references

• Paul Dütting, Silvio Lattanzi, Renato Paes Leme and Sergei Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; published in Mathematics of Operations Research, 2024. Preprint.

Motivation

Regret bounds for reinforcement learning in a single, non-episodic Markov decision process (MDP) are stated in terms of the diameter $D$ of the MDP: the worst expected time needed to travel between two states when the travel policy is chosen well. UCRL2 (Jaksch, Ortner and Auer, 2010) achieves regret $\tilde O(DS\sqrt{AT})$, against a lower bound of $\Omega(\sqrt{DSAT})$, by planning in an extended MDP, whose action set lets the planner also pick a transition law from a confidence set. Posterior-sampling methods replace the confidence set with random samples from a posterior. Agrawal and Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023) show that such a method attains a high-probability worst-case regret bound of $\tilde O(DS\sqrt{AT})$ for every communicating MDP (their Theorem 1).

Their analysis plans in an extended MDP built from finitely many sampled transition vectors. Optimal-gain policies of that MDP are only useful if it is itself communicating with a diameter comparable to $D$, so the paper needs a deterministic statement: if every state-action pair has a sample that is optimistic about travel times, the diameter of the extended MDP is at most $D/(1-\delta)$. This mission formalizes that statement, Lemma 5.6 of the paper (p. 12), together with three claims from its proof.

Setting

A finite MDP $\mathcal M$ has a finite state set $\mathcal S$ of size $S$, a finite action set $\mathcal A$ of size $A$, a probability vector $P_{s,a}\in\Delta^{S}$ for each state $s$ and action $a$, and rewards $r_{s,a}\in[0,1]$. A deterministic policy is a map $\pi:\mathcal S\to\mathcal A$; under $\pi$ the state process is the Markov chain with transition rows $P_{s,\pi(s)}$.

For states $s'$ and $s$, $T^{\pi}_{s'\to s}\in[0,\infty]$ is the expected number of steps to reach $s$ when starting at $s'$ and following $\pi$. It is $0$ when $s'=s$. The diameter is

$$D(\mathcal M)=\max_{s\neq s'}\ \min_{\pi:\mathcal S\to\mathcal A} T^{\pi}_{s\to s'},$$

and $\mathcal M$ is communicating when $D(\mathcal M)<\infty$ (Definitions 1–3, p. 3). For a target $s$, the vector $E^{s}$ collects the minimum expected times, $E^{s}_{s'}=\min_{\pi}T^{\pi}_{s'\to s}$, so $E^{s}_{s}=0$.

The extended MDP (§3, p. 5) starts from $\psi$ probability vectors $Q^{1}_{s,a},\dots,Q^{\psi}_{s,a}$ for every pair $(s,a)$. In the algorithm these are posterior samples, but here they are arbitrary. The extended MDP $\tilde{\mathcal M}$ has the same states and, for every action $a$, the actions $a^{1},\dots,a^{\psi}$. Taking $a^{j}$ in $s$ gives reward $r_{s,a}$, and the next state is drawn from $Q^{j}_{s,a}$. Its diameter $D(\tilde{\mathcal M})$ is defined as above, minimizing over policies $\tilde\pi:\mathcal S\to\{a^{j}\}$.

Formalization targets

Goal: Lemma 5.6

Let $\delta\in[0,1)$. Suppose that for every target state $s$, every state $s'$ and every action $a$ there is a sample index $j$ with

$$Q^{j}_{s',a}\cdot E^{s}\ \le\ P_{s',a}\cdot E^{s}+\delta. \tag{16}$$

Then

$$D(\tilde{\mathcal M})\ \le\ \frac{D(\mathcal M)}{1-\delta}.$$

Milestones (claims of the proof, p. 13)

1. In a communicating MDP with at least one action, for every target $s_2$ there is one deterministic policy $\pi$ with $T^{\pi}_{s'\to s_2}=E^{s_2}_{s'}$ for every $s'$.
2. First-step analysis: for every policy $\pi$ and $s\neq s_2$,

$$T^{\pi}_{s\to s_2}=1+\sum_{s'\neq s_2}P_{s,\pi(s)}(s')\,T^{\pi}_{s'\to s_2}.$$

3. Comparison (display (17)): if $E\in[0,\infty]^{\mathcal S}$ satisfies $1+\sum_{s'\neq s_2}Q_{s,\tilde\pi(s)}(s')E_{s'}\le E_s+\delta$ for all $s\neq s_2$, then $(1-\delta)\,T^{\tilde\pi}_{s\to s_2}\le E_s$ for all $s\neq s_2$.

Significance

The result. Lemma 5.6 turns a per-pair, one-sided condition on samples into a global bound on the diameter. Agrawal and Jia combine it with their Lemma 5.7, which shows that (16) holds with $\delta\le 1/2$ with high probability for their posterior samples. Together these give $D(\tilde{\mathcal M}^{k})\le 2D$ in every epoch, which is what lets the bias span of the sampled MDP enter their regret analysis. The lemma is deterministic and makes no use of how the samples were drawn, so it applies to any optimistic-sampling or perturbation scheme that produces vectors satisfying (16).

Formalizing it. The lemma is proved in the paper; no machine-checked version exists. The paper's proof assumes that every sampled entry is strictly positive ("drawn from Dirichlet distribution") so that the absorbing chain and its fundamental matrix are well defined. That assumption fails for the simple optimistic samples of the same algorithm, which can have zero entries. The statements here drop it, so a formal proof also settles the general case. Milestones 1 and 2 are standard facts about minimum expected hitting times (stochastic shortest paths) that the platform's finite-MDP library does not yet contain. They are reusable for any diameter-based regret analysis.

The main regret bound (Theorem 1) is not posed. Its constants are hidden in $O(\cdot)$, and the algorithm's parameters are given only up to $\Theta(\cdot)$.

Difficulty

The paper's argument inverts $I-Q^{\dagger}_{\tilde\pi}$ and uses the nonnegativity of the fundamental matrix of an absorbing chain. Without positive entries the policy $\tilde\pi$ can have closed classes that avoid the target, so $I-Q^{\dagger}_{\tilde\pi}$ can be singular and the matrix argument does not apply as written. The comparison has to be made with expected travel times that may be infinite.

A second obstacle is that (16) constrains only the minimizing vectors $E^{s}$ of the true MDP. The bound therefore needs a policy of $\mathcal M$ whose travel times equal $E^{s_2}$ from every state at once, not merely from the starting state $s_1$. The existence of such a uniformly optimal deterministic policy is not immediate from the definition of the diameter, which minimizes separately for each pair of states.

Finally, the platform's expected travel time is defined through finite-horizon trajectory laws, so first-step analysis is a Markov-property computation on those measures. It does not follow from the definition by unfolding alone.

Formalization scope

• Library. The mission reuses the published definitions FiniteMDPLearning (namespace BanditAlgorithm): FiniteMDP S A, mdpTravelTime M f src tgt (the expected hitting time minus one, valued in $[0,\infty]$, equal to $T^{f}_{src\to tgt}$), and mdpDiameterENN M (Definition 2 verbatim, valued in $[0,\infty]$). The mission's own definitions file adds extendedMDP, extendedAction and minTravel (the vector $E^{s}$).
• Indexing. States, actions and samples are 0-based (Fin S, Fin A, Fin ψ). The action $a^{j}$ of the extended MDP is finProdFinEquiv (a, j) : Fin (A * ψ). The epoch index $k$ plays no role and is dropped.
• Extended values. Travel times, diameters, the vectors $E^{s}$ and the inner products $Q\cdot E^{s}$ are computed in $[0,\infty]$ with $0\cdot\infty=0$. The bound $D/(1-\delta)$ is division in $[0,\infty]$ by the positive real $1-\delta$, with $\delta\in[0,1)$ as δ : ℝ≥0, δ < 1.
• Quantifiers of (16). The printed (16) uses the letter $s$ both for the target of $E^{s}$ and for the state in $P_{s,a}$. The proof applies it at the current state with a different target, so the goal quantifies the target separately: for every target, state and action there is a sample.
• Pinned hypotheses. Milestone 1 assumes $D(\mathcal M)<\infty$ (the paper's "$\mathcal M$ has diameter $D$") and $A\ge1$. The goal assumes neither: if $D(\mathcal M)=\infty$ its bound is trivially true, so it generalizes the paper's statement. No statement assumes positivity of the sampled entries or any distribution of the samples.
• Ruled-out trivializations. An extended MDP whose transitions ignore $j$ or $Q$, an $E^{s}$ that is not the infimum over policies, a hypothesis comparing $Q$ and $P$ against different vectors, and a real-valued conclusion through a truncation with junk value $0$ for non-communicating MDPs would each make the goal vacuous or different. None is used.
• Useful existing result. The platform has the proved drift criterion BanditAlgorithm.mdp_travel_time_le_of_lyapunov_drift (a real-valued nonnegative $V$ with $\sum_{s'}P_{s,f(s)}(s')V(s')+1\le V(s)$ off the target bounds the travel time by $V$), which covers the case $\delta=0$ of milestone 3 for finite $E$.
• Welcome contributions. Proofs of the three milestones and of the goal; a general first-step (Markov property) lemma for mdpMeasure; an existence theorem for uniformly optimal deterministic policies of minimum expected hitting time.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic posterior sampling for reinforcement learning: worst-case regret bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• D. P. Bertsekas and J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Mathematics of Operations Research 16(3), 1991. https://doi.org/10.1287/moor.16.3.580
• C. M. Grinstead and J. L. Snell, Introduction to Probability, American Mathematical Society, 2nd revised edition, 1997 (Chapter 11, absorbing Markov chains). https://math.dartmouth.edu/~prob/prob/prob.pdf
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (Chapter 38, MDPs and the diameter). https://tor-lattimore.com/downloads/book/book.pdf

Why blockchain adoption in supply chains is an economic question

A permissioned blockchain is a shared ledger that only invited parties may write to. In supply chains it is promoted as a way to make the provenance and quality of goods verifiable by the end consumer: a manufacturer who joins records how a good was produced, and consumers can read that record. Joining is costly, and the parties who pay the cost are not the parties who benefit most from the information. Whether such a technology is adopted at all is therefore a question about incentives, not engineering.

G. Iyengar, F. Saleh, J. Sethuraman and W. Wang, Economics of Permissioned Blockchain Adoption (SSRN 3602376; Management Science, 2023, DOI 10.1287/mnsc.2022.4532), build a stylised supply chain with vendors, price-competing manufacturers and consumers with an outside option, and show that welfare-improving adoption can fail to arise in equilibrium. This mission formalizes the first of the paper's two main results, Proposition 4.8, together with the welfare comparisons it rests on. A companion mission formalizes the second, the self-financing transfers of Proposition 4.9.

The supply chain

There are two vendors, of high and low quality $h > l \ge 0$, and a set $M$ of $4m$ manufacturers, $m \ge 2$ of each type $(q_i,\xi_i) \in \{A,B\}\times\{h,l\}$. A consumer of horizontal type $t_k$ obtains utility $H$ from a good with $q_i = t_k$ and $L$ otherwise, plus the vertical utility $\xi_i$; here $0 \le L < H$, and $\Delta := H - L > 0$ measures horizontal differentiation. Consumers can always take an outside option $\varphi_k$, drawn from a continuous distribution $G$ supported on $[0,\infty)$. The high type vendor produces at cost $c_h(x) = \gamma x$, $\gamma > 0$; the low type vendor at a strictly increasing convex cost $c_l$ with $c_l(0)=0$ and strictly increasing derivative $c_l'$ (Assumption 1, items 1–2).

Manufacturer $i$ may join the blockchain at cost $\chi_i > 0$ ($a_i = 1$) or not ($a_i = 0$). Three scenarios are compared: full adoption $F$ (all adopt), partial adoption $P$ (exactly the high type manufacturers adopt) and non-adoption $N$. The paper's Proposition A.1 gives each scenario's equilibrium in closed form: every consumer's best manufacturer offers utility

$$u^F = u^P = H + h - \gamma,\qquad u^N = \tfrac{H+L+h+l}{2} - \gamma,$$

the low type vendor price is $\Psi^F_l = \max\{\gamma-(h-l),0\}$, $\Psi^P_l = \max\{\gamma-(h-l)-\frac{H-L}{2},0\}$, $\Psi^N_l = \gamma$ (the high type price is always $\gamma$), the low type market shares are $s^F_l = (c_l')^{-1}(\gamma-(h-l))$, $s^P_l = (c_l')^{-1}(\gamma-(h-l)-\frac{H-L}{2})$, $s^N_l = (c_l')^{-1}(\gamma)$, and $s^X_h = G(u^X) - s^X_l$. Manufacturers earn zero gross profit $\Pi$ in every scenario because of price competition.

Welfare in scenario $X$ is the sum $W^X = W^X_V + W^X_M + W^X_C$ of vendor welfare $W^X_V$ (revenue minus production cost of both vendors, (10)), manufacturer welfare $W^X_M = \sum_{i}(\Pi - \chi_i a^X_i)$ and consumer welfare $W^X_C = \mathbb E[\max\{u^X,\varphi\}]$ ((12)). The adoption game (8) lets each manufacturer choose $a_i$ to maximise $\Pi(a_i,a_{-i}) - \chi_i a_i$. An adoption failure is a situation in which full adoption raises total welfare, $W^F > W^N$, but is not an equilibrium of the adoption game.

Formalization targets

Goal: Proposition 4.8 (p. 19)

With $L$ fixed and $H = L + \Delta$,

$$\exists\,\underline\Delta\ \ \forall\,\Delta > \underline\Delta:\quad W^F(\Delta) > W^N(\Delta)\ \text{ and full adoption is not an equilibrium},$$

at every such $\Delta$ at which Assumption 1 holds. The threshold $\underline\Delta$ is left unspecified, as in the paper.

Milestones

• Proposition 4.1 (pp. 15–16): $W^F_C \ge W^P_C > W^N_C$.
• Proposition 4.3 (p. 17): $W^F_M < W^P_M < W^N_M$.
• Proposition 4.4 (p. 17): $W^F_V,\ W^P_V < W^N_V$.
• Proposition 4.6 (p. 18): $W^F, W^P > W^N$ for all sufficiently large $\Delta$; at fixed $\Delta$, $W^F < W^N$ once $\sum_{i\in M}\chi_i$ is large and $W^P < W^N$ once $\sum_{i:\xi_i=h}\chi_i$ is large.
• Proposition 4.7 (p. 19): neither full nor partial adoption is an equilibrium.

What the result gives

The proposition isolates a mechanism: blockchain information raises consumer surplus, which grows without bound in $\Delta$, while Bertrand competition prevents the manufacturers who pay for adoption from capturing any of it. The conclusion is a market failure that persists however valuable the information is, and it motivates the paper's transfer scheme (Proposition 4.9), in which a consumer access fee finances the adopters. The welfare comparisons of Propositions 4.1–4.6 are reusable on their own: they quantify who gains and who loses from information disclosure in a vertically and horizontally differentiated market.

The results are proved in the paper (App. A.2, pp. 33–36). None is machine-checked. This mission produces a checked version of the welfare comparisons and of the failure result in the reduced form described below; the proofs as printed use a density for $G$ and a second derivative of $c_l$, neither of which the model assumes, so a formal proof has to avoid both.

Where the difficulty lies

The equilibrium part is light once the gross profit is zero. The substance is in the welfare comparisons. Consumer welfare is an expectation $\mathbb E[\max\{u,\varphi\}]$ of an outside option with an arbitrary continuous law: strict monotonicity in $u$ needs positive mass of $\varphi$ below $u^N$, which is a consequence of Assumption 1 rather than an assumption, and the growth in $\Delta$ of $W^F - W^N$ has to be bounded below without a density. Vendor welfare involves the generalised inverse $(c_l')^{-1}$, which is $0$ below $c_l'(0)$: the comparison $W^F_V < W^N_V$ must handle the regime where the low type vendor's share collapses to zero and the regime where it is interior, and must obtain continuity of $c_l'$ from convexity rather than from a second derivative.

Formalization scope

The paper describes a signalling and pricing game but does not define its equilibrium concept precisely; Proposition A.1 states the outcomes and every proof in App. A.2 uses only those closed forms. The mission adopts the same reduced form, disclosed in every item: welfare is evaluated at Proposition A.1's prices, shares and utilities; the manufacturers' gross profit $\Pi$ is the constant $0$ for every adoption profile (the paper's statement in the proof of Proposition 4.3, p. 34); an equilibrium of the adoption stage is a pure Nash equilibrium of (8) with that payoff, expressed with AGT.IsPureNash from the published agt_games vocabulary. The signal accuracy is fixed at $\alpha = 1/2$, as in the paper's main text.

Conventions: manufacturers are Fin 2 × Bool × Fin m (the Boolean records $\xi_i = h$), adoption profiles are Boolean functions, $G$ is ProbabilityTheory.cdf μ for a probability measure $\mu$ on $\mathbb R$, $\Delta$ is an argument of every statement with $H = L + \Delta$, and $(c_l')^{-1}(x) = \sup\{s \ge 0 : c_l'(s) \le x\}$. The standing assumptions are bundled in Model.Standing: $m \ge 2$, $0 \le L$, $0 \le l < h$, $\gamma > 0$, $\chi_i > 0$, $\mu$ an atomless probability measure with $\mu((-\infty,0)) = 0$ and positive mass on every interval $(a,b) \subseteq [0,\infty)$, $c_l$ strictly increasing and convex on $[0,\infty)$ with $c_l(0) = 0$ and a strictly increasing derivative there. One hypothesis is added to the paper's: $\varphi$ has a finite mean, which the paper uses (its proof of Proposition 4.1 integrates $v\,p(v)$) without stating it. Assumption 1, item 3, depends on $\Delta$ through $H$ and is a hypothesis at each $\Delta$; it is satisfiable (for instance with $c_l(x) = x^2$, $\varphi \sim \mathrm{Exp}(1)$, $\gamma = 1/2$, $h=1$, $L=l=0$, $\Delta = 4$) and monotone in $\Delta$.

The formalization rules out the trivializing readings: the equilibrium predicate is concrete, not an abstract hypothesis; the integrals are of integrable functions, so no junk value $0$ enters; the inverse of $c_l'$ is the explicit supremum, not Function.invFun; and $L$, not $H$, is held fixed as $\Delta$ grows.

Needed infrastructure: expectations of $\max\{c,\varphi\}$ as a function of $c$ (monotonicity, growth), and the generalised inverse of a strictly increasing derivative of a convex function. Both are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the density and the second derivative of the printed proofs.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532
• N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Ch. 1 (pure Nash equilibrium). https://doi.org/10.1017/CBO9780511800481

Motivation

Many transactions are priced by negotiation rather than posted prices: business-to-business procurement, used cars, real estate, the purchase of a company. Before negotiating, a buyer can often spend effort finding out how much the object is actually worth to it, through inspections, trials, consultants or market research. That information serves two purposes. It improves the joint decision of whether to trade at all, and it changes how the surplus of trade is split. Liang Guo's Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360) studies how a buyer's endogenous information acquisition interacts with the two primitives of bargaining: the parties' bargaining powers and the seller's cost.

The first finding of the paper, Proposition 1, concerns how much information the buyer gathers. Its comparative statics in the seller's cost are non-monotone, and this non-monotonicity drives the later results of the paper, in which a seller can be worse off with more bargaining power or a lower cost. This mission formalizes Proposition 1 in its general form, for an arbitrary prior. A companion mission (Gathering Information before Negotiation II) formalizes the payoff reversals under a uniform prior and a linear information cost.

Setting

A seller can supply one unit of a product at cost $c$. A buyer's true value $u$ of the unit is unknown to both parties; the common prior law of $u$ is $F$, with a finite mean $\hat u>0$.

Before negotiating, the buyer acquires a truth-or-noise signal $w$: with probability $\alpha$ the signal equals $u$, and with probability $1-\alpha$ it is an independent draw from $F$. Because the parties are risk neutral, only the buyer's posterior mean

$$v\equiv\alpha w+(1-\alpha)\hat u$$

matters. Ex ante, $v$ has the distribution function

$$G(v,\alpha)\equiv F\!\left(\frac{v-(1-\alpha)\hat u}{\alpha}\right).$$

The buyer chooses the informativeness $\alpha$ in an interval $[\underline\alpha,\bar\alpha]\subseteq(0,1)$ at a cost $k(\alpha)$ that is increasing, with $k(\underline\alpha)=0$ and $k(\bar\alpha)>0$.

After observing $v$, the parties trade exactly when $v>c$ and split the net surplus $v-c$ according to their bargaining powers $\theta_s,\theta_b\in(0,1)$, $\theta_s+\theta_b=1$. Anticipating this, the buyer chooses $\alpha$ to solve

$$\max_{\alpha\in[\underline\alpha,\bar\alpha]}\ U_b(\alpha)=\theta_b\,A(\alpha,c)-k(\alpha),\qquad A(\alpha,c)=\int_c^{\bar v}(v-c)\,dG(v,\alpha),\tag{6}$$

where $A(\alpha,c)$ is the total ex ante surplus (7). A solution of (6) is written $\alpha^*$; in general there may be several, and $\mathcal A^*(\theta_b,c)$ denotes the set of all of them.

Two sets $S,T\subseteq\mathbb R$ are compared in the induced set order $S\sqsubseteq T$ when $\min(s,t)\in S$ and $\max(s,t)\in T$ for all $s\in S$, $t\in T$.

Formalization targets

Goal: Proposition 1 (p. 10)

Whenever the optimal sets compared are nonempty,

$$\theta_b\le\theta_b'\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b',c),$$ $$c\le c'\le\hat u\ \Longrightarrow\ \mathcal A^*(\theta_b,c)\sqsubseteq\mathcal A^*(\theta_b,c'),\qquad \hat u\le c\le c'\ \Longrightarrow\ \mathcal A^*(\theta_b,c')\sqsubseteq\mathcal A^*(\theta_b,c).$$

The buyer's optimal information acquisition increases with its bargaining power, and first increases and then decreases with the seller's cost, turning at the prior mean $\hat u$.

Milestones

1. Display (1), p. 7. $G(v,\alpha)$ is nondecreasing in $\alpha$ for $v<\hat u$ and nonincreasing for $v>\hat u$: the family rotates about $\hat u$.
2. Display (2) and footnote 7, p. 8. The mean of $v$ is $\hat u$ for every $\alpha$, and $\alpha\mapsto A(\alpha,c)$ is nondecreasing.
3. Proof of Proposition 1, p. 30. Integration by parts: $U_b(\alpha)=\theta_b\int_c^{\infty}[1-G(v,\alpha)]\,dv-k(\alpha)$.
4. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,\theta_b)$.
5. Proof of Proposition 1, p. 30. $U_b$ has increasing differences in $(\alpha,c)$ for $c\le\hat u$ and decreasing differences for $c\ge\hat u$.
6. Topkis's theorem (Topkis 1998, Theorem 2.8.1), already proved on the platform and referenced.

Significance

The result. The first part of Proposition 1 says that a buyer with more bargaining power gathers more information, because it captures a larger share of the surplus that information creates. The second part is the less expected one: a higher seller cost shrinks the gains from trade, yet it raises the buyer's incentive to become informed as long as the cost is below the prior mean $\hat u$, and lowers it only beyond. Information is most valuable when trade is a close call. The paper's later results (Corollary 1, Propositions 2 and 3) build on this: since information acquisition responds to $\theta_b$ and $c$, the seller's equilibrium payoff need not increase in its own bargaining power or decrease in its cost. The paper also notes (p. 11) that the monotonicity in $\theta_b$ needs only that a higher $\alpha$ is a mean-preserving spread, which is why the statement is posed here for every prior with finite mean.

Formalizing it. The proposition is proved in the paper, in a short appendix argument that differentiates under the integral and appeals to Topkis's theorem. To our knowledge it has not been machine-checked. The mission produces a density-free formalization: the rotation property and the mean-preserving-spread property of the truth-or-noise family, the integration-by-parts identity for the expected positive part, and the two increasing-differences statements, which together with the already formalized Topkis theorem give the goal.

Difficulty

The paper's argument is first-order: it computes cross-partial derivatives such as $\partial^2U_b/\partial c\,\partial\alpha=\theta_b\,\partial G(c,\alpha)/\partial\alpha$ and reads off their signs. Without a density these derivatives need not exist, and the information cost $k$ is assumed only increasing, so $U_b$ need not be differentiable, concave or even continuous in $\alpha$. The statements here are therefore in difference form, and the cross effects must be established as inequalities between integrals over different distributions of $v$.

The second obstacle is the shape of the comparative statics. Topkis's theorem gives a monotone optimal set in the induced set order on a parameter range where increasing differences hold, but the cost $c$ has increasing differences only on $(-\infty,\hat u]$ and decreasing differences on $[\hat u,\infty)$. The referenced platform theorem, by contrast, asks for increasing differences on the whole product of the decision and parameter spaces, so it does not apply to $U_b$ as it stands.

The obvious shortcut of picking a selection from the optimal set and proving it monotone does not work: the cross differences are only weakly positive (they vanish when $c$ lies outside the support of $v$), so the strict version of Topkis's theorem does not apply, and two different maximizers need not be ordered.

Formalization scope

The prior is a probability measure $\mu$ on $\mathbb R$ with integrable identity and positive mean $\hat u=\int w\,d\mu$. The paper's additional assumptions on $F$ (continuous and differentiable, strictly positive density on a bounded support $[\underline u,\bar u]$) and $c\in(\underline u,\bar u)$ are dropped: every statement is posed for all priors with finite mean and all real $c$, which implies the paper's case. $F$ is ProbabilityTheory.cdf μ, and $G$ is defined from it by the page's formula. The interval $[\underline\alpha,\bar\alpha]$ satisfies $0<\underline\alpha<\bar\alpha<1$; $k$ is monotone on it with $k(\underline\alpha)=0<k(\bar\alpha)$; $\theta_b\in(0,1)$ in every statement.

The total ex ante surplus is defined as $A(\alpha,c)=\int\max(\alpha w+(1-\alpha)\hat u-c,0)\,d\mu(w)$, which is (7) after the change of variables $v=\alpha w+(1-\alpha)\hat u$. The bargaining stage is not modelled; the paper's reduction to (6) is built into $U_b$. The optimal level $\alpha^*$ is the set of maximizers of $U_b$ over $[\underline\alpha,\bar\alpha]$ (optSet), never a chosen element. "Increases" is the induced set order, and every comparison assumes both optimal sets nonempty, which is the paper's presumption that (6) has a solution.

Trivializing formalizations are ruled out: $A$ is never given by a closed form or by the integration-by-parts expression (that identity is a milestone), $\alpha^*$ is never defined by a formula or a threshold rule, and the nonemptiness hypotheses prevent the induced set order from holding vacuously on an empty optimal set.

The development reuses the platform definitions Supermodularity.Lattices.InducedSetOrder and Supermodularity.Monotonicity.IncreasingDifferencesOn and the proved theorem Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences. The rotation and mean-preserving-spread lemmas for truth-or-noise signals, and the tail-integral identity $\mathbb E[(X-c)^+]=\int_c^\infty P(X>x)\,dx$ for integrable $X$, are reusable beyond this mission. Contributions of any of the milestones, of alternative proofs that avoid the integration by parts, and of the strict versions under the paper's density assumption are welcome.

Not posed in this mission: the benchmark (3)–(5), Corollary 1, Propositions 2–7, and the extensions of §4–§5.

Selected references

• L. Guo, Gathering Information before Negotiation, author's manuscript of 15 Feb 2022, SSRN 3930651. https://ssrn.com/abstract=3930651 ; published in Management Science (2022), https://doi.org/10.1287/mnsc.2022.4360
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• J. P. Johnson and D. P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 756–784, 2006. https://doi.org/10.1257/aer.96.3.756

Motivation

A mobile retail stall can travel toward its next customer while that customer walks toward the stall. The customer's walking allowance changes where the stall stops, so it also changes the location from which the next trip begins. A useful trip-length calculation therefore needs a distribution for successive meeting points, not just a rule for one meeting. Cao and Qi study this question in a service zone assigned to one stall and give a particular magnet rule whose rendezvous chain has a simple stationary law Cao and Qi, §3.3. The result supplies the location model used in their analysis of repositioning distances.

The rule matters because different choices of a meeting point can produce different chains even when each choice lets the customer walk the same maximum distance. The paper's Theorem 1 establishes a distributional property of the specified rule, for every admissible finite grid. Its proof is in Appendix B, pp. 46–49 of the cited SSRN manuscript.

Setting

The service zone is a square drawn as a diamond in ordinary horizontal and vertical coordinates. Its edge length is $R$ in Euclidean distance, while stall and customer travel is measured in Manhattan distance. For the chain, use the paper's two edge coordinates, aligned with the lower edges of the zone. The full customer grid is $G_k=\{0,\ldots,k\}^2$, so it contains $(k+1)^2$ points. A customer is uniform on this full grid.

Write $h=\phi k$, where $\phi=r/(\sqrt2R)$ and $r$ is the customer's maximum walking distance. The paper chooses $k$ so that $h$ is an integer and assumes $2h\le k$. The stall docks only at points of the inner diamond

$$\mathcal I_0=[h,k-h]^2\cap\mathbb Z^2.$$

The name “diamond” refers to its appearance in ordinary coordinates; in edge coordinates it is an axis-aligned square. A type-1 origin lies in $\mathcal I_1=[2h,k-2h]^2\cap\mathbb Z^2$. The other origins in $\mathcal I_0$ are type 2. The closed small diamond around an origin $z_o=(x_o,y_o)$ is $\mathcal I(z_o)=[x_o-h,x_o+h]\times[y_o-h,y_o+h]\cap\mathbb Z^2$.

The magnet rule maps the origin $z_o$ and next customer location $z_c$ to a rendezvous $z_d$. The stall stays at $z_o$ when $z_c\in\mathcal I(z_o)$. Otherwise, the location of $z_c$ in one of eight surrounding regions selects one of eight customer movement arrows. At a type-1 origin the head of that arrow is the rendezvous. At a type-2 origin the rule changes an arrow whose head would leave $\mathcal I_0$, keeping the rendezvous inside it while preserving the customer's allowed walking distance. These are Definitions 1 and 2 of the paper pp. 14–16.

For $z_o,z_d\in\mathcal I_0$, let $\mathcal A(z_o,z_d)$ be the customer grid locations sent from $z_o$ to $z_d$. The transition probability is

$$\mathbb P(z_o,z_d)=\frac{|\mathcal A(z_o,z_d)|}{(k+1)^2}.$$

Thus the denominator is the number of possible customers, not the number of stall locations. Repeated independent customer locations produce a finite Markov chain on $\mathcal I_0$.

Formalization targets

The goal is Theorem 1 p. 17. For every $k,h\in\mathbb N$ with $2h\le k$, its first part says that $\mathbb P$ is doubly stochastic:

$$\sum_{z_d\in\mathcal I_0}\mathbb P(z_o,z_d)=1 \quad\text{and}\quad \sum_{z_o\in\mathcal I_0}\mathbb P(z_o,z_d)=1.$$

Its second part says that the stationary distribution is uniform on $\mathcal I_0$. The formal target states existence and uniqueness: a probability vector $\pi$ is stationary for $\mathbb P$ if and only if $\pi(z)=1/|\mathcal I_0|$ for every state $z$.

The milestones follow the source's intermediate assertions: the rule keeps the rendezvous in $\mathcal I_0$ at the prescribed customer distance; each row counts $(k+1)^2$ customers; the type-1 self-transition counts $(2h+1)^2$ customers; type-1 and type-2 columns each count $(k+1)^2$ incoming customer events; and every transition entry is positive. The last assertion supports the uniqueness clause.

Significance

A uniform stationary law replaces an unknown, history-dependent location distribution with one specified directly by the inner diamond. In the paper, that distribution is the location input for later within-radius repositioning calculations Cao and Qi, §§3.2–3.3. The result is specific to the magnet rule. It does not say that every reasonable meeting rule has a uniform stationary law.

The paper proves the finite-grid theorem in Appendix B. This mission asks for a machine-checked account of its exact finite combinatorial statement. The development will provide reusable definitions of the grid rule and its transition counts, while using an existing formal library interface for finite Markov chains. The theorem statements are open proof targets; a successful local compilation of their statements alone is not a proof.

Difficulty

Unit row sums follow from assigning each customer location to one next rendezvous. Unit column sums are subtler: fixing a destination and varying the origin gives overlapping sets of customer locations. Interior destinations and boundary destinations have different counts because a type-2 origin can redirect an arrow that would otherwise leave the allowed stall region. The source treats these as Case I and Case II on pp. 46–49. An interior-only count cannot establish the theorem for all of $\mathcal I_0$, and positivity of every transition is a separate requirement for identifying the unique stationary law.

Formalization scope

Lean uses integer coordinate pairs for grid points and finite sets for $G_k$, $\mathcal I_0$, $\mathcal I_1$, and $\mathcal I(z_o)$. The region boundaries use the paper's strict or inclusive inequalities exactly. The permitted parameters are all natural numbers $k,h$ satisfying $2h\le k$, including $h=0$, $k=0$, and $2h=k$. In physical units $h=\phi k$; no division by $k$ occurs in the formal statements. When $k=0$, there is one customer point and one state.

The matrix is computed from the paper's two-part magnet rule and uniform demand on the full grid. Defining it as a uniform matrix, using a nearest-point rule, dropping the type-2 correction, fixing one grid size, or proving only column sums would miss the target. The definition of $\mathcal A$ counts customer locations that induce a transition. This includes customers already inside $\mathcal I(z_o)$ in a self-transition, as required by the paper's Case I(IX) and row-count formula. The paper's separate Proposition 2 is not a claim of this mission because it is false as printed; none of these targets assumes it. The finite-grid theorem does not formalize the subsequent informal $k\to\infty$ statement.

The complete development needs finite-set counting, integer interval bounds, real-valued stochastic matrices, and the stationary-distribution interface of the published MarkovChain definition. Contributions proving any of the stated counting milestones or strengthening the finite-chain consequences are welcome. The paper's own proof is in Appendix B, pp. 46–49.

Selected references

• J. Cao and W. Qi, Stall Economy: The Value of Mobility in Retail on Wheels, SSRN manuscript 3711896, 2022, §§3.2–3.3 and Appendix B, pp. 46–49. Manuscript.

Motivation

In inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.

The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.

Setting

Costs lie on the unit sphere $S^d$ of $\mathbb R^d$, $d=m+1\ge2$. In period $t$ nature presents a feasible set $\mathcal X_t\subseteq\mathbb R^n$, compact, nonempty and of diameter at most $1$, and a $1$-Lipschitz context $f_t:\mathbb R^n\to\mathbb R^d$. The forward problem with cost $c$ has solution set $\psi(c,\mathcal X_t,f_t)=\operatorname{argmin}_{x\in\mathcal X_t}f_t(x)'c$. The decision-maker plays some $x^\pi_t$, nature reveals an expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ for the true cost $c^\star$, and the regret over $T$ periods is

$$\mathcal R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star .$$

The knowledge set $C(\mathcal I_t)$ is the set of costs in the initial set $C_0\subseteq S^d$ under which every expert action seen so far was optimal.

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos(c'\hat c/\|c\|\|\hat c\|)$, and the uncertainty angle of a set $C$ is $\alpha(C)=\inf_{\hat c\in S^d}\sup_{c\in C}\theta(c,\hat c)$; a minimizing $\hat c$ is a circumcenter. The initial set is pointed when $\alpha(C_0)<\pi/2$.

For a positive diagonal $W=\operatorname{diag}(w_1,\dots,w_m)$ and an orthonormal $U$, the ellipsoidal cone is

$$E(W,U)=\{c:\ \tilde c_{[1]}\ge0,\ \tilde c_{[2:d]}'W^{-1}\tilde c_{[2:d]}\le\tilde c_{[1]}^2\},\qquad \tilde c=U^{-1}c ,$$

a cone with axis $Ue_1$ and elliptical cross-section. The effective difference of period $t$ is $\delta^\pi_t=(f_t(x^\pi_t)-f_t(x^\star_t))/\|f_t(x^\pi_t)-f_t(x^\star_t)\|$ (and $0$ if the difference vanishes).

EllipsoidalCones with parameter $\epsilon$ starts from the circular cone $W_1=\tan^2\alpha(C_0)I$, $U_1e_1$ a circumcenter of $C_0$, and plays the axis $U_te_1$ as proxy cost. With $\bar\delta=U_t^{-1}\delta^\pi_t$ it keeps the cone if

$$\bar\delta_{[2:d]}'W_t\bar\delta_{[2:d]}\le\epsilon^2 \qquad (12)$$

and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.

Formalization targets

Goal: Theorem 3 (p. 20)

With $\epsilon=d/T$ there is an absolute constant $K$ such that for every $d\ge2$, $T\ge1$, closed pointed $C_0$ with $\alpha(C_0)>0$, $c^\star\in C_0$, admissible instances and run,

$$\mathcal R^\pi_T\le K\,d^2\ln\big(T\tan\alpha(C_0)\big)\ \text{ if }\alpha(C_0)>\arctan(d/T),\qquad \mathcal R^\pi_T\le K\,d\ \text{ otherwise.}$$

The constant is left unfixed: the shape $d^2\ln(T\tan\alpha(C_0))$ is the claim, and the proof's explicit constant rests on a step that fails at $d=2$.

Milestones

1. Proposition 1: $\alpha(E(W,U))=\arctan\sqrt{\lambda_{\max}(W)}$.
2. Lemma 4: if $C(\mathcal I_t)\subseteq E(W_t,U_t)$ and (12) holds, the period's regret is at most $\epsilon$.
3. Lemma B-1 ($\eta=0$): ConeUpdate's output contains $E(W,U)\cap\{\delta'c\ge0\}$ and $\prod\lambda_i$ shrinks by $e^{-1/(2(d-1))}$.
4. Lemma 3: $C(\mathcal I_{t+1})\subseteq E(W_t,U_t)\cap\{\delta^{\pi\prime}_tc\ge0\}\subseteq E(W_{t+1},U_{t+1})$, and for $d\ge3$ $\prod\lambda_i$ shrinks by $e^{-1/(d-1)}$.
5. Cohen et al. (2020), Lemmas 3 and 4 (already posed on the platform, referenced): an ellipsoid-method step shrinks the smallest eigenvalue by at most $(d-1)^2/d^2$, and does not shrink it at all below the threshold $(\epsilon/(10(d-1)))^2$ when the cut is long.
6. Lemma 5: for $d\ge3$, $\lambda_{\max}(W_t)\le(10d/\epsilon)^{2(d-2)}\lambda_{\max}(W_1)^{d-1}e^{-I^\pi_t/(d-1)}$, or no update ever happens.

Significance

The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.

The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction $d\ge3$ for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the $\eta=0$ case of Lemma B-1.

Difficulty

Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.

Formalization scope

Costs live in EuclideanSpace ℝ (Fin (m+1)) with $d=m+1$, actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. $W$ is stored as its diagonal $w$, $U$ as a real orthogonal matrix, and $U^{-1}$ is written $U^\top$. Lean periods are $0$-based: Lean period $t$ is the paper's period $t+1$. This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.

Standing assumptions carried by the statements: $d\ge2$, $n\ge1$, feasible sets nonempty, compact and of diameter at most $1$, contexts $1$-Lipschitz, $C_0$ a closed subset of $S^d$, $\epsilon>0$. Pinned and disclosed choices:

• ConeUpdate is a relation, not a function. The printed $U^{-1}B\delta_{[2:p]}$ is read as $(U^{-1}\delta)_{[2:p]}$. The first column of $V$ is the eigenvector of the positive eigenvalue of $M$ with positive first entry, and larger $|\mu|$ is paired with larger eigenvalues of $N$. The page leaves this order open, and Algorithm 1 and Lemma B-1 disagree on it.
• The printed "$U_1\leftarrow I_{d-1}$" is read as: $U_1$ orthonormal with a circumcenter of $C_0$ as its first column.
• $\alpha(C_0)>0$ on the goal. At $\alpha(C_0)=0$ the algorithm's $W_1=0$ is not positive definite.
• The rate of Lemma 3 and the first part of Lemma 5 are stated for $d\ge3$ only; the rest of both lemmas for every $d\ge2$. At $d=2$ ConeUpdate halves $W$, and $1/2>e^{-1}$.
• Lemma B-1 is stated only for $\eta=0$. Its $\eta>0$ inclusion is false as printed.
• The worst-case regret is stated as a bound for every true cost, every adaptive instance sequence and every run, not as a real supremum. The polynomial running-time claim is not formalized.

The run predicate is satisfiable: a circumcenter of a closed nonempty $C_0$ exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of $\bar\delta$ is nonzero. A formalization in which no run exists, or in which $K$ may depend on $d$ or $T$, does not state Theorem 3.

A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015
• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, 2nd ed., Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8.

Interoperability and dominant platforms

Digital markets with strong network effects (messaging, social networks, app stores) tend to concentrate: a platform with more users is worth more to each user. Interoperability, the ability of a platform's users to interact with the users of rival platforms, is a central remedy in current competition policy; the EU Digital Markets Act (2022) mandates it for messaging services offered by designated gatekeepers. Whether interoperability actually reduces the market share of a dominant platform is a question about equilibria of a pricing game.

Ekmekci, White and Wu (Management Science, 2025) answer it in a model of platform competition built on net fees. Their Proposition 6 shows, for a Logit duopoly, that lowering interoperability always admits an equilibrium with an even larger dominant platform; equivalently, interoperability may mitigate dominance. This mission formalizes that result and the steps of its proof.

Setting

There are two platforms $j\in\{1,2\}$ and one side of users. Platform $j$ chooses a net fee $t^j\in\mathbb R$: the price a user pays, net of the interaction value the platform extracts once the user has joined. With Logit demand and no outside option, platform $j$'s market share at the fee profile $t=(t^1,t^2)$ is

$$n^j(t)=\frac{e^{-t^j}}{e^{-t^1}+e^{-t^2}} .$$

Both platforms have marginal cost $c$, and each user values each other user of the same platform at $\gamma$, the network externality. The degree of interoperability $\lambda\in[0,1]$ lets a user of platform $j$ also enjoy $\lambda\gamma$ per user of the rival platform (the paper's (19)), and the platform extracts this value too. Platform $j$'s profit is

$$\pi^j(t)=\bigl(t^j+\gamma n^j+\lambda\gamma n^{-j}-c\bigr)\,n^j,\qquad n^{-j}=1-n^j .$$

A fee profile $t$ is a Nash equilibrium in net fees under $\lambda$ if no platform can raise its profit by changing its own fee to any other real number. In an equilibrium with $n^j(t)>1/2$, platform $j$ is the dominant platform.

The Lean development (namespace NetFeePlatform.InteropDominance) writes $n^j(t)$ as demand 0 t j (the 0 is the weight of the absent outside option), $\pi^j$ as profit 0 c γ lam t j, and equilibrium as IsEquilibrium 0 c γ lam t, with t : Fin 2 → ℝ.

Formalization targets

Goal: Proposition 6 (p. 23)

Let $\gamma>0$, $0\le\underline\lambda<\overline\lambda\le1$ and $\gamma(1-\underline\lambda)\le 27/8$. If $t$ is an equilibrium under $\overline\lambda$ and $n^j(t)>1/2$, then there is an equilibrium $t'$ under $\underline\lambda$ with

$$n^j(t')>n^j(t).$$

The equilibrium $t'$ is not unique in general, and the statement does not say which one; it asserts existence, exactly as the paper does.

Milestones

1. Logit derivative (p. 13): $\partial n^j/\partial t^j=-n^j(1-n^j)$.
2. First-order condition (20) (p. 23): every equilibrium satisfies $t^j=c+\frac1{1-n^j}-2\gamma n^j-\gamma\lambda(1-n^j)+\gamma\lambda n^j$.
3. Sufficiency (Appendix E.1.3 with (36)): if $\gamma(1-\lambda)\le 27/8$, a fee satisfying (20) is a best response.
4. Equivalence (p. 24): the market $(c,\gamma,\lambda)$ has the equilibria of the market $(c-\gamma\lambda,\ \gamma(1-\lambda),\ 0)$.
5. Characterization (p. 51): equilibrium shares are the zeros of $\zeta(n;\lambda)=\ln\frac{n}{1-n}+\frac1{1-n}-\frac1n-2\gamma(1-\lambda)(2n-1)$, and conversely under the bound of item 3.
6. Comparison (p. 52): $\zeta(n;\underline\lambda)-\zeta(n;\overline\lambda)=2\gamma(\underline\lambda-\overline\lambda)(2n-1)<0$ for $n>1/2$.
7. Boundary behaviour (p. 52): $\zeta(n;\lambda)\to\infty$ as $n\to1^-$.

Significance

The result. Proposition 6 is the paper's argument that interoperability mandates can reduce concentration without any change in the platforms' cost or quality: at a fixed network externality, every equilibrium with a dominant platform under a higher degree of interoperability is outsized by an equilibrium under a lower degree, so the largest dominant share an equilibrium can sustain does not increase as interoperability rises. The proof rests on the equivalence of item 4, under which interoperability acts as a reduction of the effective network externality from $\gamma$ to $\gamma(1-\lambda)$; Figure 2 of the paper plots the resulting largest equilibrium share as $\lambda$ varies at $\gamma=3.375$.

Formalizing it. The paper's proof is three paragraphs, and it identifies equilibria with zeros of $\zeta$. A formal proof has to supply what the text takes for granted: that the first-order condition is necessary at a global Nash equilibrium, that it is sufficient in the stated range, and that a zero of $\zeta$ can be turned back into a fee profile. No part of the result has been machine-checked before. A complete development also gives a reusable treatment of Logit demand and of best responses in one-variable concave games.

Difficulty

The algebra of $\zeta$ and the intermediate value step are short. The work lies in the equilibrium notion. A Nash equilibrium is a global condition over every unilateral deviation $s\in\mathbb R$, and profit is not concave in the platform's own fee. Measured against the platform's own share $n\in(0,1)$, profit has second derivative $-1/(n(1-n)^2)+2\gamma(1-\lambda)$; it is concave exactly when $2\gamma(1-\lambda)$ does not exceed the minimum $27/4$ of $1/(n(1-n)^2)$. Outside that range the first-order condition is not sufficient, and a zero of $\zeta$ need not be an equilibrium; the paper does not treat that case.

Formalization scope

• Model. One side ($S=1$), two platforms indexed by Fin 2, Logit demand with no outside option (outside weight $w=0$, literally), common $c$ and $\gamma$, interoperability $\lambda$ written lam. The Setting file states the general $J$-platform objects (demand with an outside-option weight $w\ge0$, profit with the interoperability term $\lambda\gamma\sum_{k\ne j}n^k$, equilibrium, the diversion ratio of (32)); this mission uses them at $J=2$, $w=0$.
• Hypotheses. The paper assumes $\gamma>0$ and $\lambda\in[0,1]$. The goal adds $\gamma(1-\underline\lambda)\le 27/8$, the range in which the paper proves that the first-order condition is sufficient (Appendix E.1.3 with (36), the $3.375$ of Proposition 2′); the paper's own proof stops at the first-order condition and is not complete without it.
• Correction. The paper prints $\zeta(\overline n^1;\underline\lambda)-\zeta(\overline n^1;\overline\lambda)=4(\underline\lambda-\overline\lambda)\gamma\overline n^1$; the correct value is $2\gamma(\underline\lambda-\overline\lambda)(2\overline n^1-1)$. Its sign is the same, and milestone 6 states the correct value.
• Ruled out. Equilibrium is never replaced by "the pricing formula (20) holds": that would reduce the goal to an intermediate value argument and remove its substance. Shares are always demand 0 t j at a fee profile, never free variables. Profit keeps the interoperability term; without it $\lambda$ would not enter the model at all.
• Out of scope. General (non-Logit) demand and Assumptions A1–A2, $S\ge2$ sides, $J\ge3$ platforms (Proposition 12), platform-specific $c^j,\gamma^j$, the microfoundation of Appendix A, and the numerical Figure 2.
• Welcome contributions. Proofs of the milestones, in particular the Logit change of variable from fees to shares and the concavity bound, which are reusable in the two companion missions of this series.

Selected references

• M. Ekmekci, A. White, L. Wu, Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025; accepted working-paper version of December 12, 2024 (the version cited here). https://doi.org/10.1287/mnsc.2023.02810
• J. Crémer, P. Rey, J. Tirole, Connectivity in the Commercial Internet, Journal of Industrial Economics 48(4), 2000. https://doi.org/10.1111/1467-6451.00129
• Regulation (EU) 2022/1925 (Digital Markets Act), Official Journal of the European Union L 265, 2022. https://eur-lex.europa.eu/eli/reg/2022/1925/oj