Operations Research

Motivation

Mission XII (12-packet-networks-model) built the discrete-time, slotted packet-network model from scratch and proved the chapter's own version of the fluid-to-stochastic stability bridge (Theorem 12.10). That result is only useful once paired with an actual control policy whose fluid model can be shown stable. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly such a policy in Sections 12.4-12.5: back-pressure control (called max-weight when the network is single-hop), a rule that has become the default choice in the switching and wireless-scheduling literature because it requires no advance knowledge of arrival rates and achieves the largest possible stability region. This mission formalizes back-pressure control for the discrete-time packet network model and proves it maximally stable — the chapter's own counterpart to mission VIII's continuous-time Theorem 9.12.

Setting

At the start of each timeslot, having observed the current buffer contents $z$, the max-weight/ back-pressure (MW/BP) policy solves $\max_{s\in S(z)} z\cdot Rs$ (Eq. 12.41), where $S(z) := \{s\in S : Bs\le z\}$ restricts the schedule set $S$ (mission XII) to what is actually available given $z$. Equivalently (Eq. 12.42-12.43), writing $w_j(z) := z_{u(j)} - z_{d(j)}$ (with $z_0 := 0$) for the "weight" of activity $j$, the policy maximizes $\sum_j w_j(z) s_j$ — the schedule that clears the most "backlog pressure" per timeslot. The policy is deterministic (no randomization variable is needed, since (12.41) is a genuine optimization problem, not one that inherently requires randomized tie-breaking).

Formalization targets

Goal: Theorem 12.16 — aperiodicity, irreducibility, and conditional positive recurrence

Consider a packet network satisfying (12.1) and Assumption 12.1, operating under back-pressure control. The DTMC $Z$ is aperiodic and irreducible unconditionally. If the stability condition (12.26) — the existence of $\hat s\in\langle S\rangle$ with $\lambda < R\hat s$ — is additionally satisfied, $Z$ is positive recurrent. This is the mission's headline result, and it packages both a structural fact (irreducibility/aperiodicity, needed regardless of load) and a conditional stability fact (positive recurrence, needed only under (12.26)) in one theorem.

Supporting milestones

Lemma 12.17 shows the optimization problem (12.41) always has a nonzero solution whenever the network is nonempty — the fact that back-pressure never "idles unnecessarily," which Lemma 12.18 uses to show every state can reach the empty state (hence irreducibility) and that state $0$ has period $1$ (hence aperiodicity, via (12.1)'s own assumption that no external arrivals is possible with positive probability). Lemma 12.20 is the back-pressure fluid equation (12.44), the discrete-time analog of mission VIII's Theorem 9.8: at each regular point, the fluid-scaled buffer content dotted with the fluid departure rate equals the maximum of that same dot product over the convex hull of the schedule set. Lemma 12.21 shows this fluid model is stable whenever (12.26) holds, via an explicit quadratic Lyapunov function.

Significance

The result itself. Theorem 12.16 shows that back-pressure control — a rule requiring no knowledge of arrival rates, computed fresh from the current buffer contents every timeslot — is maximally stable: combined with Theorem 12.8 and Proposition 12.9 (mission XII), it stabilizes every packet network arrival-rate vector that any policy could possibly stabilize. This is the discrete-time, slotted analog of mission VIII's Theorem 9.12, and the two proofs share their essential Lyapunov argument (the book's own text calls Lemma 12.21's proof "almost identical to that of Theorem 9.12"), even though the two chapters' back-pressure equations are built from different underlying objects — mission VIII's continuous-time allocation polytope versus this chapter's convex hull of a discrete schedule set.

Formalizing it. A live prior-art check (GET /theorems?q=back-pressure, q=max-weight) finds no relevant hits, matching mission VIII's own finding for the continuous-time version. This mission formalizes the back-pressure optimization problem and policy, the back-pressure fluid equation, and its stability from scratch, restating (per this series' convention for concurrently-drafted chunks sharing a sub-namespace) the minimal apparatus needed from mission XII: the packet network model, Assumption 12.1, the raw processes, fluid limit paths, the fluid equations (12.31)-(12.36), and the ambient-chain machinery, plus a new Aperiodic predicate this chunk needs that mission XII's own results do not.

Difficulty

The obvious approach to Lemma 12.20's back-pressure fluid equation — directly differentiate the discrete system equation — obscures the actual argument, which reduces a maximum over the (potentially non-polytope) discrete schedule set $S$ to a maximum over its convex hull $\langle S\rangle$ (justified because a linear functional on a compact polytope is maximized at an extreme point) and then shows that every schedule with a strictly smaller objective value than the maximizer contributes zero derivative to the usage-counting process $\hat T_s$ — the discrete-time analog of mission VIII's Lemmas 9.10-9.11. A second difficulty is connecting the maximum-over-a- finite-set at the fluid-scaled level to Definition 12.3's discrete, arrival-indexed back-pressure policy: this mission's own Lemma 12.20 item states the fluid-relevant consequence of the discrete policy as a documented hypothesis (mirroring mission XI's own scope decision for its structurally identical WWTA fluid equation) rather than re-deriving it from the raw stochastic recursion, which would require reconstructing infrastructure outside this chapter's own numbered results.

Formalization scope

The packet network model, Assumption 12.1, the raw processes, and the fluid-limit apparatus are restated verbatim from mission XII (12-packet-networks-model), since concurrently-drafted chunks sharing a sub-namespace do not import one another's Lean files. IsBPOptimal is phrased via domination over the feasible-at-$z$ schedule set, not sSup/argmax, per this series' junk-value-avoidance convention; the same convention is applied to the maximum over $\langle S\rangle$ in the back-pressure fluid equation. The formalization does not admit a trivializing reading: irreducibility and aperiodicity are the same non-vacuous renewal-theoretic notions used throughout this series (Aperiodic requires a genuine positive self-transition probability, not a vacuously-true condition), and the goal's positive-recurrence conjunct is genuinely conditional on (12.26), stated with the correct strict inequality rather than weakened to $\le$. Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.17's hop-count induction and Lemma 12.20's extreme-point/zero-derivative argument (mirroring mission VIII's own Lemmas 9.10-9.11, adapted to discrete time).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

Motivation

Internet routers, wireless base stations, and data-switch fabrics all face the same recurring decision: in each discrete time slot, which of many possible transfer operations should be executed, given the packets currently queued and the physical constraints (link capacities, interference between simultaneous transmissions) on what can be done at once? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 12 to exactly this question, under the name packet networks. Unlike every prior chapter of the book, which works in continuous time with Poisson-driven Markov chains, this chapter builds its stability theory from scratch for a discrete-time, slotted model — the natural setting for a system that makes one scheduling decision per clock tick. This mission formalizes the chapter's foundational layer: the model itself, its notion of a feasible schedule and control policy, subcriticality, and the discrete-time fluid-limit machinery that Chapters 13 and 14 (back-pressure control and random proportional scheduling, respectively) build their own stability proofs on top of.

Setting

A packet network (Section 12.1) has I packet classes and J activities (service types); activity $j$ transfers a packet from its input class $u(j)$ to its output class $d(j)$ (or removes it from the network if $d(j)=0$), giving an $I\times J$ input-output matrix $R$. A processing plan for class $i$ (Definition 12.2) is a chain of activities from $i$ to exit; Assumption 12.1 requires every class to have one and forbids cycles. In each timeslot the system manager chooses a schedule $s\in\mathbb Z^J_+$ from a feasible set $S$ satisfying the packet-availability constraint $Bs\le z$ (the current buffer contents); $S$ is typically built (Section 12.2) from a link usage matrix $A$ and a set $C$ of feasible link configurations via $S_c := \{s : As\le c\}$, $S := \bigcup_{c\in C} S_c$. A Markovian control policy (Definition 12.3, Eq. 12.8) chooses $s(\tau) = f(Z(\tau-1), U(\tau))$ from the current buffer contents and an independent randomization variable; it is admissible if it never overdraws a buffer, and stable if the resulting discrete-time Markov chain $Z$ is irreducible and positive recurrent.

Formalization targets

Goal: Theorem 12.10 — fluid limit stability implies positive recurrence

If the DTMC $Z$ under a Markovian policy $f$ is irreducible and its fluid limit is stable (Definitions 12.14-12.15), then $Z$ is positive recurrent. This is the chapter's own version of Theorem 6.2 (mission III) — the technical fulcrum that lets a deterministic fluid-model stability argument certify the stability of the original discrete, stochastic system — restated for a genuinely different probabilistic model, since Theorem 6.2 was built under continuous-time, Poisson-arrival hypotheses this chapter does not share.

Supporting milestones

Propositions 12.6-12.7 characterize the convex hulls $\langle S_c\rangle$ and $\langle S\rangle$ as explicit polytopes cut out by the link usage matrix — the combinatorial core that Theorem 12.8 (stability implies subcriticality, this chapter's analog of Theorem 5.2) and Proposition 12.9 (a necessary condition for subcriticality) both build on. Lemma 12.11 records that the schedule-usage counting process is Lipschitz; Lemma 12.12 is the functional strong law of large numbers the external arrival process satisfies; and Theorem 12.13 combines them to establish existence of discrete-time fluid limits satisfying the chapter's own fluid equations (12.31)-(12.36) — the chapter's analog of Theorem 6.5.

Significance

The result itself. Theorem 12.10 is what makes the rest of Chapter 12 (and Chapters 13-14) tractable: rather than analyzing an infinite-state discrete-time Markov chain's positive recurrence directly — a notoriously hard problem in general — it suffices to exhibit a deterministic fluid model and show every solution of that fluid model empties in finite time. This is the same strategy Chapter 6 established for the book's continuous-time model, but Chapter 12 cannot simply invoke that earlier theorem: the packet network model uses discrete time slots rather than a continuous clock, and its probabilistic structure (arbitrary i.i.d. arrival increments rather than Poisson arrivals) is different enough that the fluid-limit compactness argument has to be redone, even though — as the book's own text notes — "the proof mimics that of Theorem 6.2."

Formalizing it. A live prior-art check (GET /theorems?q=packet+network, q=discrete-time+Markov+chain, q=slotted+time) finds no relevant hits. A dedicated further check for MarkovMixing, a different mission's own corpus offering a PositiveRecurrent predicate for Markov chains, found a representationally distinct formalization (a row-function transition kernel rather than this series' own PMF-based jump-chain convention); this mission restates positive recurrence and irreducibility locally instead, consistent with every mission in this series since mission I. Everything else — the packet network model, schedules and configurations, the subcritical region, Markovian policies, and the discrete-time fluid-limit apparatus — is formalized from scratch.

Difficulty

The most consequential decision in this mission is representational, not mathematical: Theorem 12.10's fluid-limit-stability hypothesis quantifies over all fluid limit paths, which are themselves scaling limits of a genuinely stochastic discrete-time process — reconstructing that process from Chapter 2/4's own primitive stochastic elements (arrival processes, phase-type service mechanics) would require rebuilding infrastructure this chapter's own numbered results do not supply. Following mission III's own precedent for its structurally identical Theorem 6.5, this mission instead takes the raw, per-initial-state schedule-usage and arrival processes as given data satisfying only the recap properties the chapter's own proofs actually cite (Eq. 12.9-12.10's system equation, monotonicity), and fixes a single sample point together with an explicit SLLN hypothesis rather than a bare "for almost all $\omega$" quantifier — matching the book's own statement of Theorem 12.13, which itself begins "Fix an $\omega\in\Omega_1$" rather than quantifying almost everywhere within the theorem itself. A second difficulty is genuinely combinatorial: Proposition 12.6's proof constructs an explicit product-form probability distribution over schedules (one independent randomization per link) whose mean recovers an arbitrary point of the polytope $\{Ax\le c\}$ — a real combinatorial argument, not a formal consequence of the convex-hull operator's definition.

Formalization scope

Classes, activities, links, schedules and configurations are represented via Fin-indexed types throughout; S and C are taken as Finsets (every worked example in the book has finitely many configurations, and the link usage matrix's single-1-per-column structure bounds each schedule component, so this is a genuine, if implicit, standing feature of the model rather than an added restriction). IsScheduleSetAt/IsScheduleSet characterize $S_c$/$S$ via an ↔ against the underlying capacity constraint, rather than constructing them, matching how set-valued model data is handled elsewhere in this series. The formalization does not admit a trivializing reading: the ambient chain's positive recurrence (PositiveRecurrent) is the same non-vacuous renewal-theoretic notion used throughout this series, PacketFluidLimitStable quantifies over every genuine fluid limit path (not a hand-picked one), and subcriticalRegion is stated with a strict inequality ($A\hat s < \hat c$) exactly as Eq. 12.24 requires, not weakened to $\le$. Contributions completing the eight by sorry proofs are welcome, particularly Proposition 12.6's explicit randomized- schedule construction and Theorem 12.13's compactness argument (mirroring mission III's own Theorem 6.5 proof, adapted to discrete time).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org

Motivation

Large-scale data-intensive computing splits a job into many small "map tasks," each of which must be assigned to one of thousands of general-purpose servers in a data center — the MapReduce paradigm introduced by Dean and Ghemawat (2008). Because a task's input data is stored on only a few of those servers, routing it to a server that already holds its data ("data locality") avoids costly network transfer, so a task-allocation policy that ignores locality can leave a server farm badly underutilized even when raw compute capacity is ample. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 11 to a rigorous stability analysis of Xie, Yekkehkhany, and Lu's (2016) workload-weighted task allocation (WWTA) policy, which routes each arriving task to whichever eligible server currently carries the least (locality-weighted) backlog. This mission formalizes the chapter's central result: WWTA is not merely a reasonable heuristic but is maximally stable — it keeps the system stable whenever any routing policy could.

Setting

A task allocation model (Sections 11.2-11.3) has L task categories and K servers; a class is a pair $(\ell,k)$, a category routed to a specific server, with mean service time $m_{\ell k} > 0$ (Eq. 11.3) reflecting both data locality (local, rack-local, or remote access) and the server's relative processing speed. Tasks in category $\ell$ arrive according to a Markovian arrival process (MArP) with long-run average rate $\nu_\ell$ — a substantially more general model than the independent Poisson streams used elsewhere in the book, needed to capture batches of map tasks generated from a single job. Routing is by immediate commitment: each task is assigned to a server the instant it arrives, based only on its category and the current backlog, with no possibility of later reassignment. The workload of server $k$ at time $t$ (Eq. 11.7) is $W_k(t) := \sum_\ell m_{\ell k} Z_{\ell k}(t)$, the locality-weighted total backlog assigned to it. Workload-weighted task allocation (WWTA), Definition 11.3, routes an arriving category-$\ell$ task to any server achieving $\operatorname{argmin}_{k} m_{\ell k} W_k(t-)$ (Eq. 11.8, ties broken arbitrarily), where $W(t-)$ is the workload vector's left limit at the arrival instant.

Formalization targets

Goal: Theorem 11.6 — WWTA fluid model stability under the load condition

If there exists $\lambda = (\lambda_{\ell k}) \ge 0$ with $\sum_k \lambda_{\ell k} = \nu_\ell$ for each category (Eq. 11.4) and $\sum_\ell m_{\ell k}\lambda_{\ell k} < 1$ for each server (Eq. 11.5), then the WWTA fluid model — the deterministic fluid equations (11.11)-(11.16) that arise as scaling limits of the stochastic model under WWTA control — is stable: every solution reaches the zero state in finite time proportional to its initial size.

Supporting milestones

Lemma 11.2 shows this load condition is equivalent to subcriticality of the task allocation model, in the sense of Section 5.2's general definition, reducing an existence statement over the model's full $G,R,A,b$ apparatus to a simple linear-feasibility check. Theorem 11.4 establishes that fluid limits of the stochastic model exist and satisfy the general fluid equations (11.11)-(11.15) under any immediate-commitment routing policy, and the WWTA-specific equation (11.16) under WWTA — the chapter's version of the fluid-limit machinery Chapter 6 builds for the book's standard model, adapted to Markovian (not Poisson) arrivals and immediate-commitment routing. Theorem 11.5 is the corresponding replacement for Theorem 6.2 (mission III): fluid limit stability implies stability of the original stochastic model. Corollary 11.7 is the mission's other headline consequence: WWTA is maximally stable, stabilizing the model whenever any simply structured routing policy could.

Significance

The result itself. A task-allocation heuristic motivated purely by an intuitive "balance-the-weighted-backlog" idea turns out to have the strongest stability guarantee a policy can have: it never needs re-tuning as arrival rates change, and no alternative policy can stabilize a regime WWTA cannot. Xie, Yekkehkhany, and Lu (2016) proved this fact (calling it "throughput optimality") by direct analysis of the discrete stochastic model using a quadratic Lyapunov function; Dai and Harrison's contribution is to prove the same conclusion via the fluid-model route, and — because the task allocation model violates two of the standing assumptions under which Chapter 6's general theory was built (MArP rather than Poisson arrivals, immediate-commitment routing rather than the book's default relaxed control) — to show that the general fluid-stability machinery survives those changes with only minor modification.

Formalizing it. A live prior-art check (GET /theorems?q=task+allocation, q=server%20farm, q=data%20locality) finds no relevant hits on the platform (workload returns one unrelated text-corpus-statistics result). This mission formalizes the task allocation model, WWTA, the fluid equations, and the stochastic-to-fluid bridge from scratch, reusing Mathlib's general real-analysis, measure-theory, and PMF-based Markov-chain substrate, and restating (per this series' convention for concurrently-drafted chunks) the minimal apparatus needed from missions I and III.

Difficulty

The obvious approach to Definition 11.3 — pick a canonical minimizer of $m_{\ell\cdot}W_\cdot(t-)$, e.g. via Finset.min' — silently narrows WWTA to a single tie-breaking rule, when (11.8) explicitly allows any minimizer; this mission instead states WWTA as domination over every server, accepting every admissible tie-break. A second difficulty is genuinely structural: Theorem 11.4's "for almost all $\omega$" existence claim is a measure-theoretic statement about a probability space that mission III's own analogous Theorem 6.5 sidesteps by fixing a sample point $\omega$ together with the specific SLLN limit that argument needs — this mission follows the same precedent rather than introducing a bare "almost everywhere" quantifier, which does not by itself supply the type information Lean's typeclass resolution needs to identify an ambient measure. A third is connecting Definition 11.3's discrete, arrival-indexed routing rule to the raw (pre-limit) process family that Theorem 11.4's existence argument operates on: the book's own proof derives the needed consequence (Eq. 11.22, "server $k$ receives no more category-$\ell$ tasks in a neighbourhood of $t$") via an explicit $\varepsilon$-$\delta$ argument from the discrete policy, which this mission takes as a documented hypothesis rather than re-deriving, since building the arrival-sequence-to-counting-process reconstruction is genuinely Chapter 2/4 machinery outside this chapter's own numbered results.

Formalization scope

Classes are represented as pairs (ℓ,k) : Fin L × Fin K rather than flattened to a single index, avoiding an arbitrary choice of encoding. TaskAllocationProcessFamily, FluidLimitPath, and TaskAllocationFluidLimitStable restate mission III's SPNProcessFamily/FluidLimitPath/ FluidLimitStable apparatus, adapted to this model's (E,D,Z) triple and doubly-indexed classes; PositiveRecurrent restates mission I's renewal-theoretic positive-recurrence notion. The formalization does not admit a trivializing reading: IsWWTA accepts every admissible tie-break rather than a single canonical one, SatisfiesWWTAFluidEquation requires Nonempty (Fin K) so its min_{k} is a genuine minimum rather than a junk value at zero servers, and the goal's conclusion WWTAFluidStable is the same non-vacuous fluid-model-stability predicate (Definition 6.3, specialized) used throughout this series. Contributions completing the five by sorry proofs are welcome, particularly Theorem 11.4's fluid-limit compactness argument (mirroring mission III's own Theorem 6.5 proof) and Theorem 11.6's explicit quadratic-Lyapunov-function argument.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. Dean and S. Ghemawat, "MapReduce: simplified data processing on large clusters," Communications of the ACM 51 (2008), 107–113.
• Q. Xie, A. Yekkehkhany, and Y. Lu, "Scheduling with multi-level data locality: throughput and heavy-traffic optimality," IEEE INFOCOM 2016.

Motivation

An inventory manager who stocks many products, faces random demand and pays ordering, holding and shortage costs must decide each period how much of each product to order. In general the optimal decision depends on the whole state and is found by solving a dynamic programme, which becomes impractical as the number of products grows. Myopic (or base stock) policies avoid this: in each period they aim at a target level computed from that period's data alone. Knowing when such a policy is optimal over an infinite horizon tells a practitioner when the multi-period problem decouples into a sequence of one-period problems.

Arthur F. Veinott, Jr. gave such conditions in Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem (Management Science 12(3):206–222, 1965). Earlier results of this type were for a single product (the paper cites Karlin, Management Science 6(3), 1960, Bellman–Glicksberg–Gross, Management Science 2(1), 1955, Iglehart–Karlin 1962, and the Arrow–Karlin–Scarf volume of 1958); Veinott's model allows several products, several demand classes, costs and demand distributions that change over time, general ordering constraints and general stock dynamics (backlogging, lost sales, and mixtures), and it does not use the functional equation of dynamic programming. Instead, the proofs analyse the inventory process directly.

Setting

There are $n$ products and $m$ demand classes. Vectors are compared componentwise: $u \le v$ means $u_j \le v_j$ for all $j$. In period $i = 1, 2, \dots$ the manager observes the inventory vector $x_i \in X_i \subseteq \mathbb{R}^n$ (negative coordinates are backlogs) and orders up to a vector $y_i \in Y_i \subseteq \mathbb{R}^n$, subject to $y_i \ge q_i(x_i)$, where $q_i$ is a vector of extended-real functions (for instance $q_i(x) = x$ forbids disposal). A random demand vector $D_i$ with law $\Phi_i$ and values in a Borel set $\mathfrak{D}_i \subseteq \mathbb{R}^m$ then occurs, and the next inventory vector is $x_{i+1} = s_i(y_i, D_i) \in X_{i+1}$. The demands $D_1, D_2, \dots$ are independent. Ordering $y_i - x_i$ costs $c_i \cdot (y_i - x_i)$, the holding and shortage cost is $g_i(y_i, D_i)$, and $\alpha_i \ge 0$ is the discount factor of period $i$.

Regrouping the ordering costs gives the one-period cost

$$W_i(y,t) = c_i\, y + g_i(y,t) - \alpha_i\, c_{i+1}\, s_i(y,t), \qquad G_i(y) = \int_{\mathfrak{D}_i} W_i(y,t)\, d\Phi_i(t),$$

with discount weights $\beta_1 = 1$ and $\beta_i = \alpha_1 \cdots \alpha_{i-1}$. The integrals are assumed finite, and $G_i \ge \gamma_i$ with $\sum_i |\beta_i \gamma_i| < \infty$. An ordering policy $\bar Y$ chooses $y_i$ as a Borel function of the past; it is feasible if $y_i \in Y_i$ and $y_i \ge q_i(x_i)$ for every possible history. Its cost is

$$f(x_1 \mid \bar Y) = \sum_{i=1}^\infty \beta_i\, E\, G_i(y_i) \in (-\infty, +\infty],$$

and a feasible policy of least cost is optimal.

Let $\bar y_i$ minimize $G_i$ over $Y_i$. When $\bar y_i$ is not attainable from $x$, the minimal feasible level $w_i(x)$ is the least element of $Y_i \cap \{y : y \ge q_i(x),\ y \ge \bar y_i\}$. The base stock ordering policy orders up to $\bar y_i$ if $q_i(x_i) \le \bar y_i$ and up to $w_i(x_i)$ otherwise.

Formalization targets

The hypotheses are: (3a) $\bar y_i \in Y_i$ minimizes $G_i$ over $Y_i$; (3b) $q_{i+1}(s_i(\bar y_i, t)) \le \bar y_{i+1}$ for $t \in \mathfrak{D}_i$; (3c) $Y_i$ is closed and linearly ordered by $\le$; (3d) $G_i$ and $s_i(\cdot, t)$ are nondecreasing on $\{y \in Y_i : y \ge \bar y_i\}$, and $q_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$.

Goal: Theorem 3.2

Under (3a)–(3d), the base stock ordering policy

$$\bar Y_i^*(H_i^*) = \begin{cases} \bar y_i, & q_i(x_i^*) \le \bar y_i, \\ w_i(x_i^*), & q_i(x_i^*) \not\le \bar y_i \end{cases}$$

is feasible and optimal: $f(x_1 \mid \bar Y^*) \le f(x_1 \mid \bar Y)$ for every feasible $\bar Y$.

Milestones

1. A nonempty, closed, linearly ordered, bounded-below subset of $\mathbb{R}^n$ has a least element (p. 212); hence $w_i(x)$ exists and equals $\bar y_i$ when $q_i(x) \le \bar y_i$.
2. $w_i$ is nondecreasing where $q_i(x) \not\le \bar y_i$ (p. 214).
3. Once $q_k(x_k^*) \le \bar y_k$, the base stock policy orders up to $\bar y_i$ for all $i \ge k$.
4. Theorem 3.1: under (3a) and (3b), if $q_1(x_1) \le \bar y_1$, ordering up to $\bar y_i$ in every period is optimal, with cost $\sum_i \beta_i G_i(\bar y_i)$.
5. The coupling (3.1): before the first period $T$ with $q_T(x_T^*) \le \bar y_T$,

$$\bar y_i < y_i^* = w_i(x_i^*) \le w_i(x_i) \le y_i.$$

6. Pathwise dominance: $G_i(y_i^*) \le G_i(y_i)$ for every $i$ and every possible demand path.
7. The reduction behind (2.3): $E\, W_i(y_i, D_i) = E\, G_i(y_i)$, by independence of $y_i$ and $D_i$.

Significance

The theorem shows that under (3a)–(3d) the infinite-horizon, nonstationary, multi-product problem is solved by one-period optimization: compute $\bar y_i$ from $G_i$ alone, and when it is unreachable order the least feasible amount. No value function is computed. It covers backlogging and lost sales, products stocked in fixed proportions, and time-varying cost and demand data, and Theorem 3.1 alone settles the frequent case in which the initial stock is small.

The result is proved in the paper. To our knowledge it has not been machine-checked: this mission produces a Lean model of a general stochastic, infinite-horizon, multi-product inventory problem (feasible policies, the expected discounted cost with $+\infty$ allowed), and a checked proof that a myopic policy is optimal in it. The model and its cost are reusable for other base stock and myopic optimality results.

Difficulty

The obvious argument would compare the base stock policy with an arbitrary policy period by period using (3a) alone. That fails once $\bar y_i$ is unreachable. The base stock policy then holds less stock than $\bar y_i$ would require, and it has to be shown that no other policy can reach a lower-cost level later. The proof couples the two trajectories along every demand path, using the monotonicity in (3d) and the linear order of $Y_i$ from (3c), until the base stock level becomes attainable, after which (3b) keeps it attainable. The formal difficulties are:

• the existence and monotonicity of the least element $w_i(x)$ in a closed chain of $\mathbb{R}^n$;
• the measurability of the base stock policy, which is part of its feasibility;
• the passage from pathwise dominance to the expected discounted cost when the cost may be $+\infty$.

Formalization scope

Periods are 0-based in Lean (Lean period $k$ is the paper's period $k+1$). Vectors are Fin n → ℝ with the product order; $q_i$ takes values in Fin n → EReal. Policies are functions of the past demands. The paper shows on p. 219 that this loses no generality once $x_1$ is fixed. The cost is excess, a $[0,\infty]$-valued series of lower Lebesgue integrals of $\beta_i(G_i(y_i) - \gamma_i)$, plus the finite real $\sum_i \beta_i\gamma_i$, taken in EReal. A divergent series therefore gives $+\infty$ and never the junk value $0$. "Minimal element" is IsLeast. The $G_i$ in the statements is the integral of $W_i$ built from the data, and the policy in the goal is constructed from $\bar y$, $q$, $w$ and $s$. Neither is an arbitrary object satisfying the conclusion. The goal concludes optimality, which includes feasibility: a pathwise or conditional statement would not be the theorem.

Hypotheses added relative to the page, each used by the paper without being stated:

• Order feasibility: from every $x \in X_i$ some $y \in Y_i$ with $y \ge q_i(x)$ exists (p. 212 asserts the set defining $w_i(x)$ has a minimal element, which needs it nonempty). The least-element lemma likewise assumes $A$ nonempty.
• (3d)'s $q$-clause in one-sided form: if $x \le x'$ in $X_i$ and $q_i(x) \not\le \bar y_i$, then $q_i(x) \le q_i(x')$. This is the form the proof on p. 214 uses; monotonicity on the region $\{q_i(x) \not\le \bar y_i\}$ alone admits a counterexample to Theorem 3.2.
• Integrability of $W_i(y_i, D_i)$ in the milestone $E W_i = E G_i$.
• Borel measurability of $q_i$ on all of $\mathbb{R}^n$ rather than on $X_i$ (a harmless strengthening).

A complete development needs: least elements of closed chains in $\mathbb{R}^n$; measurability of the least-element selection $x \mapsto w_i(x)$; a Fubini/independence argument for $E\,W_i(y_i,D_i)=E\,G_i(y_i)$; and monotone summation of lower integrals. The least-element lemma and the cost encoding are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments.

Selected references

• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• R. Bellman, I. Glicksberg, O. Gross, On the Optimal Inventory Equation, Management Science 2(1):83–104, 1955. https://doi.org/10.1287/mnsc.2.1.83
• S. Karlin, Dynamic Inventory Policy with Varying Stochastic Demands, Management Science 6(3):231–258, 1960. https://doi.org/10.1287/mnsc.6.3.231

Motivation

Mission IX (09-proportional-fairness-core) formalized proportional fairness (PF) as a control policy and proved the technical core of its stability theory: under a load condition, the PF fluid model is stable (Theorem 10.5), via an entropy Lyapunov function that is genuinely not Lipschitz continuous — a departure from every other stability argument in J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org). A stability theorem for one fixed arrival-rate vector is, on its own, a narrower claim than practitioners actually want: real systems see load that changes over time, and a control policy worth adopting should not need re-tuning every time the mix of traffic shifts. This mission completes Theorem 10.5's proof and turns it into exactly that stronger guarantee — proportional fairness is maximally stable: stable throughout the entire region where any policy could be stable, without knowing the arrival rates in advance — and specializes the result to two concrete network families, bandwidth-sharing networks and queueing networks under head-of-line proportional processor sharing (HLPPS), that were already familiar from earlier in the book under different control policies.

Setting

Fix a unitary network operating under PF control with mean service times $m > 0$, routing matrix $P$, a partition of job classes into demand groups $\{\mathcal I(\ell), \ell \in \mathcal L\}$, and a reduced allocation set $\tilde{\mathcal A} \subset \mathbb R^{\mathcal L}_+$ (all restated from mission IX, Definition 10.3). The entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38, mission IX) admits an alternative decomposition $\varphi = \sum_\ell \varphi_\ell$ in terms of the within-group entropy term

$$f(t) := \sum_{\ell\in\mathcal L}\sum_{i\in\mathcal I(\ell)} Z_i(t)\log\!\left(\frac{Z_i(t)}{Y_\ell(t)}\right), \qquad Y(t) := GZ(t) \quad \text{(Eq. 10.50)},$$

with the convention that the term for class $i$ is $0$ when $Z_i(t)=0$. Here $D^+$/$D^-$ denote the upper-right/upper-left Dini derivatives (Appendix A.4, Eqs. A.9-A.10): at a point where the ordinary derivative may not exist, these one-sided $\limsup$s still let a Lyapunov-drift argument go through. A control policy is maximally stable (Section 5.7) for a network if its implementation does not depend on the arrival-rate vector $\lambda$ and it is stable for every $\lambda$ in the network's stability region $\Lambda^*$ — the largest region any policy could possibly stabilize.

Formalization targets

Goal: Corollary 10.16 — maximal stability of PF control for a unitary network

$$\text{IsMaximallyStable}\Big(\lambda \mapsto \text{PFFluidStable}(\lambda, m, P, \mathrm{grp}, \tilde{\mathcal A})\Big)$$

for the single PF policy value (its implementation never depends on $\lambda$). This is the applied payoff of Theorem 10.5 (mission IX): combined with Theorem 6.2 (mission III, fluid stability implies SPN stability) and Corollary 5.6 (mission II, a $\lambda$-independent policy stable throughout the subcritical region is automatically maximally stable), it upgrades a single-$\lambda$ stability statement to the strongest form the book's own framework can express.

Supporting milestones

Lemmas 10.11-10.15 supply the remaining technical content of Theorem 10.5's proof that mission IX's own milestones left open: Lemma 10.11 is the uniform negative-drift bound $\sum_i \dot Z_i(t)\log(\dot D_i(t)/\alpha_i) \le -\varepsilon$ at every regular point with $Z(t) \ne 0$; Lemmas 10.12-10.14 establish continuity and two successively sharper Dini-derivative bounds on the within-group entropy term $f$; Lemma 10.15 shows that positivity of the departure rate $\dot D_i(t)$ propagates from occupied classes to every class. Corollaries 10.17 and 10.18 specialize the goal to bandwidth-sharing networks and to HLPPS-controlled queueing networks, respectively.

Significance

The result itself. A stability theorem tied to one fixed $\lambda$ is of limited practical use: it would need to be re-verified every time the arrival-rate vector changes, which real traffic does constantly. Maximal stability removes that dependency entirely — a single policy, implemented without any knowledge of $\lambda$, is guaranteed stable throughout the full region any control could stabilize. Corollaries 10.17 and 10.18 make this concrete for two network families with independent histories in the literature: bandwidth-sharing networks (the original motivation for proportional fairness, Kelly 1997) and queueing networks under HLPPS, connecting PF's static, utility-theoretic motivation to a scheduling rule that predates it.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=maximal%20stability, q=bandwidth%20sharing) finds no relevant hits on the platform. This mission formalizes the remaining entropy-Lyapunov lemmas, the within-group entropy term, the BWS and HLPPS network models (restated locally, since no other drafted chunk covers Sections 4.5-4.6), and the maximal-stability predicate, reusing only Mathlib's general real-analysis substrate (Dini derivatives via Filter.limsup) and definitions restated from missions II, III, V, and IX under this series' restate-not-import convention for concurrently-drafted chunks.

Difficulty

The obvious approach to Corollary 10.16 — restate "maximally stable" with an explicit $\lambda$-dependent policy family and add "the policy doesn't actually depend on $\lambda$" as a side hypothesis — obscures the point: a policy that is definitionally independent of $\lambda$ is a stronger and cleaner claim than one that happens to satisfy an extra equation. This formalization instead instantiates the abstract policy type at Unit, so $\lambda$-independence holds by construction rather than as a hypothesis to verify, matching the book's own reading of Section 5.7's definition. A second difficulty is Lemma 10.13's Dini-derivative inequality (Eq. 10.56): the plain-text extraction of this display equation loses bracket and subscript structure that changes its meaning, so the exact grouping was confirmed against the PDF page directly and cross-checked against the book's own re-derivation of the same bracketed expression inside Lemma 10.14's proof. A third is Corollary 10.17's proof, which genuinely depends on three facts outside this chunk's own chapter portion (Proposition 4.4 and the Section 4.4 model translation, Proposition 5.1, Theorem 5.2); rather than silently assuming them or re-deriving their proofs from scratch, they are stated as explicit hypotheses of the milestone itself, so the item's actual content — deriving the two-sided conclusion — is exactly what remains to be proved.

Formalization scope

RestatedCore, RestatedFluidModel, and the maximal-stability predicate MaximalStability are restated verbatim (or, for MaximalStability, in shape) from missions IX, III/V, and II respectively, since concurrently-drafted chunks in this series do not import one another's Lean files even when they share a sub-namespace. New to this chunk: diniUpperLeft (Eq. A.10, needed alongside mission IX's diniUpperRight for Lemma 10.13's two-sided bound), the within-group entropy term withinGroupEntropy (Eq. 10.50, deliberately not named f, since the book's own f already denotes the unrelated PF optimization objective of Eq. 10.2 within the same chapter), and BWSNetworkData/QueueingNetworkDataHL/HLPPSFluidStable (Sections 4.5-4.6, restated locally since no drafted chunk's BRIEF.md covers them). The formalization does not admit a trivializing reading: IsMaximallyStable is instantiated with the genuine, non-vacuous predicate PFFluidStable/HLPPSFluidStable — the same predicate whose stability Theorem 10.5 (mission IX) already establishes on the load-condition region — never with a policy type or stability predicate engineered to make the maximal-stability claim vacuous. Contributions completing the eight by sorry proofs are welcome, particularly Lemma 10.13's Dini-derivative estimate (Section B.4's preliminary results) and Lemma 10.15's connectivity argument (Appendix B.9/B.17).

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, "Charging and rate control for elastic traffic," European Transactions on Telecommunications 8 (1997), 33–37.
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.

Motivation

Dynamic pricing under limited inventory is a core problem of revenue management: a seller holds $C_0$ units of a perishable product (airline seats, hotel rooms, seasonal goods) and must choose prices over a finite selling horizon while demand is random and responds to price. The exactly optimal policy solves a stochastic dynamic program whose state is the remaining inventory, and it changes the price after every sale. In practice sellers often prefer a simpler rule, fixed in advance: solve the deterministic version of the problem, in which random demand is replaced by its mean, and charge the resulting prices whatever happens.

Gallego and van Ryzin (Management Science 1994) showed that in continuous time with Poisson demand this fixed-price heuristic is asymptotically optimal, and bounded its relative loss by the coefficient of variation of demand. Bitran and Caldentey's survey (MSOM 2003, §3.2.1) extends this bound to a discrete-time, periodic-review model with general demand distributions, as Proposition 8, proved in the paper's Appendix. The proof combines three ingredients: a Lagrangian duality argument showing that the deterministic problem is an upper bound on the optimal expected revenue, a sample-path comparison of lost sales, and a distribution-free moment bound of Gallego (1992) on $E[(X-C)^+]$.

Setting

A single product is sold over $N \ge 1$ periods $n = 1, \dots, N$ starting from inventory $C_0$. In period $n$ the seller charges a price $p \ge 0$, and the demand $D_n(p)$ is a nonnegative random variable with finite mean $E[D_n(p)]$, whose law may depend on $n$ and $p$ arbitrarily. With inventory $C$ the seller sells $\min\{D, C\}$ units; unmet demand is lost.

The optimal expected revenue $V_1(C_0)$ is defined by the Bellman recursion $V_{N+1} \equiv 0$,

$$V_n(C) = \sup_{p \ge 0} E\big[p\min\{D_n(p), C\} + V_{n+1}\big(C - \min\{D_n(p), C\}\big)\big].$$

The deterministic problem (32)–(33) is

$$V_1^{\det}(C_0) = \sup_{p \in [0,\infty)^N} \sum_{n=1}^N p_n E[D_n(p_n)] \quad \text{subject to} \quad \sum_{n=1}^N E[D_n(p_n)] \le C_0,$$

and $p^{\det}$ denotes an optimal solution. The deterministic-price heuristic charges $p^{\det}_n$ in period $n$ regardless of sales. Its period demands $D_n(p_n^{\det})$ are independent, $\mathscr{D}_n^{\det} = \sum_{i=1}^n D_i(p_i^{\det})$ is the cumulative demand, and its expected revenue is

$$V_1(p^{\det}, C_0) = \sum_{n=1}^N p_n^{\det} E\Big[D_n(p_n^{\det}) - \big(D_n(p_n^{\det}) - (C_0 - \mathscr{D}_{n-1}^{\det})^+\big)^+\Big].$$

With $\sigma_n^2 = \operatorname{Var}(\mathscr{D}_n^{\det})$, eq. (34) defines

$$\eta_n^{\det}(C_0) = \frac{\sqrt{\sigma_n^2 + (C_0 - E[\mathscr{D}_n^{\det}])^2} - (C_0 - E[\mathscr{D}_n^{\det}])}{2},$$

and $\nu(C_0) = \sigma_N / E[\mathscr{D}_N^{\det}]$ is the coefficient of variation of the total demand.

Formalization targets

Goal: Proposition 8, eq. (35)

Assume that $p \mapsto p\,E[D_n(p)]$ is concave and $p \mapsto E[D_n(p)]$ is convex on $[0,\infty)$ for each $n$, that some price $p^\infty \ge 0$ has $\sum_n E[D_n(p^\infty)] < C_0$, and that $p^{\det}$ is optimal for (32)–(33). Then

$$1 \ge \frac{V_1(p^{\det}, C_0)}{V_1(C_0)} \ge \frac{1}{V_1^{\det}(C_0)} \sum_{n=1}^N p_n^{\det} E[D_n(p_n^{\det})]\left(1 - \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}\right) \ge 1 - \max_n \frac{\eta_n^{\det}(C_0)}{E[D_n(p_n^{\det})]}.$$

The constants are the paper's, and the goal is the full chain.

Milestones

1. Gallego's bound (Appendix, (*)): for square-integrable $X$, $E[(X - C)^+] \le \frac12\big(\sqrt{\operatorname{Var}X + (C - EX)^2} - (C - EX)\big)$, which is at most $\frac12\sqrt{\operatorname{Var} X}$ when $EX \le C$.
2. Eq. (24): in one period, $E[p\min\{D(p), C\}] \le p\min\{E[D(p)], C\}$, so $V(C) \le V^{\det}(C)$.
3. Proposition 6, eq. (26): in one period, $V(C, p^{\det})/V(C) \ge 1 - \nu^{\det}/2$.
4. $V_1^{\det}$ is concave in the capacity (first sentence of the Appendix proof).
5. Proposition 8, first assertion: $V_1(C_0) \le V_1^{\det}(C_0)$.
6. The Appendix display bounding $V_1(p^{\det}, C_0)$ below by $\sum_n p_n^{\det}E[D_n](1 - E[(\mathscr{D}_n^{\det} - C_0)^+]/E[D_n])$.
7. Eq. (36), after the goal: if $E[D_n(p)] = T_n\lambda(p)$, one constant price solves (32)–(33) and $1 \ge V_1(p^{\det},C_0)/V_1(C_0) \ge 1 - \nu(C_0)/2$.

Significance

The result gives a guarantee for a pricing policy that needs no inventory tracking: its relative loss is controlled by the first two moments of cumulative demand, with no distributional assumption beyond finite variance. When demand grows while its coefficient of variation shrinks, as for sums of independent period demands, the guarantee tends to one, which is the discrete-time form of asymptotic optimality of fixed prices. The upper bound $V_1 \le V_1^{\det}$ is used throughout revenue management as the benchmark for heuristics (fluid or deterministic LP bounds).

The paper's proof is complete in the Appendix, and the mathematics is not in question beyond minor typos. None of it is machine-checked. A formal development adds a checked Bellman model of periodic-review pricing with general demand laws, a checked fluid upper bound for it, and a checked form of Gallego's moment bound, all reusable for other revenue-management statements. A related platform theorem, RevenueManagement.deterministic_upper_bound (mission The Theory and Practice of Revenue Management III), states the deterministic bound for a Bernoulli-arrival model with at most one sale per period; the model here is different (arbitrary demand laws, continuous inventory), and neither statement implies the other.

Difficulty

The upper bound $V_1(C_0) \le V_1^{\det}(C_0)$ is the hard part. The natural induction replaces $V_2$ by $V_2^{\det}$ and applies Jensen's inequality, but $V_2^{\det}(C)$ is $-\infty$ at capacities where the remaining deterministic problem is infeasible, while $V_2(C)$ stays nonnegative. The induction therefore fails as stated when mean demand never vanishes. The paper's argument also passes through the Lagrangian dual of (32)–(33), and strong duality for that program on $[0,\infty)^N$ under the Slater point $p^\infty$ is not available in Mathlib in this form.

The lower bound is less deep but technical: it needs the product law of the period demands, linearity of expectation for truncated sums, and variances of partial sums. Gallego's inequality is elementary once the right quadratic bound on $(x - C)^+$ is found, but it is not in Mathlib.

Formalization scope

• Periods are Fin N, 0-based. Demand laws are μ n p : Measure ℝ, probability measures carried by $[0,\infty)$ with finite mean, required at every price (laws at negative prices never enter a statement).
• The Bellman value is computed in $[0,\infty]$ with the lower Lebesgue integral and ⨆ over $p \ge 0$, so no supremum takes a junk value; the paper's $V_n$ is valueToGo M (N - n + 1). Ratios use its real value.
• $V_1^{\det}$ is an EReal supremum over the feasible set ($-\infty$ if infeasible). In the goal $p^{\det}$ is an optimal solution, so $V_1^{\det}(C_0)$ is its objective value.
• The heuristic's demands are independent: the joint law is the product measure.
• Implicit hypotheses made explicit: "concave objective and convex feasible region" is read as concavity of $p\,E[D_n(p)]$ and convexity of $E[D_n(p)]$ on $[0,\infty)$, the latter making (33) convex for every capacity; existence of the optimal deterministic solution; finite variance and positive mean of each $D_n(p_n^{\det})$; and $V_1^{\det}(C_0) > 0$, without which the ratios are $0/0$.
• The typo $\mathscr{D}_n^{\det} := \sum_{i=1}^n D_n(p^{\det})$ on p. 221 is read as $\sum_{i=1}^n D_i(p_i^{\det})$.

Trivializing formalizations ruled out: $V_1$ is defined by the Bellman recursion, not as a supremum over an unspecified policy class or as a variable constrained by hypotheses; $\eta_n^{\det}$ is the expression (34), not a hypothesis-supplied bound on expected overflow; the goal does not assume strong duality or a Lagrange multiplier, since that is the proof's key step; independence is built into the joint law, not assumed as an inequality; variances are taken only under square integrability, since Mathlib's variance is $0$ for infinite variance.

Needed infrastructure: measurability of the Bellman integrand (monotonicity of $V_n$ in inventory), Jensen's inequality for $\min\{\cdot, C\}$ (ConcaveOn.le_map_integral), Lagrangian strong duality for a separable concave program with one convex constraint, marginals and variances of sums under Measure.pi, and Gallego's bound. The duality and moment results are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the upper bound, are welcome.

Selected references

• G. R. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–230, 2003. https://doi.org/10.1287/msom.5.3.203.16061
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11(1):55–60, 1992 (as cited in Bitran and Caldentey 2003).
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993.

Motivation

Multistage stochastic linear programs model decisions taken in periods $t = 1, \dots, T$ while a random vector $\xi_t$ is revealed period by period: production and capacity planning, energy scheduling, asset–liability management. With finitely many scenarios the problem is one very large linear program with a tree structure, and decomposition methods solve it by passing information up and down the scenario tree instead of solving it whole. John R. Birge's Nested Decomposition for Stochastic Programming Algorithm (NDSPA), published in Operations Research in 1985 (DOI), is the multistage extension of the L-shaped method of Van Slyke and Wets (SIAM J. Appl. Math. 1969) and the ancestor of the nested Benders and stochastic dual dynamic programming codes in use today.

The paper reports a practical defect of the method: degeneracy leads to many repeated solutions of the same scenario problem (Remark 4, p. 996–997), an effect Abrahamson (1980) had observed for deterministic nested decomposition. Propositions 3 and 4 (p. 997) identify where the degeneracy comes from: cuts that bind at the ancestor force the descendant problems that produced them into degenerate bases. This mission formalizes those two propositions.

Setting

Fix a node of a finite scenario tree: scenario $j$ at period $t$, with decision $x \in \mathbb{R}^{n}$. Its ancestor's decision $x^{a}$ enters only through the right-hand side of its equality rows. After $r$ feasibility cuts and $s$ optimality cuts have been added, the node solves the scenario problem (7):

$$\min\ c^\top x + \theta \quad\text{s.t.}\quad A x = \xi + B x^{a},\quad D_l^\top x \ge d_l\ (l \le r),\quad E_l^\top x + \theta \ge e_l\ (l \le s),\quad x \ge 0,$$

over $x$ and a free scalar $\theta$, which stands in for the expected future cost. During NDSPA's forward pass the node also carries the restriction $\theta = 0$; a last-period node has no future cost and keeps that restriction.

A descendant problem (period $t+1$, scenario $j' \in J'$) has the same shape, with right-hand side $\xi_{j'} + B_{j'} x$ depending on the node's decision $x$. Two kinds of cut flow from descendants to the node:

• a feasibility cut arises when a descendant is infeasible at some $x^0$: a Farkas certificate $\lambda$ of that infeasibility, with parts $\pi, \rho, \sigma$ on the descendant's rows (7.2), (7.3), (7.4), yields the cut $D^\top x \ge d$ with $D = -\pi^\top B_{j'}$ and $d = \pi^\top \xi_{j'} + \rho^\top d_{j'} + \sigma^\top e_{j'}$;
• an optimality cut is built in NDSPA Step 3a from optimal dual vectors $\lambda_{j'}$ of all descendants at the current $\bar x$ and weights $p_{j'}$: $E = -\sum_{j'} p_{j'} \pi_{j'}^\top B_{j'}$ and $e = \sum_{j'} p_{j'} (\pi_{j'}^\top \xi_{j'} + \rho_{j'}^\top d_{j'} + \sigma_{j'}^\top e_{j'})$. It is added only if it cuts off the current point, the test (9): $\bar\theta < e - E^\top \bar x$.

A cut $E^\top x + \theta \ge e$ is valid when $e - E^\top x$ never exceeds the weighted sum of the descendants' objective values at feasible points, for any $x$. A basic solution of (7) is a point at which all equality rows hold and $n + 1$ linearly independent constraints are active; it is degenerate when more than $n + 1$ constraints are active.

Formalization targets

Goal: Proposition 4

Let two distinct valid optimality cuts $l_1, l_2$ bind at $(\bar x, \bar\theta)$. Let each descendant $j'$ have an optimal basic feasible solution $z_{j'}$ and an optimal dual vector $\lambda_{j'}$ at $\bar x$, and suppose the Step 3a cut built from these duals fails (9), so that $\bar\theta \ge e - E^\top \bar x$. Then

$$\exists\, j' \in J' : \ z_{j'} \text{ is a degenerate basic solution of the problem (7) of } j' \text{ at } \bar x .$$

Milestone: Proposition 3

If descendant $j'$ generates feasibility cut $l'$ of the node and that cut binds at $\bar x$, then

$$\text{every basic feasible solution of the problem (7) of } j' \text{ with } \bar x \text{ in (7.2) is degenerate.}$$

Significance

The result. The two propositions explain a failure mode that every nested-decomposition implementation meets. The backward pass of NDSPA stalls, adding no cut, at exactly the points where Proposition 4 applies, and the degenerate descendant bases it predicts are what make the same ancestor basis recur over many iterations. The analysis motivated the partitioning method of Section 3 of the paper and the intermediate problem of Birge (1980), and it is the reason later codes pay attention to the choice among multiple optimal duals.

Formalizing it. The paper states both propositions without proof and refers the proofs to Birge (1980), an unpublished technical report. A machine-checked proof makes the statements self-contained. It also pins down what they assume: which cuts are meant, which invariants of the algorithm they rely on, and which notion of degeneracy applies to a problem with a free variable and inequality cuts. The definition layer (scenario problems with their cut families, LP duals, Farkas certificates, the Step 3a cut) is reusable for any statement about nested Benders or L-shaped methods. The finite convergence of the nested method is the subject of a separate private formalization (Birge and Louveaux, Ch. 6, Thm. 1, StochasticProg.Multistage.thm1_finite_convergence), so this mission does not restate NDSPA's convergence.

Difficulty

The statements connect the geometry of the ancestor's value function to the combinatorics of descendant bases. For Proposition 4 the difficulty is that nothing in the hypotheses mentions the descendants' bases directly: they speak of two cuts at the ancestor and one failed test. The conclusion is a statement about the descendants' simplex bases, so the ancestor-level information has to be transported down to the descendant problems, where the relevant objects (optimal bases, optimal duals, optimal-value functions of the right-hand side) are not unique in exactly the degenerate case the proposition is about. Two hypotheses that look dispensable are not. Without distinctness a duplicated cut gives a counterexample. Without validity a cut that is not a lower bound can bind anywhere. For Proposition 3 the certificate must be the one that generated the cut; an arbitrary cut row that happens to bind says nothing about the descendant.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the variable of (7) is $z = (x, \theta) \in$ Fin (n+1) → ℝ with $\theta$ its last coordinate. The paper suppresses transposes; here they are explicit, and a row vector times a matrix ($\pi B$) is vecMul. Basic, basic feasible and degenerate solutions are the general-form notions of Bertsimas and Tsitsiklis (Defs. 2.9–2.10), reused from the public definition BasicSolution, applied to the whole constraint family of (7), the free $\theta$ included. A last-period node is represented with the restriction $\theta = 0$, which pairs one extra variable with one extra active equality and so preserves basicness and degeneracy.

Readings of informal words, each stated in the items:

• "generate a feasibility constraint": the Van Slyke–Wets construction from a Farkas certificate at an earlier input $x^0$, stated against the descendant's current constraint family;
• "binding for some solution": the row holds with equality at the point; feasibility or optimality of the point for the ancestor is not assumed, which strengthens both statements;
• "two constraints of type (7.4)": two distinct cuts, both valid, the invariants NDSPA maintains;
• "every set of optimal solutions … that produces $E$ and $e$": one optimal basic feasible solution and one optimal dual vector per descendant, the cut computed from those duals;
• "degenerate": general-form degeneracy, not the standard-form count of zero components.

Correction to the page. Step 3a prints $E = -\sum \pi B_t$ and $e = \sum \pi \xi$. The formalization completes $e$ with the terms $\rho^\top d + \sigma^\top e$ from the descendants' own cuts, without which the cut is not a valid lower bound when the descendants carry cuts. It also adds weights $p_{j'} > 0$; conditional probabilities are a special case, and $p \equiv 1$ is the printed sum. The data $A$, $B$ may differ between descendants, which is more general than the paper.

Proposition 3 is vacuous when the descendant is infeasible at $\bar x$; that is the paper's statement. No trivializing reading is available for the goal: the cuts are computed from certificates and duals inside the statement, never taken as arbitrary vectors, and a sorry-free local check confirms that all hypotheses of Proposition 4 hold together on a small instance. Propositions 1 and 2, NDSPA's convergence, the partitioning method of Section 3 and the computational study are out of scope. Contributions welcome: proofs of Propositions 3 and 4, and supporting lemmas on LP duality and basis stability over general-form constraint families.

Selected references

• J. R. Birge, Decomposition and Partitioning Methods for Multistage Stochastic Linear Programs, Operations Research 33(5):989–1005, 1985. https://doi.org/10.1287/opre.33.5.989
• R. M. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM J. Appl. Math. 17(4):638–663, 1969. https://doi.org/10.1137/0117061
• J. R. Birge, Solution Methods for Stochastic Dynamic Linear Programs, Technical Report SOL 80-29, Stanford University, 1980.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Defs. 2.9–2.10).
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011 (nested L-shaped method for multistage problems). https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$, the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$. When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$, a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ($\varphi$) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$, $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$, which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$, not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
• R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

Motivation

A two-sided market in which each participant trades with at most one partner on the other side — houses and buyers, workers and firms, producers and consumers under exclusive bilateral contracts — is the setting of L. S. Shapley and M. Shubik's assignment game (Int. J. Game Theory 1 (1971) 111–130). Money is transferable, so the natural solution concept is cooperative: a division of the total gain that no coalition of traders can improve upon. The question the paper answers first is whether such a division exists and how to find it, given that a market with $m$ sellers and $n$ buyers has $2^{m+n}$ coalitions.

The answer, Theorem 2 of the paper, connects the core of the game with the dual of the linear-programming relaxation of the optimal assignment problem. It is the starting point of the literature on two-sided matching markets with transfers: the lattice structure of the core (Theorem 3 of the same paper), the ascending auctions of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the equivalence of core outcomes with competitive equilibrium prices. The same LP pairing reappears in stable matching with transfers and in the VCG analysis of multi-item auctions with unit demand.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers; either may be empty and their sizes need not agree. A matrix $a = (a_{ij})_{i \in M, j\in N}$ of nonnegative reals records the profit $a_{ij} \ge 0$ that the partnership of seller $i$ and buyer $j$ can realise (in the real-estate reading, $a_{ij} = \max(0, h_{ij} - c_i)$ with $h_{ij}$ buyer $j$'s valuation of house $i$ and $c_i$ its owner's reservation value).

A coalition $S \subseteq M \cup N$ is described by its sellers $A = S\cap M$ and buyers $B = S \cap N$. A matching inside $(A, B)$ is a set of seller–buyer pairs from $A \times B$ in which no player appears twice. The characteristic function (2.6) assigns to $S$ its worth

$$v(S) = \max_{P} \sum_{(i,j) \in P} a_{ij},$$

the maximum over matchings $P$ inside $S$. One-sided coalitions and singletons are worth $0$.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb R^M$, $v \in \mathbb R^N$ (the paper uses $v$ both for the characteristic function and for buyers' payoffs; the formal development calls the former worth). The core is the set of payoff vectors with

$$\sum_{i\in M} u_i + \sum_{j \in N} v_j = v(M \cup N) \quad (3.5), \qquad \sum_{i\in S\cap M} u_i + \sum_{j \in S\cap N} v_j \ge v(S)\ \text{ for all } S \quad (3.6).$$

The assignment LP (3.1)–(3.2) maximises $z = \sum_{i,j} a_{ij} x_{ij}$ over $x_{ij} \ge 0$ with $\sum_{i} x_{ij} \le 1$ for each $j$ and $\sum_j x_{ij} \le 1$ for each $i$. Its dual (3.3)–(3.4) minimises $w = \sum_i u_i + \sum_j v_j$ over $u_i \ge 0$, $v_j \ge 0$ with $u_i + v_j \ge a_{ij}$ for all $i, j$. The optimal values are $z_{\max}$ and $w_{\min}$.

Formalization targets

Goal: Theorem 2 (p. 118)

$$\operatorname{core}(a) = \{(u,v) : (u,v) \text{ is an optimal solution of the dual LP (3.3)–(3.4)}\}.$$

The statement holds for every finite $M$, $N$ and every $a \ge 0$, with no constants to fix.

Milestones, in the order the paper's argument uses them

1. Eq. (3.6), p. 118: every dual-feasible $(u, v)$ gives every coalition at least its worth.
2. Sec. 3.1, p. 117 (quoting Dantzig, p. 318): the assignment LP attains its maximum at a $0/1$ point, and $z_{\max} = v(M \cup N)$.
3. Sec. 3.1, p. 118 (quoting Dantzig, p. 129): both LPs have optima and $w_{\min} = z_{\max}$.
4. Eq. (3.5), p. 118: every dual minimiser satisfies $\sum_i u_i + \sum_j v_j = v(M \cup N)$.

Further results on the same definitions

• Sec. 3.2, p. 118: the core is nonempty.
• Sec. 3.2, p. 119: for $(u,v)$ in the core, $v_j = \max\bigl(0, \max_{i}(a_{ij} - u_i)\bigr)$ for every buyer $j$ — at the seller prices $p_i = c_i + u_i$, buyer $j$'s best net gain is exactly $v_j$.

Significance

Theorem 2 replaces the $2^{m+n}$ coalition constraints of the core with the $mn$ constraints of a linear program. Consequences stated in the paper: the core is never empty; its points are exactly the dual optimal solutions, so the core is a polytope computable by linear programming without evaluating the worth of any coalition other than the grand one; and dual variables are prices — a seller's core payoff determines a price at which every buyer's best purchase yields that buyer's core payoff. The lattice and corner results of Sec. 3.3 build on this identification.

The paper's proof is short but leans on two results quoted from Dantzig's Linear Programming and Extensions: the integrality of the rectangular assignment polytope and the LP duality theorem. A formalization makes these dependencies explicit for the inequality-constrained rectangular case with possibly unequal sides. To our knowledge Theorem 2 has no machine-checked proof. On Prove2Me, general LP strong duality is formalized (LinearOptimization.lp_strong_duality, SmaleNinth.lp_strong_duality), and integrality of the square doubly stochastic assignment LP (UnderstandingML.assignment_lp_integral, FamousTheorems.birkhoff_von_neumann); neither is the specialised statement here, but both are natural substrate.

Difficulty

The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth $v(M \cup N)$, which is not a statement about linear programming alone: it needs both LP duality and the integrality of the assignment polytope. The integrality needed is for the polytope cut out by inequalities $\le 1$ on a possibly non-square matrix, which is not the Birkhoff polytope of doubly stochastic matrices already on the platform; the gap between the two must be bridged.

The converse, "core ⊆ dual optimal", is dismissed as "clearly" in the paper, but the core is defined through the worth of every coalition, a maximum over exponentially many matchings, while dual optimality is a comparison with every dual-feasible vector. Neither side mentions the other's objects, and the naive reading "the core is the dual feasible set" is false: large payoffs are dual feasible and violate (3.5).

Formalization scope

Lean represents sellers and buyers as types M, N with [Fintype M] [Fintype N]; no nonemptiness is assumed, so markets with an empty side are included (there the core is $\{0\}$). The matrix is a : M → N → ℝ with the standing hypothesis ∀ i j, 0 ≤ a i j on every theorem. A coalition is a pair (A, B) : Finset M × Finset N. A matching is a Finset (M × N) inside A ×ˢ B with no repeated seller and no repeated buyer. The worth is Finset.sup' over the finite, nonempty set of matchings (the empty matching is always present), so there is no junk value. The paper's (2.6) takes exactly $k = \min(|S\cap M|, |S\cap N|)$ pairs; the formal definition takes all partial matchings, which gives the same maximum because $a \ge 0$.

Payoff vectors are pairs (M → ℝ) × (N → ℝ). The core is defined by (3.5) and (3.6) for all coalitions; nonnegativity is not a separate clause since it follows from singleton coalitions. The dual LP keeps the nonnegativity of $u$ and $v$ that (3.3) imposes, and "solutions of the LP dual" is read as optimal solutions (DualOptimal: dual feasible and of minimal objective among dual-feasible vectors), as the text preceding Theorem 2 does.

The worth is the combinatorial maximum, not the LP value, and the core is defined by coalitions, not through the dual; defining either through the other would make Theorem 2 true by unfolding, and such a formalization is ruled out. Likewise the goal is not the weaker "core = dual feasible set", which is false.

Contributions welcome: integrality of the rectangular inequality-form assignment polytope, a specialisation of general LP duality to this pair, and the coalitional inequality (3.6). The first two are reusable for any bipartite matching model.

Selected references

• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9 (1962), 45–48. https://doi.org/10.1002/nav.3800090106
• G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393

Motivation

Every stability result up through mission VII proves that a particular control policy — a fixed priority list, HLSPS, a policy tailored to one network's topology — keeps a specific processing network stable throughout its subcritical region. None of them answer a more practical question a system designer actually faces: given an arbitrary Leontief network (one where every activity has a well-defined, unique buffer it draws from), is there a single control rule, computable from the network's data alone with no bespoke analysis, that is guaranteed stable whenever stability is possible at all? J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) answers this in Chapter 9 with the back-pressure (equivalently, in the single-hop case, max-weight) control policy: at every decision time, choose the allocation of service effort that maximizes a bilinear "weighted throughput" objective built directly from current buffer contents. This mission formalizes the policy, the characteristic fluid equation it induces, and the resulting maximal-stability theorem — the chapter's central result and one of the most cited scheduling policies in the queueing-networks literature.

Setting

A Leontief network (Definition 9.5) is an SPN whose input-output matrix $R$ satisfies two assumptions: Assumption 9.1, that each activity has a unique buffer it draws material from (so $i(j)$, the buffer served by activity $j$, is well-defined), and Assumption 9.2, that there is a nonnegative activity-level vector driving every buffer's net output rate strictly positive — the structural condition under which the network can be drained at all. The back-pressure (or, in the single-server, single-hop case, max-weight) control policy chooses, at each decision time, the feasible allocation $\beta$ of service rates that maximizes the bilinear objective $p(\beta, \hat z) = \hat z \cdot R\beta$, where $\hat z$ is the current vector of buffer contents. The "relaxed" version of the policy allows $\beta$ to range continuously over the allocation polytope $\mathcal A = \{\beta \in \mathbb R^J_+ : A\beta \le b\}$; the "basic" version restricts to integer service-initiation decisions in a genuine SPN with discrete jobs. A network's static planning problem's optimal value $\gamma^* < 1$ is the subcriticality condition throughout this chapter, exactly as in missions II, III, and V.

Formalization targets

Goal: Theorem 9.12 — maximal stability of relaxed back-pressure

Consider a Leontief network operating under the relaxed back-pressure control policy. If the static planning problem has optimal objective value $\gamma^* < 1$, then the corresponding fluid limit is stable, and hence, by Theorem 6.2 (mission III), the network's ambient Markov chain is positive recurrent. This is the chapter's payoff: back-pressure control needs no network-specific tuning — it stabilizes every Leontief network throughout its entire subcritical region, the same universal guarantee mission VI showed only for feedforward networks and HLSPS control specifically.

Supporting milestones

Lemma 9.3 and Proposition 9.4 develop the linear-algebraic machinery of basis matrices: any feasible material-balance vector can be re-expressed using only $I$ "basic" activities (Lemma 9.3), and Assumption 9.2 holds if and only if some basis's associated matrix has spectral radius below one (Proposition 9.4) — the practical, checkable criterion for the network being well-posed at all. Proposition 9.6 shows the back-pressure optimization problem always admits a solution among the finitely many extreme allocations, licensing Remark 9.7's standing convention of restricting attention to that finite set. Lemma 9.10 shows a $z$-maximal extreme allocation can always be chosen to idle any activity whose buffer is currently empty — a fact that looks obvious but genuinely needs proof, because at the fluid level an activity can serve an instantaneously empty buffer at a positive rate (Section 9.5's tandem-model illustration). Theorem 9.8 is the chapter's characteristic fluid equation: under relaxed back-pressure control, the realized fluid service-rate derivative always achieves the bilinear maximum over the allocation polytope, at every regular point. Lemma 9.11 derives this from the raw ("pre-limit") stochastic dynamics — a strictly dominated allocation accrues no processing time — via a genuine limit-passage argument. Theorem 9.13 and Lemma 9.14 extend the maximal-stability guarantee from the relaxed policy to the basic (discrete-decision) policy, under the extra restriction that each server pool is a single server acting alone; this needs a residual-time strong law of large numbers (Lemma 9.14) to show that a server's decision to switch away from a dominated allocation happens quickly enough, relative to elapsed time, that the fluid limit is unaffected.

Significance

The result itself. Theorem 9.12 is the book's formalization of the max-weight/back-pressure maximal-stability theorem originally due to Tassiulas and Ephremides (1992) for multi-hop packet radio networks, later popularized under the "back-pressure" name by Tassiulas (1995) and extended substantially by Dai and Lin (2005), on whose work this chapter is explicitly based. Unlike every policy considered in missions IV, VI, and VII, back-pressure requires no topology-specific insight to design or verify — it is defined uniformly from $B$, $\Gamma$, $A$, and current buffer contents, and Theorem 9.12 certifies it stable for every Leontief network in its subcritical region. This universality is precisely what distinguishes it from HLSPS (mission VI), which needs the network to be feedforward or the policy to be head-of-the-line proportional-sampling before the same guarantee holds.

Formalizing it. A live prior-art check (GET /theorems?q=max-weight%20scheduling, q=back-pressure) returns no hits, so this mission formalizes the policy, its characteristic fluid equation, and both stability theorems entirely from scratch. SPNPlanningData, the input-output matrix R, and the static planning problem are restated from mission II's own apparatus; RegularPoint is restated from mission V's Definition 8.7.

Difficulty

The chapter's central subtlety is that "operating under back-pressure control" cannot be stated directly as a hypothesis on the fluid-limit path $(\hat D,\hat F,\hat T,\hat Z)$ itself: the policy is defined in terms of the discrete, pre-limit decision process, and its fluid-level consequence — the characteristic equation (9.22) — is a genuine theorem (9.8), not a restatement of the policy's definition. Formalizing Theorem 9.8 naively by hypothesizing "$\hat T$ satisfies (9.22)" would make Lemma 9.11 (whose conclusion (9.28)-(9.31) is what Theorem 9.8's own proof literally invokes) circular relative to it. This mission instead hypothesizes Lemma 9.11's raw, pre-limit optimality condition (hYopt: a strictly dominated allocation accrues no processing time over any interval where domination persists) as the operational meaning of "following the back-pressure rule," and derives (9.28)-(9.31) from it as Lemma 9.11's genuine conclusion — Fed into Theorem 9.8 exactly as the book's own proof does ("By Lemma 9.11 and the fact that $\sum_\beta \dot{\hat Y}_\beta(t) = 1$..."). A second difficulty is Theorem 9.13's genuinely distinct proof from Theorem 9.12's: the basic (discrete) policy's fluid limit satisfying the same characteristic equation is not automatic, and needs the residual-time SLLN of Lemma 9.14 plus two extra structural hypotheses (each server pool is a single server, each activity uses exactly one server) that go beyond "basic vs. relaxed" and are stated explicitly rather than folded silently into the policy's name.

Formalization scope

SPNPlanningData, its input-output matrix R, and the static planning problem (SPPFeasible, IsOptimalSPPValue) are restated unmodified from mission II's own apparatus (drafts in this series do not import one another); RegularPoint is restated unmodified from mission V's Definition 8.7. "Basis" is named ActivityBasis, not Basis, to avoid colliding with Mathlib's vector-space Basis type — a deliberate departure from the book's own overloaded terminology, which its own text flags as "slightly narrower than [the] standard meaning in linear programming theory." ExtremeAllocations reuses Mathlib's Set.extremePoints directly rather than restating extreme-point theory from scratch, and Proposition 9.4's spectral-radius condition reuses Mathlib's own spectralRadius (Mathlib.Analysis.Normed.Algebra.Spectrum) rather than defining eigenvalues by hand. IsZMaximal (Definition 9.9) is phrased as "feasible and dominates every feasible alternative" rather than via an explicit sSup/⨆ expression, which sidesteps any Mathlib junk-value risk while remaining definitionally equivalent to "achieves the maximum" whenever a maximizer exists — the same convention this series has used since mission III. Theorem 9.8's hypothesis that the fluid limit "operates under relaxed back-pressure control" is packaged as Lemma 9.11's own conclusion (hTY/hYmono/hYsum/hYopt), matching the book's proof architecture exactly rather than re-deriving it inline. Theorem 9.13 states its two extra single-server hypotheses (hb1, hA01) explicitly as the mission's own BRIEF.md warns to. Lemma 9.14's condition (9.44) — quoted in the book's preparatory material for Theorem 9.13 rather than in the excerpt originally assembled for this lemma — was located directly in source.txt (p. 178, PDF p. 194) and confirmed verbatim, not reconstructed; its formalization (h944) matches the confirmed text exactly. The one acknowledged source inconsistency, noted by BRIEF.md itself, is that (9.56)'s printed left-hand side reads u_i(s,ω) where the surrounding proof otherwise uses t throughout — treated as a typesetting slip and formalized with t, as the lemma evidently intends. IsFluidModelSolution, IsRelaxedBPFluidSolution, RelaxedBPFluidStable, ActivityBasis, AllocationPolytope, and IsZMaximal are the primary reusable contributions; contributions completing the nine by sorry proofs, especially Lemma 9.11's limit-passage argument and Lemma 9.14's SLLN chain, are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• L. Tassiulas and A. Ephremides, "Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks," IEEE Transactions on Automatic Control 37 (1992), 1936–1948.
• J. G. Dai and W. Lin, "Maximum pressure policies in stochastic processing networks," Operations Research 53 (2005), 197–218.

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$. The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$) needs.

Timeline.

• Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
• Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$. For $X\subseteq\mathbb R^n$, $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$-subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$, the line $x_2=2x_1$ is a $\Lambda$-subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$.

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$-free convex set of $W$ if $S\subseteq W$, $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$. It is maximal if no other $\Lambda$-free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ($W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$. The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$.

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$, a set $S$ is a maximal $\Lambda$-free convex set of $W$ if and only if

$$\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};$$ $$\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};$$ $$\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}$$

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$, $S$ is a maximal $\Lambda$-free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$-subspace and $\dim S=\dim P+\dim L=\dim V$, with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$-subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ($S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$-free), Lemma 17 (projection along a $\Lambda$-subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$.

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$-subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$.

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$, the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$-subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$, and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$, and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

1. Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$. For $W=V=\{0\}$ the only maximal set is $\emptyset$, which satisfies none of the listed cases, so the printed statements are false there.
2. Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$, discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
• L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054