Optimization

Motivation

Minimum hourly earnings rules for ride-hailing drivers are meant to protect income during periods when drivers spend part of their time idle. A platform pays a wage per hour carrying riders, yet drivers care about earnings per hour logged onto the platform. When many drivers enter after a wage increase, utilization can fall and offset the increase. A regulation that uses the preceding period's utilization to set the next wage can therefore create feedback in the marketplace. Asadpour, Lobel, and van Ryzin model this feedback and identify the exact minimum earnings targets compatible with bounded wages and continuing service (Asadpour, Lobel, and van Ryzin, 2022, §§3–4).

The question matters to marketplace design because a target that cannot be sustained within the model cannot be reached through a bounded wage policy, even if the platform changes prices over time. The theorem separates two economic regimes. When labor supply is tight, the decisive number is the price where demand equals supply. When supply is loose, the decisive number is the greatest revenue the platform can obtain from riders, converted into affordable driver earnings. This mission concerns the paper's threshold theorem and the four lemmas that state its main analytic ingredients.

Setting

In each discrete period $t$, a platform chooses a rider price $p_t\ge0$ and a wage per ride hour $w_t\ge0$. At price $p$, riders demand $D(p)$ hours of trips. At expected hourly earnings $z$, drivers supply $S(z)$ hours. The quantity of completed rides and driver utilization are

$$Q(p,z)=\min\{D(p),S(z)\},\qquad u(p,z)=\frac{Q(p,z)}{S(z)}.$$

Drivers earn wages only while carrying riders. Thus an earnings equilibrium is a positive sequence $z_t$ satisfying $z_t=w_tu(p_t,z_t)$ in every period. The platform's period profit is $\pi(p,w,z)=(p-w)Q(p,z)$. A minimum earnings target $M>0$ requires

$$w_{t+1}\ge\frac{M}{u(p_t,z_t)}.$$

The rule uses utilization in one period to set a wage floor in the next. A policy is stable if its prices and wages are feasible, it satisfies equilibrium and the wage rule, wages have a finite upper bound across all periods, and profit is nonnegative in all but finitely many periods. This definition permits a finite transition with losses but excludes a wage sequence that grows without bound (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Definitions 1–2 and (5)).

The revenue function is $R(p)=pD(p)$, and the labor cost function is $C(z)=zS(z)$. Write $H$ for the inverse of $C$ on positive expenditure. The paper assumes that $D$ is positive, continuous, and strictly decreasing; $S$ is strictly increasing, differentiable, and positive except possibly at zero; $R$ has a unique peak at $p^*$; and demand and supply cross at $w^*$, so $D(w^*)=S(w^*)$ (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Regularity assumptions).

Each theorem in this mission retains these standing assumptions, including when a particular result uses only some of them.

Formalization targets

Exact stability threshold

The goal is Theorem 1 of the paper. For every $M>0$, stability is characterized by

$$\operatorname{Stable}(D,S,M)\quad\Longleftrightarrow\quad M\le z^*,\qquad z^*=\begin{cases}w^*,&p^*\le w^*,\\H(R(p^*)),&p^*>w^*.\end{cases}$$

The equality case $p^*=w^*$ belongs to the first branch. The theorem gives an if and only if statement about all feasible sequences of prices and wages, rather than a condition for one chosen stationary policy (Asadpour, Lobel, and van Ryzin, 2022, p. 11, Theorem 1 and (7)).

Supporting results

The milestones reproduce Lemmas 1–4 and two claims in the Online Appendix. Lemma 1 establishes the inverse labor cost's existence, regularity, and monotonicity. Lemma 2 identifies continuous, unique equilibrium earnings for a given price and positive wage. Lemma 3 states that stability admits a policy with price equal to wage. Lemma 4 rewrites the wage rule in that regime. The appendix claims compare the loose-supply threshold with $w^*$ and show that the tight-supply wage-growth factor exceeds one above $w^*$ (Asadpour, Lobel, and van Ryzin, 2022, pp. 9–10 and Online Appendix p. 4).

Significance

The theorem identifies the full stable range of targets in this model. In the tight-supply case, raising the target above the demand–supply crossing cannot be stabilized by choosing a different sequence of prices. In the loose-supply case, the highest stable target is tied to the cost of supplying drivers at the platform's peak potential revenue. The distinction explains why the same regulation can have different limits across markets with different demand and supply curves (Asadpour, Lobel, and van Ryzin, 2022, p. 11 and Figure 2).

The paper proves this result mathematically. The remaining formalization task is to represent its sequence model and analytic assumptions in Lean and prove the threshold statement and its supporting lemmas there. Its inverse-cost, equilibrium, and policy-stability interfaces can also be reused for the companion results on utilization shocks and static stability in the same paper. Those companion theorems are separate missions in this series.

Difficulty

The short threshold formula hides two distinct obligations: a policy must satisfy the earnings equilibrium and lagged wage rule at every period, while the impossibility direction must exclude every stable feasible policy, including policies that vary prices over time. The equilibrium earnings formula changes regime when supply at the posted wage crosses demand. At the boundary the two formulas must agree, and the argument must still handle wages that approach or cross the demand–supply point. Boundedness and profit conditions also interact with a finite initial period in which profit may be negative.

The paper's printed explanation for one strict inequality in the tight-supply converse is insufficient: two decreasing factors do not determine the direction of their product. The formal target keeps the inequality the paper uses, while the appendix quotation remains as printed (Asadpour, Lobel, and van Ryzin, 2022, Online Appendix p. 4).

Formalization scope

Prices, wages, earnings, demand, supply, cost, and revenue are real valued. The curves' regularity is imposed on $[0,\infty)$; differentiability of supply is imposed on $(0,\infty)$ together with continuity at zero. Revenue is strictly increasing up to $p^*$ and strictly decreasing afterward, encoding the unique peak. The crossing $w^*$ and inverse $H$ are parameters with their characterizing properties, so the statements hold for their uniquely determined values. The inverse is only used at positive costs.

Lean indexes the first period by $0$, so its rule applies to $w_{t+1}$ for every $t\ge0$ and places no floor on $w_0$. The paper starts at period $1$ and likewise leaves the first wage free. “Bounded wages” means a single real upper bound for every period; “all but finitely many periods” is represented by an eventually true condition on $\mathbb N$.

An equilibrium requires $z_t>0$. This explicit domain condition prevents a zero-supply input from making $u=0/0$ and then $M/u=0$ under Lean's total real division, which would make the regulation vacuous. Lemma 2 correspondingly uses $w>0$. Its branch condition $S(w)<D(p)$ agrees with the paper's $w<S^{-1}(D(p))$ wherever that inverse exists and remains meaningful when demand is outside the range of supply. These domain choices are stated with the items they affect. A complete development needs real-analysis facts about continuous strictly monotone functions and inverses, eventual properties of sequences, and elementary bounds on the utilization ratio. Contributions establishing these interfaces or the stated milestones are within scope.

Selected references

• Arash Asadpour, Ilan Lobel, and Garrett van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN preprint 3502607, version of August 24, 2022; published in Manufacturing & Service Operations Management, 2022. SSRN preprint. The local formalization uses the dated preprint's page and theorem numbering.

Why digital businesses choose how much data to keep and how well to guard it

Platforms that earn money from their users' activity make two linked decisions about the data that activity generates: how much of it to record and store, and how much to spend protecting what they store. Stored data lets a business tailor its services and sell data-driven products, but it also attracts adversaries (hackers, data brokers, unauthorized third parties) whose access harms users, who then use the service less. Fainmesser, Galeotti and Momot, Digital Privacy (Management Science 69(6), 2023, doi:10.1287/mnsc.2022.4513; author manuscript SSRN 3459274), build a tractable model of this trade-off and solve it in closed form. Their first main result, Theorem 1, gives the profit-maximizing data strategy explicitly and shows that a business whose revenue depends more on data both collects more and protects more. The result is the basis for the paper's policy analysis (data protection standards, Pigouvian taxes on stored data) and for its comparison with the social optimum, which is the subject of a companion mission.

Setting

A unit mass of identical users each choose an activity level $a \ge 0$. The business stores a fraction $\xi \in [0,1]$ of every user's activity and protects it at level $C \ge 0$, at cost $\psi C$. With average activity $\bar a$ and a mass $\omega$ of active adversaries, a user's utility is (display (1))

$$U(a, \bar a) = a - \tfrac12 a^2 + \beta a\bar a + (\rho - \omega) a\xi ,$$

where $\beta \in [0,1)$ measures network effects and $\rho \in [0,1)$ the users' benefit from tailored services built on stored data. Adversaries have access costs $\gamma C$ with $\gamma$ uniform on $[0, M]$ and gain $\bar a\xi$; letting $M \to \infty$, the mass of active adversaries is $\omega = \xi\bar a/C$. Proposition 1 shows that for every data strategy $(\xi, C)$ with $C > 0$ this users–adversaries subgame has a unique equilibrium,

$$\bar a^*(\xi, C) = \frac{C(1+\rho\xi)}{C(1-\beta)+\xi^2}, \qquad \omega^*(\xi, C) = \frac{\xi\bar a^*(\xi, C)}{C},$$

with consumer surplus $\mathrm{CS}(\xi, C) = \tfrac12\bar a^*(\xi, C)^2$; when nothing is stored, $\bar a^*(0, C) = 1/(1-\beta)$. The business's profit is (display (2))

$$\Pi(\xi, C) = (1-P)\,\bar a^*(\xi, C) + P\,\xi\bar a^*(\xi, C) - \psi C ,$$

where the revenue model $P \in [0,1]$ is the share of revenue that is data-driven: $P = 0$ is a purely usage-driven business, $P = 1$ a purely data-driven one. A business optimum is a strategy $(\xi, C) \in [0,1] \times [0,\infty)$ that maximizes $\Pi$ over $[0,1] \times [0,\infty)$.

The Lean development uses the same names: abar, omegaStar, CS, profit, Feasible, IsBusinessOpt, the best-response quantities Ch ($C_h$), kappa ($\kappa$), Cl ($C_l$), xiBR, the threshold psiL ($\psi_L$), the interior root xiI ($\xi_i$), and the closed forms xiStar ($\xi^\star$) and CStar ($C^\star$).

Formalization targets

Goal: Theorem 1

For fixed $0 \le \beta < 1$, $0 < \rho < 1$, $\psi > 0$ and every $P \in (0,1]$, let

$$\xi^\star = \max\Big\{0, \min\Big\{1, \frac{1}{2P\rho}\Big(-(1-P)\rho - P + |P-(1-P)\rho|\sqrt{\frac{\psi}{\max\{0,\psi-P\rho\}}}\Big)\Big\}\Big\},$$ $$C^\star = \frac{\xi^\star}{1-\beta}\Big(-\xi^\star + \sqrt{\tfrac1\psi(1+\rho\xi^\star)(1-P(1-\xi^\star))}\Big).$$

Then $(\xi^\star, C^\star)$ is a business optimum, and both $P \mapsto \xi^\star$ and $P \mapsto C^\star$ are weakly increasing on $(0,1]$.

Milestones

1. Proposition 1 (p. 10): the subgame equilibrium (3) is unique, and consumer surplus is (4).
2. Proposition 1 (a)–(b) with footnote 15: $\bar a^*$ and $\xi\bar a^*$ increase in $C$, and are single-peaked in $\xi$.
3. Lemma 1 (p. 29): for fixed $\xi$, the unique optimal protection is $\max\{C_h(\xi), 0\}$.
4. Lemma 2 (p. 29): for fixed $C > 0$, the unique optimal collection is $-\kappa(C) + \sqrt{\kappa(C)^2 + C(1-\beta)}$ if $C < C_l$ and $1$ if $C > C_l$.
5. App. A.2 summary (p. 31): with $P\rho \le \psi_L \le \psi_H$, the business optimum is $(1, C_h(1))$ for $\psi \le \psi_L$, $(\xi_i, C_h(\xi_i))$ with $\xi_i \in (0,1)$ for $\psi_L < \psi < \psi_H$, and $(0,0)$ for $\psi \ge \psi_H$.

Significance

Theorem 1 is the statement that a business's revenue model alone orders its data practices: holding users and costs fixed, moving toward data-driven revenue never lowers collection and never lowers protection. The paper uses it to explain why consumer surplus is maximized at an intermediate revenue model $P = \rho/(1+\rho)$ (Proposition 2), and as the benchmark against which it evaluates regulation in §6. The closed form also makes the regime structure explicit: no collection when protection is expensive, full collection when it is cheap, and an interior solution in between.

The result is proved in the paper (App. A.2–A.3, with the proofs of Lemmas 1–2 in Online App. B), but parts of that proof are informal: several steps are "easy to check" or "can be derived similarly", one case is treated and the other left to the reader, and the second-order conditions are referred to a general lemma in Online App. C.5. No machine-checked version exists. A formal proof certifies the closed form, including its boundary cases, which the printed formula handles through an infinite square root.

Difficulty

The profit is not jointly concave, so first-order conditions do not settle the problem. The argument intersects the two best responses (Lemmas 1–2), and two candidate strategies survive in the intermediate regime: $(0,0)$ and the interior point. Choosing between them requires comparing profits across all $\psi$ and showing the comparison flips exactly at $\psi_H$. Monotonicity in $P$ is harder still: as $P$ moves, so do both thresholds $\psi_L(P)$ and $\psi_H(P)$, so a fixed $\psi$ can cross from one regime to another, and $\xi^\star$ and $C^\star$ must be shown monotone within each regime and across the switches. Within the interior regime $C^\star = C_h(\xi^\star)$ depends on $P$ both directly and through $\xi^\star$, so differentiating the closed form does not by itself give the sign.

Formalization scope

All parameters are explicit real numbers; every optimum is taken over $\xi \in [0,1]$, $C \ge 0$, never over $\mathbb R^2$. The page's ranges are $0 \le \beta < 1$, $0 \le \rho < 1$, $\psi \ge 0$, $0 \le P \le 1$. The following are added and disclosed in each item: $\psi > 0$ everywhere (otherwise $C_h$ and (6) divide by zero and no maximizer exists); $P > 0$ and $\rho > 0$ in Theorem 1 and the App. A.2 summary (formula (5) divides by $2P\rho$); $C > 0$ in Proposition 1 and Lemma 2 (the adversary mass $\xi\bar a/C$); $\rho > 0$ in Lemma 2.

Three conventions are fixed. First, $\bar a^*(0, C) = 1/(1-\beta)$ for every $C$, the paper's value at $(0,0)$ where (3) is $0/0$. Second, $\xi^\star = 1$ whenever $\psi \le P\rho$, the page's own reading of the infinite square root in (5). Third, $\psi \ge \psi_H$ is written as $(P+(1-P)\rho)^2 \le 4(1-P)\psi$, so that $\psi_H = +\infty$ at $P = 1$. Using Lean's $0/0 = 0$ at either of the first two places makes Theorem 1 false, not trivial, and is ruled out by these definitions. Theorem 1 asserts that $(\xi^\star, C^\star)$ is a maximizer: uniqueness fails at $P = \rho/(1+\rho)$, $\psi = \rho^2/(1+\rho)$. Monotonicity is MonotoneOn on $(0,1]$ with $\beta, \rho, \psi$ fixed; a Monotone statement with junk values outside $(0,1]$ would not be the paper's claim.

A complete development needs only real analysis from Mathlib: one-variable calculus for the best responses, square-root and absolute-value manipulations for the closed form, and a profit comparison across regimes. The best-response lemmas are reusable for the companion mission on the social optimum. Contributions of proofs of any milestone, and of auxiliary lemmas such as $C^\star = C_h(\xi^\star)$, are welcome.

Selected references

• I. P. Fainmesser, A. Galeotti, R. Momot, Digital Privacy, Management Science 69(6):3157–3173, 2023. doi:10.1287/mnsc.2022.4513; author manuscript (This Draft: April 2022), SSRN 3459274.
• E. L. Glaeser, J. A. Scheinkman, Non-Market Interactions, NBER Working Paper 8053, 2000 (existence and uniqueness of the users' response, used in App. A.1). doi:10.3386/w8053

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

split capacities into scarce, moderate and ample zones.

Formalization targets

Goal: Corollary 1

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Machines in production lines deteriorate in ways that are only partly visible. A machine may run in a degraded state that raises costs without announcing itself, and eventually fail in a way that cannot be missed. The decision maker must choose between continuing production, paying for an inspection that reveals the hidden state, and replacing the machine preventively. Models of this kind are partially observable Markov decision processes (POMDPs), and for POMDPs closed-form optimal policies are rare: the value function lives on the space of beliefs and is usually only computed numerically.

H. Zhang and W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures (Management Science, 2022; read here as SSRN 2945049, version of 2022-08-21), solve the classical two-state version of this problem completely. Working in the dual "efficient frontier" framework of Zhang (2010), they show that the optimal solution has exactly six possible structures and give each in closed form, with explicit or implicitly characterized thresholds on the replacement and inspection costs.

Setting

A machine is in a hidden state $x\in\{0,1\}$ (good or bad) or in the observable failure state $F$. Each period, if the machine has failed it is replaced correctively at cost $c^F$; otherwise one of three actions is chosen:

• production $P$ costs $0$ in state 0 and $c^P$ in state 1;
• inspection $I$ costs $c^I$ and reveals the current state;
• preventive replacement $R$ costs $c^R$ and resets the machine to state 0.

Production always takes place. From state 0 the machine moves to state 1 with probability $\gamma_0$; from state 1 it fails with probability $\gamma_1$. Write $\bar\gamma_x=1-\gamma_x$, $\mathbf p_0=(\bar\gamma_0,\gamma_0)'$, $\mathbf p_1=(0,\bar\gamma_1)'$, $\mathbf g^P(u_F)=(0,c^P+\beta\gamma_1u_F)'$, $\mathbf g^I(u_F)=(c^I,c^I+\beta\gamma_1u_F)'$ and $\mathbf P^P\mathbf u=(\mathbf p_0'\mathbf u,\mathbf p_1'\mathbf u)'$. Costs are discounted by $\beta$ over an infinite horizon.

A continuation-cost vector $\mathbf u=(u_0,u_1)'$ records the cost of a continuation policy from each hidden state, and $u_F$ the cost after a failure. The expected optimal cost at an (unnormalized) belief $\boldsymbol\pi=(\pi_0,\pi_1)'\ge0$ is $V(\boldsymbol\pi)=\min_{\mathbf u\in U^*}\boldsymbol\pi'\mathbf u$, where $U^*$ is the set of extreme points of the efficient frontier. The pair $(U^*,u^*_F)$ is the fixed point of the dual value iteration (12)–(16). In support-function form, a pair $(W,w_F)$ is mapped to

$$W'(\boldsymbol\pi)=\min\Big\{\boldsymbol\pi'\mathbf g^P(w_F)+\beta W\big((\mathbf P^P)'\boldsymbol\pi\big),\ (\pi_0+\pi_1)\big(c^R+\beta W(\mathbf p_0)\big),\ \boldsymbol\pi'\mathbf g^I(w_F)+\beta\big(\pi_0W(\mathbf p_0)+\pi_1W(\mathbf p_1)\big)\Big\},$$ $$w_F'=c^F+\beta W(\mathbf p_0),$$

the three terms being $P$, $R$ and $I$. A finite set $U$ with a number $u_F$ is the optimal solution for an action set if value iteration from zero terminal costs converges to $\min_{\mathbf u\in U}\boldsymbol\pi'\mathbf u$ for every $\boldsymbol\pi\ge0$ and to $u_F$ after a failure.

The structures are built from two point sequences. The production sequence is $\mathbf u_{i+1}=\mathbf g^P(u_F)+\beta\mathbf P^P\mathbf u_i$. Started on the diagonal at $(u^R,u^R)'$ with $u_F=u^R+c^F-c^R$, the self-consistency equation $u^R=c^R+\beta\mathbf p_0'\mathbf u_m$ has a unique solution $u^R=f(m)$ (31). Started instead at the inspection point (35), it gives $g(m)$ (40).

Formalization targets

Goal: Theorem 2 (pp. 27–28, Table 1)

Let $\theta=\dfrac{c^P+\beta\gamma_1c^F}{1-\beta+\beta(\gamma_0+\gamma_1)}$ and $\hat c=(1+\beta\gamma_0)c^P-\beta\bar\gamma_1(1-\beta+\beta\gamma_0+\beta\gamma_1)c^R+\beta^2\gamma_1\bar\gamma_1c^F$. Under $\{P,I,R\}$:

$$c^R\ge\theta\ \Rightarrow\ [P];\qquad \tfrac{\gamma_0}{\gamma_1}\theta\le c^R<\theta\ \Rightarrow\ R[P],\ IR[P]\ \text{or}\ [PIR]\ \text{by explicit thresholds on }c^I;$$ $$c^R<\min\{\tfrac{\gamma_0}{\gamma_1}\theta,\theta\}\ \Rightarrow\ \exists\,0<\hat c_1\le\hat c_2<c^R:\ [PR],\ I[PR]\ \text{or}\ [PIR]\ \text{as}\ c^I\ge\hat c_2,\ \hat c_1\le c^I<\hat c_2,\ c^I<\hat c_1,$$

with every structure an explicit pair $(U^*,u^*_F)$ from Table 1, and the thresholds characterized implicitly ($\mathbf u^{I\dagger}$ on the frontier of $U^\dagger$ at $c^I=\hat c_2$; $\min f=\min g$ at $c^I=\hat c_1$).

Milestones

Proposition 2 (the fixed-point equations), Proposition 3 (the cost of producing forever), Lemma 1 and Lemma 6 (the two sequences in closed form), Lemma 3 and Lemma 7 (the anchors $f$ and $g$), Proposition 4 (unimodality of $f$), Theorem 1 (the two-action solution: $[P]$, $R[P]$, $[PR]$, with extreme-point exactness) and Lemma 5 (when inspection enters).

Significance

The result. The theorem turns a POMDP into a finite list of explicit policies. Each structure is a periodic plan that needs no belief updating: produce for $m^\dagger$ periods and replace; or inspect every $m^*$ periods and replace only if the machine is found bad. The thresholds tell when inspection is worth its cost, and the comparative statics of $m^\dagger$ and $m^*$ follow from the closed forms. The authors use the solution to justify common maintenance practices.

Formalizing it. The result is proved in the paper (main text §4, proofs in its e-companion, App. A); no part is machine-checked. The proofs of Theorems 1 and 2 argue geometrically from figures of convex curves in the plane ("the curve bends back", "all the points are still extreme points"). A formal development has to turn these into inequalities between piecewise-linear concave functions, and has to prove convergence of value iteration to the stated sets. The implicit thresholds of part (3) were not checked numerically when this mission was planned. Parts (1) and (2) and Theorem 1 were.

Difficulty

Verifying that a candidate set $U$ is a fixed point is not enough: the goal asserts that value iteration from zero converges to it, so uniqueness of the bounded fixed point must be proved (a contraction argument in the supremum norm over the simplex). More importantly, finding the frontier requires knowing which points of the infinite production sequence are extreme, which depends on the location of the anchor relative to the curve $\{\mathbf u_i:i\ge0\}$ (Fig. 5 of the paper, five subcases). The natural induction on $m$ fails because $f$ is not monotone: its least minimizer $m^\dagger$ must be located through the unimodality of the real extension (Proposition 4). In part (3) the thresholds $\hat c_1,\hat c_2$ are defined implicitly, and showing that the three regimes are ordered in $c^I$ requires monotonicity of the whole frontier in $c^I$.

Formalization scope

Everything is defined in the namespace MaintPOMDP.Frontier. Vectors and beliefs are Fin 2 → ℝ (index 0 = good state); beliefs are unnormalized, $\boldsymbol\pi\ge0$. The optimal solution is the limit of the support-function value iteration started from $W\equiv0$, $w_F=0$; "the structure is X" means that this limit equals $\min$ over the points of row X of Table 1, with the failure cost of that row.

Standing assumptions: $0<\beta<1$, $0<c^P<c^I<c^R<c^F$ (p. 14), and $0<\gamma_0<1$, $0<\gamma_1<1$, which the paper never states and which are added (the thresholds divide by $\gamma_1$). The hypothesis $\gamma_0\ne\gamma_1$ is added only to Lemmas 1, 3, 6, 7 and Proposition 4, whose printed formulas divide by $\gamma_1-\gamma_0$; $f$ and $g$ themselves are defined as solutions of the affine anchor equations, so Theorems 1 and 2 cover $\gamma_0=\gamma_1$. Proposition 4 also carries the range of $c^R$ that its proof uses. "$m^\dagger=\arg\min f$" is the least minimizer, and its existence is part of the conclusion. In Theorem 2, the indices $n_R,n_I$ of Table 1 are existential and extreme-point exactness is not asserted for the $I[PR]$ and $[PIR]$ rows (Table 1's $I[PR]$ row conflicts with the paper's Proposition 8). It is asserted in Theorem 1. In part (3) the thresholds are chosen before $c^I$ and the claims hold for every $c^I\in(c^P,c^R)$.

Trivializing readings are ruled out: the value function is the limit of the iterates, not an arbitrary fixed point or a junk limit; identities hold for every belief $\boldsymbol\pi\ge0$, not only at vertices; every frontier set is given by formulas, so no extra points can be slipped in; minimizers are asserted, not assumed; and thresholds involving $\gamma_0/\gamma_1$ are evaluated with $\gamma_1>0$.

A complete development needs convergence of value iteration for a monotone contraction on bounded functions over the cone $\boldsymbol\pi\ge0$, explicit solutions of two-dimensional linear recurrences, and lemmas on lower envelopes of finitely many linear functions in two variables. These are reusable beyond this mission, for other two-state POMDPs. Contributions of any milestone, of the γ0 = γ1 closed forms (App. B), or of a proof of Theorem 1 alone are welcome.

Selected references

• H. Zhang, W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4547 (read as SSRN 2945049, https://ssrn.com/abstract=2945049)
• H. Zhang, Partially Observable Markov Decision Processes: A Geometric Technique and Analysis, Operations Research 58(1), 2010. https://doi.org/10.1287/opre.1090.0697
• R. D. Smallwood, E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071
• S. M. Ross, Quality Control under Markovian Deterioration, Management Science 17(9), 1971. https://doi.org/10.1287/mnsc.17.9.587

Motivation

Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in $\mathbb R^n$ inside a box of radius $R$ that uses an expected $O(n\log(nR/\epsilon))$ oracle calls and $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time, improving on the $O(n^{\omega+1}\log(nR/\epsilon))$ additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.

The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing $\vec 0$ game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in $\mathbb R^m$ that is partially reset at every step.

Setting

Fix a dimension $m\ge1$ and constants $c>0$, $R>0$. For $\vec v\in\mathbb R^m$, $\|\vec v\|_\infty=\max_i|v_i|$ and $\|\vec v\|_2=(\sum_iv_i^2)^{1/2}$.

A point starts at $\vec x^{(1)}=\vec 0$. Each round $k=1,2,\dots$ runs as follows (Algorithm 4).

1. A stochastic adversary chooses a probability distribution $\mathcal D^{(k)}$ on $\mathbb R^m$ with mean $\vec 0$ and $\|\vec\Delta\|_2\le c$ for every $\vec\Delta$ in its support.
2. The adversary chooses an observation $\vec y^{(k)}$ with $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$.
3. The player chooses a coordinate $i^{(k)}$, knowing only $\vec y^{(k)}$: neither $\vec x^{(k)}$, nor $\mathcal D^{(k)}$, nor the step.
4. A step $\vec\Delta^{(k)}$ is drawn from $\mathcal D^{(k)}$ and the point moves to

$$x^{(k+1)}_{i^{(k)}}=0,\qquad x^{(k+1)}_j=x^{(k)}_j+\Delta^{(k)}_j\quad(j\ne i^{(k)}).$$

The adversary may use everything that has happened so far to make its choices. The player wants to keep $\vec x^{(k)}$ near $\vec 0$ in $\|\cdot\|_\infty$; the adversary wants to push it away. The largest-coordinate strategy is $i^{(k)}=\operatorname{argmax}_i|y^{(k)}_i|$: reset the coordinate that looks largest.

Formalization targets

Goal: Theorem 34

If the player uses the largest-coordinate strategy, then for every $p\in(0,1]$, with probability at least $1-p$,

$$\|\vec x^{(k)}\|_\infty\le2(c+R)\log\big(4mk^2/p\big)\qquad\text{for all }k\ge1.$$

The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in $k$, in $m$ and in $1/p$.

Milestones

The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:

1. the exponential inequality $e^x\le1+x+\tfrac{x^2}{2}e^{|x|}$ and its consequence $e^{\alpha x+\alpha\delta}\le e^{\alpha x}+\alpha\delta e^{\alpha x}+\tfrac12\alpha^2\delta^2e^{\alpha x+|\alpha|c}$ for $|\delta|\le c$;
2. the one-step drift bound for the potential $\Phi(\vec x)=\sum_ie^{\alpha x_i}+\sum_ie^{-\alpha x_i}$:

$$\mathbb E_{\vec\Delta\sim\mathcal D}\,\Phi(\vec x+\vec\Delta)\le\Phi(\vec x)+\alpha^2e^{\alpha c}c^2\eta,\qquad\eta=\max\big(\max_ie^{\alpha x_i},\max_ie^{-\alpha x_i}\big);$$

3. the choice $\alpha=1/(2(c+R))$, for which $e^{2\alpha(c+R)}(\alpha(c+R))^2\le1$ and $\alpha^2e^{\alpha c}c^2\le e^{-\alpha(R+c)}$;
4. the union-bound arithmetic $1-\sum_{k\ge1}2m/\lambda_k=1-\sum_{k\ge1}p/(2k^2)\ge1-p$ for $\lambda_k=4mk^2/p$.

Significance

Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.

None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant $4$ inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in $\mathbb R^m$.

Difficulty

The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to $2R$ smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all $k$ at once, with only logarithmic dependence on $k$, has to control all coordinates jointly. Establishing such joint control, with the specific constant $4$ inside the logarithm, against the most adversarial interaction between the observation error $R$ and the step size $c$, is where the work lies.

Formalization scope

• Probability model. The randomness is a probability space $(\Omega,\mu)$ with a filtration $(\mathcal F_k)_{k\ge0}$. The adversary's adaptive choice of $\mathcal D^{(k)}$ is modelled by the conditional law of the step: each coordinate of the step has conditional mean $0$ given the past, the step is measurable with respect to the next $\sigma$-algebra, and $\sum_i\Delta_i^2\le c^2$ holds everywhere. The observation $\vec y^{(k)}$ is measurable with respect to the current $\sigma$-algebra, so it is fixed before the step is drawn, and $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ holds on the actual trajectory.
• Indexing. Coordinates are Fin m (0-based), with $m\ge1$. Lean round $k\in\mathbb N$ is the paper's round $k+1$, so the goal's bound reads $\log(4m(k+1)^2/p)$; at Lean round $0$ the point is $\vec 0$.
• Norms. $\|\cdot\|_\infty$ is Lean's sup norm on Fin m → ℝ. The step bound $\|\vec\Delta\|_2\le c$ is written as $\sum_i\Delta_i^2\le c^2$, never as a sup-norm bound. The paper's prose once writes $\|\vec\Delta\|_2^2\le c$; Algorithm 4 and the proof use $\|\vec\Delta\|_2\le c$, which is what is formalized.
• Tie rule. $\operatorname{argmax}_i|y_i|$ breaks ties by the least index; the paper's theorem is claimed for any tie rule.
• Constants. $c>0$, $R>0$ (Algorithm 4), $0<p\le1$, natural logarithm. The drift milestone adds $\alpha\ge0$.
• Not trivial by construction. The hypotheses are satisfiable by genuinely random adversaries (a fair-coin step of size $c$ is one), and the conclusion is a probability lower bound on an event, not a statement that holds vacuously; a formalization in which the observation could depend on the step, or in which the step bound were a sup-norm bound, would not be the paper's theorem.
• Out of scope. Running time, the leverage-score application (Section 7.1, Theorem 31) and the rest of the cutting plane method.
• Infrastructure. Conditional expectation with respect to a filtration, Markov's inequality and countable union bounds are in Mathlib. Supermartingale lemmas for nonnegative adapted processes, and the passage from a per-step drift inequality to a bound on the expected potential, are reusable well beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, FOCS 2015; arXiv:1508.04874v2, 2015. https://arxiv.org/abs/1508.04874
• P. M. Vaidya, A new algorithm for minimizing convex functions over convex sets, FOCS 1989; Mathematical Programming 73 (1996) 291–341. https://doi.org/10.1007/BF02592216

Motivation

Submodular function minimization (SFM) asks for a set $S \subseteq V$ minimizing a function $f : 2^V \to \mathbb Z$ with diminishing marginal returns. It contains minimum cut, matroid intersection and many problems of combinatorial optimization, and the question of how fast it can be solved with a value oracle has a long history: Grötschel, Lovász and Schrijver (1981) gave the first polynomial algorithm via the ellipsoid method; Iwata, Fleischer and Fujishige (2001) and Schrijver (2000) gave the first combinatorial strongly polynomial algorithms; Orlin (2009) brought the bound to $O(n^5 \cdot \mathrm{EO} + n^6)$.

Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) applied their faster cutting plane method to SFM and obtained an $\tilde O(n^3 \cdot \mathrm{EO} + n^4)$ strongly polynomial algorithm. Like several earlier strongly polynomial algorithms, theirs works over a ring family and repeatedly adds new valid arcs that shrink the family without losing a minimizer. The combinatorial core of that step is Lemma 79 (p. 84) and its mirror image Lemma 80 (p. 86), which the authors describe as new to their work. This mission formalizes Lemma 79 and the lemmas its proof uses.

Setting

Let $V = [n]$ and let $f : 2^V \to \mathbb Z$ be submodular (Definition 58): $f(T + i) - f(T) \le f(S + i) - f(S)$ whenever $S \subseteq T$ and $i \notin T$, where $S + i = S \cup \{i\}$. As in §13.1, $f(\emptyset) = 0$.

For $y \in \mathbb R^n$ write $y(S) = \sum_{i \in S} y_i$. The base polyhedron is

$$\mathcal B(f) = \{ y \in \mathbb R^n : y(S) \le f(S) \ \forall S \subseteq V,\ y(V) = f(V) \}.$$

Every permutation $v_1, \dots, v_n$ of $V$ defines a basic feasible solution (BFS) $h$ of $\mathcal B(f)$ by $h_{v_i} = f(\{v_1, \dots, v_i\}) - f(\{v_1, \dots, v_{i-1}\})$ (Theorem 62); $v_i$ precedes $v_j$ when $i < j$.

A set $A$ of arcs on $V$ (an acyclic digraph) represents the ring family $\mathcal F_A$ of sets $S$ such that $i \in S$ implies $j \in S$ for every arc $(i, j) \in A$. $R(i)$ and $Q(i)$ are the descendants and the ancestors of $i$, both including $i$. A permutation, or its BFS, is consistent with $A$ if for every arc $(i, j)$ the element $j$ precedes $i$ (Definition 74). A vector is non-degenerate if it has both a positive and a negative entry. Finally,

$$\mathrm{upper}(i) = f(R(i)) - f(R(i) - i), \qquad \mathrm{lower}(i) = f(V \setminus Q(i) + i) - f(V \setminus Q(i)).$$

An arc $(p, q)$ is valid if adding it keeps a minimizer of $f$ over $\mathcal F_A$.

Formalization targets

Goal: Lemma 79 (new arc)

Let $y = \sum_k \lambda^{(k)} y^{(k)}$ be a non-degenerate convex combination of BFS's consistent with $A$. If

$$\mathrm{upper}(p) > n^4 \max_j y_j,$$

then there is $q \notin R(p)$ such that every minimizer of $f$ over $\mathcal F_A$ that contains $p$ also contains $q$.

Milestones, in the order of the proof

1. Lemma 65 (p. 77): a non-negative $h \in \mathcal B(f)$ makes $\emptyset$ a minimizer; a non-positive one makes $V$ a minimizer.
2. (15.2) (p. 85): moving $R(p)$ to the front of a consistent permutation gives a BFS $y'$ with $y'_p = \mathrm{upper}(p)$, $y'_j \ge y_j$ on $R(p)$ and $y'_j \le y_j$ off $R(p)$.
3. The restriction claim (p. 85): $f'(S) = f(S \cup R(p))$ on $V \setminus R(p)$ is submodular, $S_{\min} \setminus R(p)$ minimizes it over the induced ring family, and $y'$ restricted to $V \setminus R(p)$ lies in its base polyhedron.
4. (15.3) (p. 85): $y'(V \setminus R(p)) < (n - n^4) \max_j y_j$.
5. Lemma 77 (p. 84): if $y \in \mathcal B(f)$ is non-degenerate and $y_i < -(n-1)\max_j y_j$, then $i$ is in every minimizer over $\mathcal F_A$.

The mission also contains Lemma 76 (the mirror of Lemma 77), Lemma 78 ($\mathrm{lower}(i) \le h_i \le \mathrm{upper}(i)$ for consistent BFS's) and Lemma 80 (the mirror of Lemma 79, giving an arc $(q, p)$ with $q \notin Q(p)$ when $\mathrm{lower}(p) < n^4 \min_j y_j$).

Significance

Lemmas 79 and 80 are what make the paper's SFM algorithms strongly polynomial: each application adds one of at most $2\binom n2$ arcs, and the cutting plane method supplies, through its separating hyperplanes, exactly the convex combinations of consistent BFS's the lemmas take as input. Lemma 80 has no counterpart in earlier work, and the two lemmas are stated for general ring families, which the earlier versions were not. They are also a robust version of Lemma 65: a point of the base polyhedron that is only approximately degenerate still yields structural information about every minimizer.

The lemmas are proved in the paper; none of them is formalized. The mission produces machine-checked statements and proofs of the arc-adding step, in a form independent of the cutting plane machinery and reusable by any formalization of a ring-family SFM algorithm (Iwata–Fleischer–Fujishige, Orlin, or Lee–Sidford–Wong).

Difficulty

The inequality chain of each lemma is short; the work is in the combinatorics of permutations. Moving $R(p)$ to the front of a permutation must be shown to produce a permutation again, and the comparison (15.2) depends on knowing exactly which elements precede each $j$ before and after the move; the identity $y'_p = \mathrm{upper}(p)$ holds only because consistency puts all of $R(p) - p$ before $p$, which needs an induction along paths of $A$. The restriction to $V \setminus R(p)$ changes the ground set, so Lemma 77, stated on the full ground set, does not apply verbatim to the restricted problem. The paper's application of Lemma 77 also does not check that the restricted vector is non-degenerate, so that case has to be handled as well.

Formalization scope

The ground set is Fin n (0-based); sets are Finset (Fin n), $f$ is integer valued and vectors are real. A permutation σ : Equiv.Perm (Fin n) is a position map ($u$ precedes $v$ iff σ u < σ v), and the BFS of a permutation is defined by the formula of Theorem 62; Theorem 62 itself (that these are the vertices of $\mathcal B(f)$) is not formalized and not needed. Arcs are a relation on Fin n; $R$ and $Q$ use its reflexive-transitive closure, and the digraph is assumed acyclic, as the paper does. Minimizers in Lemmas 76–80 are over the ring family $\mathcal F_A$; in Lemma 65 over all subsets. Constants $n^4$, $n - 1$ and $n - n^4$ are real numbers.

Running-time and oracle-count clauses ("using $O(n \cdot \mathrm{EO})$ oracle calls and $O(n^2)$ time") are out of scope, as is the paper's main Theorem 31 and the bound $O(n)$ on the number of BFS's in the combination (the existence claim holds for any finite combination). Validity of the new arc is stated in the strong form proved on p. 85: every minimizer containing $p$ contains $q$. The page's base polyhedron constraint "$\forall S \not\subseteq V$" is read as $S \subseteq V$. The restricted base polyhedron in the restriction claim uses the normalized $f' - f'(\emptyset)$.

The hypotheses are satisfiable: with $n = 2$, $A = \emptyset$, $f(\{0\}) = f(\{1\}) = 1000$, $f(\emptyset) = f(V) = 0$, the combination $(\tfrac12 + \tfrac1{64})(1000, -1000) + (\tfrac12 - \tfrac1{64})(-1000, 1000)$ satisfies them for $p = 0$. A modular $f$ never does, so the goal is not vacuous only because $f$ is genuinely submodular; a formalization in which the BFS's are not tied to $f$, or in which non-degeneracy is non-strict, would change the statement and is ruled out.

Useful infrastructure: greedy vectors of a submodular function lie in its base polyhedron; reordering lemmas for permutations of Fin n; restriction of a set function to the complement of a set. Contributions of proofs of any milestone, and of Lemmas 76, 78 and 80, are welcome.

Selected references

• Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, arXiv:1508.04874v2, 2015; FOCS 2015. https://arxiv.org/abs/1508.04874
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981). https://doi.org/10.1007/BF02579273
• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000). https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001). https://doi.org/10.1145/502090.502096
• J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009). https://doi.org/10.1007/s10107-007-0189-2
• S. T. McCormick, Submodular function minimization, Handbooks in OR & MS 12 (2005). https://doi.org/10.1016/S0927-0507(05)12007-6