Operations Research

Motivation

Alternating-offer bargaining asks how an agreement is selected when two people can keep making proposals until one accepts. A prediction based only on behavior at the start may rely on threats that would no longer be sensible after a rejection. Ariel Rubinstein's 1982 paper studies strategies after every possible sequence of offers and gives a characterization of the partitions compatible with perfect equilibrium. Its setting has a unit pie, complete information, no fixed last round, and preferences that may describe more than a particular discount formula.

The question matters for sequential bargaining models in which the order of moves and the cost of delay affect the agreement. The paper distinguishes the set obtained when player 1 offers first from the set obtained when player 2 offers first. It also provides applications to fixed bargaining costs and fixed discount factors. This mission targets the paper's general characterization, from which those examples can be studied without building a new equilibrium concept for each preference family.

Setting

A partition is a number $s\in S=[0,1]$: player 1 receives $s$ of the unit pie and player 2 receives $1-s$. An outcome $(s,t)$ means that the offer $s$ is accepted in period $t$; $(0,\infty)$ denotes perpetual disagreement. Periods of actual play start at 1. The paper also uses $(s,0)$ when comparing acceptance of a current offer with a future outcome. Each player $i\in\{1,2\}$ has a complete, reflexive, transitive preference relation $\succcurlyeq_i$ on outcomes. Strict preference $\succ_i$ and indifference $\sim_i$ are derived from it.

The game alternates proposals and responses. One player offers a partition, the other accepts or rejects, and rejection makes the responder the next proposer. A strategy specifies what a player does after every possible history, including histories inconsistent with the player's earlier plans. A perfect equilibrium requires the relevant player's continuation to withstand every alternative continuation strategy at each rejected history and to make a planned acceptance or rejection consistent with the current offer. The empty history is included, so the opening proposer must also have no profitable deviation.

Write $A$ for the set of player-1 shares reached by perfect equilibria when player 1 opens, and $B$ for the corresponding set when player 2 opens. Perpetual disagreement contributes no share to either set. Define $\Delta\subseteq S\times S$ by a pair of one-period thresholds: for $(x,y)\in\Delta$, $y$ is the smallest share whose immediate acceptance player 1 weakly prefers to $(x,1)$, and $x$ is the largest share whose immediate acceptance player 2 weakly prefers to $(y,1)$. Let $\Delta_1$ and $\Delta_2$ be its coordinate projections. All four sets contain numbers interpreted as player-1 shares, even when player 2 moves first. These are the objects of Sections 2–5.

Formalization targets

Characterization

Under the paper's five preference assumptions (A-1)–(A-5), the goal is its THEOREM on p. 106:

$$A=\Delta_1\ne\varnothing,\qquad B=\Delta_2\ne\varnothing,$$

with $A$ and $B$ nonempty closed intervals and some $e\ge 0$ satisfying

$$B=\{a-e:a\in A\}.$$

The translation parameter is allowed to be zero, and either interval may be a single point. The goal fixes the paper's general shape without choosing a particular utility representation or assuming immediate agreement in every equilibrium.

Milestone statements

The attack path follows Lemmas 1–4 and Propositions 1–4 in their printed order. The lemmas constrain how a partition in one opening order relates to a feasible continuation in the other. Proposition 1 places each pair in $\Delta$ inside $A\times B$; Proposition 2 asserts existence; Proposition 3 describes $\Delta$ as a closed segment parallel to the diagonal; Proposition 4 gives the reverse containment of $A$ and $B$ in the threshold projections. Each numbered result is a separate theorem target.

Significance

The theorem identifies the full set of equilibrium partitions from preference comparisons one period apart. Nonemptiness says the model admits at least one equilibrium partition in either opening order. The interval conclusion describes cases with multiple equilibrium shares, while the translate relation states exactly how reversing the first mover changes the two sets. In the paper's discounting example, a single share is selected under the stated parameter conditions; in a fixed-cost boundary case, multiple shares can occur. These are applications in Section 6, not assumptions of the general target.

Rubinstein proved the result in 1982. Here the definitions and theorem statements are Lean drafts; the numbered targets and the main theorem still require machine-checked proofs. A local verification module establishes that one discounting instance satisfies the first three axioms and that the paper's Section 3 strategy example accepts its first offer in period 1. Completing the mission would give a reusable formal account of an infinite-horizon alternating-offer game and its subgame equilibrium conditions, alongside the paper's characterization.

Difficulty

A first-round equilibrium condition does not control what a strategy promises after an offer is rejected. The paper's equilibrium definition checks the entire continuation at every history, with the player's role changing after each rejection. As a result, showing that a proposed share is an equilibrium partition requires more than checking the opening offer: the answer and the next proposal must remain consistent throughout the game tree. The model also allows arbitrary complete preferences satisfying axioms, so a calculation with one discount function cannot establish the general theorem.

The boundary at a zero share requires care. Assumption (A-2) asserts strict preference for earlier positive shares; it says nothing directly about a player receiving zero. The printed proof of Lemma 1 invokes it for a comparison that can occur at that boundary. The local lemma drafts explicitly carry the paper's (A-4) closedness axiom to support that comparison. This added assumption, and its propagation to Lemmas 2–4, is disclosed in the audit notes rather than silently attributed to the Section 4 statement.

Formalization scope

Lean represents $S$ as the subtype of real numbers in $[0,1]$. Outcomes are an option type: an agreement contains a partition and a natural-number period, while none is perpetual disagreement. This prevents an endless play from acquiring a default last partition. Strategies are unrestricted functions of lists of past offers. The play uses the first accepted offer, with period number one greater than its zero-based sequence index. A subgame after a rejected history restarts the period count and swaps the opening role when the history has odd length. The perfect-equilibrium predicate includes the empty history; acceptance comparisons use period 0 for the offer already on the table.

The threshold correspondence uses actual least and greatest elements among partitions in $S$. No real infimum or supremum supplies a default for an empty candidate set. “Closed interval” in the goal means an explicit $[\ell,u]$ with $\ell\le u$. “$A-e$” is the image of $A$ under $a\mapsto a-e$. Proposition 3's “parallel line segment” is the full image of a nonempty interval under $x\mapsto(x,x-e)$. These readings exclude a vacuous equilibrium set, a disagreement-to-zero coercion, and a hard-coded discounting special case.

The common outcome and preference definitions, the history-based strategy and play, and the equilibrium predicate are reusable for other alternating-offer questions. Contributions toward their structural properties, the numbered milestones, and the full theorem are in scope. The two displayed claims inside proofs and the fixed-cost and discounting conclusions are deferred to keep this proposal on the theorem's numbered path. Existing platform entries on Nash's axiomatic bargaining solution and a sealed-offer double auction concern different objects; neither supplies this game's equilibrium definition.

Selected references

• Ariel Rubinstein, Perfect Equilibrium in a Bargaining Model, Econometrica 50(1), 97–109, 1982. DOI 10.2307/1912531.

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, 441–450. https://doi.org/10.1287/moor.12.3.441
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.

Motivation

A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.

This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.

Setting

Let $S$ be a finite set of states and $s_0\in S$ the initial state. At each $s\in S$ there is a finite, nonempty decision set $D_s$. A decision $d\in D_s$ has a real cost $c(s,d)$ and moves the process with certainty to $\operatorname{next}(s,d)\in S$. All of these data are stationary: they do not change with time. A policy $\delta(s,t)$ chooses a decision for each state and each time $t=0,1,2,\ldots$. It generates a trajectory by $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.

The paper prints the finite average with $T+1$ cost terms and denominator $T$:

$$a_T^\delta(s_0)=\frac{1}{T}\sum_{t=0}^{T}c(s_t,\delta(s_t,t)).$$

A time-dependent policy's averages may fail to converge. We use the upper limit $g^\delta(s_0)=\limsup_{T\to\infty}a_T^\delta(s_0)$ and optimize over all policies, $g^*(s_0)=\inf_\delta g^\delta(s_0)$. A state $u$ is reachable if some finite walk of decision arcs goes from $s_0$ to $u$. A simple cycle $C$ is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is $\operatorname{mean}(C)=c(C)/|C|$. A loop is a one-arc simple cycle.

For states $u,v$, the min-plus adjacency entry $A_{uv}$ is the least cost of a decision arc from $u$ to $v$, or $+\infty$ when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus $(A^k)_{uv}$ represents the least cost of a $k$-arc walk from $u$ to $v$, when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.

Formalization targets

Reachable cycles

The first target identifies the value of the original policy optimization problem:

$$g^*(s_0)=\min_{\substack{C\text{ simple cycle}\\C\text{ reachable from }s_0}}\operatorname{mean}(C).$$

It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with $\liminf$, so it applies even when a policy's averages oscillate.

Min-plus calculation

The second target identifies the finite graph calculation used in the paper:

$$g^*(s_0)=\min_{\substack{u\text{ reachable from }s_0\\1\leq k\leq |S|\\(A^k)_{uu}<+\infty}}\frac{(A^k)_{uu}}{k}.$$

The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from $1$ through $|S|$ recover the least simple-cycle mean. The restriction to reachable $u$ is essential: a cheap cycle in a disconnected component cannot be used from $s_0$.

Significance

The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.

Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.

Difficulty

An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.

Formalization scope

Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; $A_{uv}$ takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once $s_0$ is supplied. Policy time starts at zero. The printed $T+1$ terms divided by $T$ are retained; Lean's $T=0$ quotient is zero and has no effect on the limit. The optimum is the infimum over all policies $\delta(s,t)$, not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.

The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, pp. 441–450. DOI.

Motivation

Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon $T$ much larger than the state set, so a method that processes all $T$ stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)

The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447

Setting

Let $S$ be a finite nonempty set of states, with $n=|S|$, and fix an initial state $s_0$. At each state $s$, a finite nonempty set $D_s$ contains the available decisions. A decision $d\in D_s$ has a certain successor state $\operatorname{next}(s,d)$ and a real cost $c(s,d)$. The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445

A policy is a function $\delta(s,t)\in D_s$ of both state and time. Starting at $s_0$, it produces $s_{t+1}=\operatorname{next}(s_t,\delta(s_t,t))$. In the convention of the paragraph before Theorem 5, horizon $T$ means $T$ decisions and therefore a walk with $T$ arcs. Its cost is

$$J_T(s_0,\delta)=\sum_{t=0}^{T-1}c(s_t,\delta(s_t,t)),\qquad J_T^*(s_0)=\inf_\delta J_T(s_0,\delta).$$

A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.

Formalization targets

The first milestone identifies $J_T^*(s_0)$ with the minimum cost of a $T$-arc walk from $s_0$. The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than $n$ times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447

For $l\le T$ and $u\in S$, let $w_{l,u}$ be the cheapest $l$-arc walk from $s_0$ that visits $u$. Let $r_{k,u}$ be the cheapest closed $k$-arc walk at $u$. Only choices for which these walks exist are included. The mission's goal is

$$J_T^*(s_0)=\min_{\substack{l\le T,\ l<n^3,\ u\in S,\\1\le k\le n,\ k\mid T-l}}\left(w_{l,u}+\frac{T-l}{k}\,r_{k,u}\right),\qquad T>n^2.$$

The $l<n^3$ bound is the paper's finite compression claim. The divisibility condition makes $(T-l)/k$ an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447

Significance

The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than $n^3$ arcs and closed walks of at most $n$ arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447

The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.

Difficulty

The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed $n^3$ bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447

Formalization scope

Lean represents $S$ and each $D_s$ as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an $l$-arc walk has states at indices $0,\ldots,l$.

The paper's general finite-horizon definition sums costs from $0$ through $T$, while the Theorem 5 paragraph explicitly asks for a $T$-arc walk. This mission follows the latter convention: decisions occur at $0,\ldots,T-1$. The goal also imposes $l\le T$, which the printed loop leaves implicit, and uses a closed walk for $r_{k,u}$ because that is what the length-$k$ graph calculation computes. It does not assume distinct walk costs. The condition $T>n^2$ is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447

Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.

Selected references

• Christos H. Papadimitriou and John N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. DOI: 10.1287/moor.12.3.441

Motivation

A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.

The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size $N$, and its threshold includes the case of $N$ support constraints. The paper's Section 6 gives the model and its two probability guarantees.

Setting

Let $S$ be a set of decisions. A subset $X\subseteq S$ is the domain; a real function $f:S\to\mathbb R$ is the cost. An uncertain outcome $\delta$ belongs to a measurable space $\Delta$ with probability measure $P$, and imposes a constraint set $X_\delta\subseteq S$. For a sample $\omega=(\delta^{(1)},\ldots,\delta^{(N)})$ of $N$ independent outcomes, the program minimizes $f(x)$ over $x\in X$ that belongs to every sampled $X_{\delta^{(i)}}$. The sample law is $P^N$. There is no algebraic or topological condition on the feasible sets or on $f$.

A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution $x_N^*(\omega)$ whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is $s_N^*(\omega)$. Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.

The violation of a decision is $V(x)=P\{\delta:x\notin X_\delta\}$. Thus $V(x_N^*)$ is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function $\varepsilon$ evaluated at the observed count, $\{V(x_N^*)>\varepsilon(s_N^*)\}$. For each $k\ge0$, the paper also uses a generalized distribution function $F_k(v)=P^k\{V(x_k^*)\le v,\ s_k^*=k\}$. It need not have total mass one.

Formalization targets

Variational bound, Theorem 3

For any $N\ge1$ and any $[0,1]$-valued $\varepsilon$ on $\{0,\ldots,N\}$, let $\gamma^*$ be the infimum of feasible values $q(1)$ over real polynomials of degree at most $N$ satisfying

$$\frac{q^{(k)}(t)}{k!}\ge {N\choose k}t^{N-k}{\bf1}_{[0,1-\varepsilon(k))}(t),\qquad 0\le k\le N,\quad 0\le t\le1.$$

The goal is the paper's Theorem 3:

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\gamma^*.$$

The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous $d$ in Theorem 3's range for $k$; its generic setting and variational problem use $0\le k\le N$.

Explicit confidence bound, Theorem 4

For $0<\beta<1$, the paper's Theorem 4 defines $t(k)\in(0,1)$ as the unique root of

$$\frac{\beta}{N+1}\sum_{m=k}^{N}{m\choose k}t^{m-k}-{N\choose k}t^{N-k}=0\qquad(0\le k<N).$$

With $\varepsilon(k)=1-t(k)$ for $k<N$ and $\varepsilon(N)=1$, its conclusion is

$$P^N\{V(x_N^*)>\varepsilon(s_N^*)\}\le\beta.$$

The terminal value $\varepsilon(N)=1$ is essential because the paper gives examples with $s_N^*=N$ and $V(x_N^*)=1$.

Significance

Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter $\beta$. The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.

A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and $\gamma^*$ must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.

Difficulty

The observed support count is data-dependent. Conditioning on $s_N^*=k$ therefore cannot be treated as conditioning on a fixed subset of $k$ sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with $N$, so the distributional characterization has one measure $F_k$ for every $k\ge0$ and moment equations for every sample size. The resulting infinite family must still be related to the finite degree-$N$ polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.

Formalization scope

Lean represents the decision set by an arbitrary type $S$, with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and $F_k$ are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that $S$ is nonempty.

The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The $F_k$ are finite measures on $\mathbb R$, so the paper's Stieltjes integrals are represented as integrals over $(\varepsilon(k),1]$ or $[0,1]$ against those measures. The polynomial class $\mathcal P_N$ means degree at most $N$, matching the $N+1$ coefficients in (36). The value $\gamma^*$ is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.

The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of $\gamma^*$, and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.

Selected references

• M. C. Campi and S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. DOI: 10.1007/s10107-016-1056-9. The mission uses the authors' accepted manuscript, especially Sections 6–7 and Theorems 3–4.

Motivation

In Stackelberg network pricing a leader sets prices on some resources, and a follower then buys the cheapest structure available to them, paying the leader for the priced resources they use. The Stackelberg Minimum Spanning Tree problem, introduced by Cardinal, Demaine, Fiorini, Joret, Langerman, Newman and Weimann (Algorithmica 2011), is the version in which the follower buys a minimum spanning tree. The best known approximation factors for it are those of uniform pricing, which gives every priced edge the same price (Berbeglia–Joret, p. 21).

Independently, revenue management studies assortment optimisation: a seller chooses which products to offer, and customers choose among the offered products according to a discrete choice model. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) analyse the revenue-ordered heuristic (offer every product whose revenue is at least some threshold) under any regular choice model, and prove tight approximation bounds.

§4.6 of that paper shows that the two problems are the same problem: a Stackelberg Matroid pricing instance is an assortment problem under a regular choice model, and uniform pricing is the revenue-ordered heuristic on that model. The bounds of Cardinal et al. on uniform pricing thus become special cases of the general bounds on revenue-ordered assortments. This mission formalizes that correspondence (Theorem 4.16).

Setting

Choice model. Let $\mathcal C$ be a finite set of products. A system of choice probabilities assigns to each offered set $S\subseteq\mathcal C$ and product $x$ a probability $\mathcal P(x,S)$, with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. It is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ whenever $S\subseteq S'$ and $x\in S\cup\{0\}$. With revenues $r:\mathcal C\to\mathbb R_{>0}$, $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$. The revenue-ordered assortment generated by $y$ is $\{y'\in\mathcal C:r(y')\ge r(y)\}$.

Greedy algorithm. Given a family of independent sets, a linear ordering $L$ and a set $F$, $\mathrm{greedy}(F,L)$ scans $F$ in the order induced by $L$, starting from $\emptyset$, and adds each element that keeps the current set independent.

Stackelberg Matroid problem. An instance is a matroid $M=(E,\mathcal X)$, a bipartition $E=R\sqcup B$ into red and blue elements, and red costs $c:R\to\mathbb R_{>0}$; some base of $M$ lies inside $R$. The leader chooses prices $p:B\to\mathbb R_{>0}$. The customer buys a minimum-weight base by running greedy on $R\cup B$ with an ordering $L^*$ that is non-decreasing in weight ($c$ on $R$, $p$ on $B$) and puts blue elements first on ties. The leader earns $\mathrm{rev}_{\mathrm{Stack}}(p,L^*)=\sum_{e\in B\cap\mathrm{greedy}_M(R\cup B,L^*)}p(e)$.

The assortment instance. Let $c_1<\dots<c_k$ be the distinct red costs. Products are $\mathcal C=B\times\{c_1,\dots,c_k\}$ with $r((e,q))=|B|\,q$. The auxiliary matroid $M'$ on $R\cup\mathcal C$ declares $X$ independent when it holds at most one pair $(e,q)$ per blue $e$ and $(R\cap X)\cup\{e:(e,q)\in X\}$ is independent in $M$. With an ordering $L$ of $R\cup\mathcal C$ that is non-decreasing in cost and puts products before red elements on ties, $\mathcal P((e,q),S)=1/|B|$ if $(e,q)\in\mathrm{greedy}_{M'}(R\cup S,L)$ and $0$ otherwise.

Formalization targets

Goal: Theorem 4.16 (p. 24)

For the instance above, with $B\ne\emptyset$ and every admissible $L$:

$$\mathcal P\ \text{is regular},\quad r>0,\qquad \max_{S\subseteq\mathcal C}\mathrm{rev}(S)=\max_{p>0,\ L^*}\mathrm{rev}_{\mathrm{Stack}}(p,L^*),$$

and uniform pricing corresponds to revenue-ordered assortments: for each $c_i$ some revenue-ordered assortment earns the revenue of the uniform price $c_i$, and every revenue-ordered assortment earns the revenue of some uniform price $c_i$.

Milestones

1. Lemma 4.14 (p. 23): for $F\subseteq F'$, $|\mathrm{greedy}_M(F',L)|\ge|\mathrm{greedy}_M(F,L)|$ and $F\cap\mathrm{greedy}_M(F',L)\subseteq\mathrm{greedy}_M(F,L)$.
2. Property (14) (p. 31): orderings agreeing on a block partition make greedy pick the same number of elements per block.
3. Lemma 4.15 (p. 23): the Stackelberg revenue does not depend on the compatible ordering.
4. $M'$ is a matroid (p. 32).
5. Regularity of $\mathcal P$ (pp. 32–33).
6. $\mathrm{rev}(S)$ equals the Stackelberg revenue of $p_S(e)=\min\{q:(e,q)\in S\}$ (pp. 33–34).
7. Rounding prices up to the cost levels does not decrease revenue (p. 34).
8. For prices in $\{c_1,\dots,c_k\}\cup\{+\infty\}$, $\mathrm{rev}(S_p)$ equals the Stackelberg revenue of $p$ (pp. 34–35).

Significance

Theorem 4.16 transfers every guarantee for revenue-ordered assortments under regular models to uniform pricing in Stackelberg Matroid pricing. Specialising Theorems 3.1, 3.2 and 3.3 of the paper through it gives exactly the three bounds on uniform pricing proved by Cardinal et al. for Stackelberg Minimum Spanning Tree (Theorem 3 of their paper), which those authors showed to be tight (p. 24). It also places uniform pricing inside a general picture: it is a threshold policy for a regular choice model whose purchase probabilities come from a matroid greedy algorithm, and the paper notes that the argument extends to polymatroids.

The result is proved in the paper, with two steps left to the reader ($M'$ is a matroid) or justified briefly (rounding prices). No machine-checked proof exists. A formalization also produces a reusable greedy algorithm on finite matroids with its monotonicity properties (Lemma 4.14, (14)), which Mathlib at the pinned revision does not have.

Difficulty

The obvious argument identifies the customer's run of greedy on $(M,R\cup B)$ with the run of greedy on $(M',R\cup S)$ step by step. That identification fails as stated: the choice probabilities are defined with one fixed ordering $L$ of $R\cup\mathcal C$, while the customer's ordering $L^*$ is any ordering compatible with the prices, and ties among blue elements of equal price, or between a product and a red element of equal cost, may be broken differently. Equality of revenues therefore needs the tie-independence property (14) applied to $M'$ as well as to $M$, which in turn needs $M'$ to be a matroid. A second gap is axiom (iv) for the no-purchase option: it requires that offering more products never decreases the number of products greedy selects, which is Lemma 4.14 (i)–(ii) for $M'$ combined, not a pointwise statement. Finally, the paper's "$+\infty$" price must be handled with the red base: without a base inside $R$, a blue element priced above all costs can still be bought and the optimum is unbounded.

Formalization scope

• Elements and orderings. The matroid is a Mathlib Matroid α; $R$, $B$ are Finset α with $R\cup B$ equal to the ground set; costs and prices are functions α → ℝ, used only on $R$ and $B$. A linear ordering is a duplicate-free List covering the set; greedy on $F$ scans the whole list and skips elements outside $F$, so $F$ is never re-sorted.
• Greedy is defined for an arbitrary independence predicate on finite sets, so that it applies to $M'$ before $M'$ is shown to be a matroid.
• Customer model. Compatibility (15a)–(15b), including blue priority on ties, is part of the definition of an admissible customer ordering. The red base is a field of every instance.
• Assortment instance. Elements of $R\cup\mathcal C$ live in α ⊕ (α × ℝ). The paper's conditions (1)–(2) for $M'$ contain two typos (a missing "$\in X$" and $\mathcal X$ for $X$); the intended conditions are formalized. The price $+\infty$ is the real number $1+\sum_{f\in R}c(f)$, strictly above every red cost.
• Goal shape. The theorem is stated for the explicit instance of the proof, for every admissible $L$. The optimum of the Stackelberg side is a maximum (IsGreatest) over positive real prices and all compatible customer orderings. Cost levels are quantified as elements of the set of red costs rather than by index.
• Ruled out. An existential statement ("some regular instance has the same optimum") is met by a single product with revenue $\mathrm{OPT}_{\mathrm{Stack}}$ and is not this theorem; so is a customer model without tie-breaking, a formalization without the red base, or Lemma 4.14 only for $F=F'$.

Contributions welcome: proofs of Lemma 4.14 and (14) for Mathlib matroids (reusable beyond this mission), the matroid property of parallel extensions such as $M'$, and the three revenue identities.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019 (Algorithmica, 2020). https://arxiv.org/abs/1606.01371
• J. Cardinal, E. D. Demaine, S. Fiorini, G. Joret, S. Langerman, I. Newman and O. Weimann, The Stackelberg Minimum Spanning Tree Game, Algorithmica 59(2):129–144, 2011. https://doi.org/10.1007/s00453-009-9299-y
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Vol. B, Algorithms and Combinatorics 24, Springer, 2003 (matroids and the greedy algorithm). https://link.springer.com/book/9783540443896

Motivation

Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.

D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.

Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.

Setting

Fix $n, m \in \mathbb N$, a vector $a \in \mathbb R^n$, a symmetric positive definite $n\times n$ matrix $G$, an $n\times m$ matrix $C$ with columns $n_1,\dots,n_m$, and $b \in \mathbb R^m$. The quadratic program (1.1) is

$$\min_x\ f(x) = a^{\mathsf T}x + \tfrac12 x^{\mathsf T}Gx \quad\text{subject to}\quad s_i(x) = n_i^{\mathsf T}x - b_i \ge 0,\quad i \in K = \{1,\dots,m\}.$$

The gradient is $g(x) = Gx + a$. For $J \subseteq K$, the subproblem $P(J)$ keeps only the constraints indexed by $J$; $P(\emptyset)$ is solved by $x^0 = -G^{-1}a$. A set $A \subseteq K$ is linearly independent if the normals $n_i$, $i\in A$, are.

For an independent $A$, let $N$ be the matrix with columns $n_i$, $i\in A$, and define

$$N^* = (N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1},\qquad H = G^{-1} - G^{-1}N(N^{\mathsf T}G^{-1}N)^{-1}N^{\mathsf T}G^{-1}.$$

The multipliers are $u(x) = N^*g(x)$; for a constraint $p \notin A$ with normal $n^+ = n_p$ the infeasibility multipliers are $r = N^*n^+$; a superscript $+$ denotes the same objects for $A^+ = A\cup\{p\}$.

An S-pair $(x, A)$ is an independent active set $A$ with $s_i(x) = 0$ for $i\in A$ and $x$ optimal for $P(A)$. A V-triple $(x, A, p)$ has $p\notin A$, $A^+$ independent, $s_p(x) < 0$, $s_i(x) = 0$ for $i \in A$, $H^+g(x) = 0$ and $u^+(x) = (N^+)^*g(x) \ge 0$.

The dual algorithm starts from $(x^0, \emptyset)$. In Step 1 it stops if $x$ is feasible; otherwise it picks any violated constraint $p$. In Step 2 it moves along the primal direction $z = Hn^+$ and the dual direction $(-r; 1)$ with step $t = \min\{t_1, t_2\}$, where $t_1$ is the largest step that keeps the multipliers nonnegative and $t_2 = -s_p(x)/z^{\mathsf T}n^+$ makes constraint $p$ active. If both are infinite it reports infeasibility. A full step ($t = t_2$) adds $p$ and returns to Step 1. A partial step ($t = t_1 < t_2$), or a dual step ($z = 0$), drops a constraint $k$ attaining $t_1$ and repeats Step 2.

Formalization targets

Goal: Theorem 3 (p. 11)

For every choice of the violated constraint $p$ and of the dropped constraint $k$:

$$\text{no run from } (x^0,\emptyset) \text{ is infinite, and every run that cannot continue ends in } \begin{cases}\text{STOP at an optimal } x \text{ of (1.1)}, \text{ or}\\ \text{STOP with } \{x : C^{\mathsf T}x \ge b\} = \emptyset.\end{cases}$$

Milestones, in attack order

1. Properties (2.6)–(2.9) (p. 5): $Hw = 0 \iff w \in \operatorname{range} N$; $H \succeq 0$; $HGH = H$; $N^*GH = 0$.
2. Optimality conditions (2.3)–(2.4) (p. 5): on the manifold of $A$, $x$ solves $P(A)$ iff $N^*g(x) \ge 0$ and $Hg(x) = 0$.
3. Lemma 1 (p. 8): along $\bar x = x + tHn^+$ from a V-triple, $H^+g(\bar x) = 0$, the constraints of $A$ stay active, $u^+(\bar x) = u^+(x) + t(-r;1)$ and $s_p(\bar x) = s_p(x) + t\,z^{\mathsf T}n^+$.
4. Theorem 1 (pp. 8–9): the step $t = \min\{t_1,t_2\}$ increases $s_p$ and $f$; a partial step yields a V-triple, a full step an S-pair.
5. Theorem 2 (p. 10): if $n_p = Nr$ and $s_p(x) < 0$ at an S-pair, then $r \le 0$ means $P(A\cup\{p\})$ is infeasible; otherwise dropping a minimizing $k$ gives a V-triple.
6. One round of Step 2 (p. 11): from an S-pair and a violated $p$, at most $|A|$ partial or dual steps and one final step end either in infeasibility of (1.1) or in a new S-pair $(\bar x, \bar A \cup\{p\})$ with $\bar A\subseteq A$ and $f(\bar x) > f(x)$.

Significance

Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.

The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for $N^*$ and $H$, a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.

Difficulty

The obvious termination argument is that $f$ increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave $x$ unchanged (the dual steps of Step 2(c)(ii)), so $f$ is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move $x$. Any such argument relies on invariants (independence of $A^+$, nonnegativity of the multipliers, $s_p < 0$ along partial steps) that hold only on reachable states, and the operators $N^*$ and $H$ are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.

Formalization scope

Vectors are Fin n → ℝ, $G$ is Matrix (Fin n) (Fin n) ℝ with G.PosDef, $C$ is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in $A$. Lean's matrix inverse returns $0$ for singular matrices, so every statement about $N^*$ and $H$ assumes $G \succ 0$ and an independent active set (directly, or through an S-pair or V-triple).

The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of $p$ and $k$. Infinite step lengths are separate transitions; a tie $t_1 = t_2$ takes the full step, as the paper tests $t = t_2$ first. The running value of $f$ and the factorizations of Section 4 are not part of the state.

Explicit readings of the paper's words:

• "solves the QPP or indicates infeasibility in a finite number of steps" is: no infinite sequence of Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);
• "S-pair" is: $A$ independent and active at $x$, with $x$ optimal for $P(A)$ (the reading every use in the paper needs);
• in Theorem 1 the partial-step clause carries $t < t_2$ (as in its proof), and the multiplier printed $u^+_{j+1}$ in (3.16) is $u^+_{q+1}$, the entry belonging to $p$;
• "an S-pair can never reoccur" is expressed as the strict increase $f(\bar x) > f(x)$ in milestone 6.

Property (2.10), printed $HH^+ = H^+$, is false unless $G = I$ and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.

A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.

Needed infrastructure: Schur-complement and projector identities for $N^*$ and $H$; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about $N^*$ and $H$, are welcome.

Selected references

• D. Goldfarb and A. Idnani, A numerically stable dual method for solving strictly convex quadratic programs, Mathematical Programming 27 (1983) 1–33. https://doi.org/10.1007/BF02591962
• C. E. Lemke, A method of solution for quadratic programs, Management Science 8 (1962) 442–453. https://doi.org/10.1287/mnsc.8.4.442
• J. Nocedal and S. J. Wright, Numerical Optimization, 2nd ed., Springer, 2006, Chapter 16. https://doi.org/10.1007/978-0-387-40065-5

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$. At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$, and one customer either buys a product $c_t\in S_t$ or buys nothing ($c_t=0$). Given $S_t=S$, the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$:

$$p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$. The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$, $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

$$\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).$$

The seller knows $r$ and $\mathcal S$ but not $v$.

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$, $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$, and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

$$v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},$$

starting from $v^{\mathrm{UCB}}_{i,0}=1$, and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$, and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$,

$$\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .$$

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

1. The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
2. Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
3. Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$, and its rate of convergence.
4. Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$) and Lemma 4.2.
5. The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
6. The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$-cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$.

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

• Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$, as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$, and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
• Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$).
• Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$, never $v$. Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$.
• Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$, on the event that epoch $\ell$ is completed by customer $T$; uniformity in $T$ is the paper's infinite-horizon statement.
• Repairs of the page, all disclosed in the items:
  1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$.
  2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$.
  3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$.
  4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
  5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
  6. (A.14) is an inequality, since the horizon cuts the last epoch.
• Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
• No trivialization. The policy cannot see $v$, the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
• Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. doi:10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. doi:10.1287/msom.2013.0429
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.

Why coverage of an optimal value matters

Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.

The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.

Decisions, losses, and divergence neighborhoods

Let $\mathcal X\subseteq\mathbb R^d$ be a nonempty compact decision set. An observation $\xi$ has population law $P_0$, and $\ell(x;\xi)\in\mathbb R$ is the loss at decision $x$. The quantity of interest is the optimal-value functional

$$T_{\rm opt}(P)=\inf_{x\in\mathcal X}\mathbb E_P[\ell(x;\xi)].$$

The observations $\xi_1,\ldots,\xi_n$ are independent and identically distributed with law $P_0$. Write $\widehat P_n$ for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights $p_i$ with $\sum_i p_i=1$. Indexed weights also cover samples with repeated observations. For a convex divergence generator $f$ normalized by $f(1)=f'(1)=0$ and $f''(1)=2$, its divergence from the empirical law is $D_f(p\|\widehat P_n)=n^{-1}\sum_i f(np_i)$. Assumption A further requires $f$ to be three times continuously differentiable near $1$; it permits $f(0)=+\infty$.

At radius $\rho/n$, the divergence ball consists of the weights with $\sum_i f(np_i)\le\rho$. The confidence set is its image under $T_{\rm opt}$:

$$C_{n,\rho}=\{T_{\rm opt}(p):D_f(p\|\widehat P_n)\le\rho/n\}.$$

Assumption B makes $\mathcal X$ compact and requires $\ell(\cdot;\xi)$ to be Lipschitz on it with a measurable random coefficient $M(\xi)$. The theorem adds finite second moments for $M$ and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.

Formalization targets

The goal is the exact asymptotic coverage of the population optimal value, with $x^\star$ the unique optimizer and $\operatorname{Var}_{P_0}(\ell(x^\star;\xi))>0$:

$$P^*\!\left(T_{\rm opt}(P_0)\in C_{n,\rho}\right)\longrightarrow P(\chi_1^2\le\rho),\qquad \rho\ge0.$$

Here $P^*$ denotes outer probability, and $\chi_1^2$ is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of $C_{n,\rho}$; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set $C_{n,\rho}$, including both sides of that interval.

What the result provides

The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.

A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.

The mathematical obstacle

Pointwise control of each loss $\ell(x;\xi)$ is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over $x$. The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.

Formalization scope

Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first $n$ observations are indices $0,\ldots,n-1$. Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.

The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius $\rho/n$ and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is $\sup_p\inf_x$; the different minimax expression $\inf_x\sup_p$ is not substituted. The chi square target uses the standard Gaussian measure of $\{z:z^2\le\rho\}$.

Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action $H(x)$ on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.

Selected references

• John C. Duchi, Peter W. Glynn, and Hongseok Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; published in Mathematics of Operations Research 46(3), 2021. arXiv preprint