Operations Research

Motivation

A multiple objective program asks to maximize $k$ objectives $f_1(x),\dots,f_k(x)$ simultaneously over a feasible set $S$. There is usually no point that is best in every objective, so the object of interest is the set of nondominated criterion vectors: those that cannot be improved in one objective without being worsened in another. Interactive procedures for multiple criteria decision making work by computing nondominated vectors one at a time, by solving a single-objective scalarization, and presenting them to a decision maker.

A scalarization is useful for this purpose only if it is complete (every nondominated vector is the solution of some instance of it) and sound (every solution is nondominated). The weighted-sum scalarization is sound for positive weights but not complete when the feasible region is nonconvex. R. E. Steuer and E.-U. Choo (Math. Programming 26 (1983) 326–344) built their interactive procedure on weighted Tchebycheff distances to an ideal point, following Bowman (1976) and Choo and Atkins (1983). In §3 they treat finite feasible regions with an augmented metric, which requires choosing a small parameter $\rho>0$. In §4 (pp. 334–336) they show that a lexicographic version of the weighted Tchebycheff program is complete and sound for any feasible region, including nonconvex continuous ones, with no parameter to estimate. This mission formalizes that result, Theorems 4.5 and 4.6.

Setting

Let $Z\subseteq\mathbb R^k$, $k\ge1$, be the set of feasible criterion vectors (the image of $S$ under $f=(f_1,\dots,f_k)$). A vector $z$ dominates $\bar z$ if $z_i\ge\bar z_i$ for all $i$ and $z_i>\bar z_i$ for at least one $i$. The nondominated set $N\subseteq Z$ consists of the $\bar z\in Z$ dominated by no $z\in Z$.

An ideal criterion vector is a $z^*\in\mathbb R^k$ with

$$z^*_i=\max\{z_i\mid z\in Z\}+\varepsilon_i,$$

where $\varepsilon_i\ge0$, and $\varepsilon_i>0$ is required whenever (i) more than one nondominated vector maximizes objective $i$, or (ii) the only nondominated vector maximizing objective $i$ also maximizes another objective. So $z^*$ may touch $Z$ in coordinate $i$ only in a controlled way.

The weight set is the simplex $\bar\Lambda=\{\lambda\in\mathbb R^k\mid\lambda_i\ge0,\ \sum_i\lambda_i=1\}$. For $\lambda\in\bar\Lambda$ the weighted Tchebycheff program minimizes $\alpha$ subject to $\alpha\ge\lambda_i(z^*_i-z_i)$ for all $i$ and $z\in Z$; its value at a fixed $z$ is

$$t_\lambda(z)=\max_{1\le i\le k}\lambda_i(z^*_i-z_i).$$

The lexicographic weighted Tchebycheff program first minimizes $t_\lambda$ over $Z$ and then, among the first-stage minimizers, minimizes $e^{\mathsf T}(z^*-z)=\sum_i(z^*_i-z_i)$. The paper writes it as $\min\{P_1\alpha+P_2e^{\mathsf T}(z^*-z)\}$ with pre-emptive priority factors. Finally, for $\bar z\in\mathbb R^k$ the weights $\bar\lambda$ of eq. (4.3) are $\bar\lambda_i\propto1/(z^*_i-\bar z_i)$, normalized to sum to one, when $\bar z_j\ne z^*_j$ for all $j$. When some $\bar z_j=z^*_j$, $\bar\lambda_i$ is $1$ on the coordinates with $\bar z_i=z^*_i$ and $0$ elsewhere.

Formalization targets

Goal: Theorem 4.6 (p. 336)

For compact $Z$, an ideal vector $z^*$ and $\bar z\in Z$,

$$\bar z\in N\iff\exists\,\lambda\in\bar\Lambda\ \text{such that}\ \bar z\ \text{minimizes the lexicographic weighted Tchebycheff program with weights }\lambda .$$

Milestones

1. Proof of Theorem 4.5 (pp. 335–336). For $\bar z\in N$, $\bar\lambda$ as in (4.3) and $\hat\alpha$ the minimal first-stage value,

$$\bar z\in\Phi(\hat\alpha),\qquad N\cap\Phi(\hat\alpha)=\{\bar z\},\qquad \Phi(\hat\alpha)=\{z\mid z_i\ge z^*_i-\hat\alpha/\bar\lambda_i\ \text{when}\ \bar\lambda_i>0\}.$$

2. Theorem 4.5 (p. 335). For $\bar z\in N$: $\bar\lambda\in\bar\Lambda$, and $\bar z$ is the unique minimizer of the lexicographic program with weights $\bar\lambda$.
3. Remark after Theorem 4.6 (p. 336). For every $\lambda\in\bar\Lambda$ the lexicographic program has a minimizer when $Z$ is compact and nonempty, and every minimizer is nondominated.

The goal is the characterization; Theorem 4.5 is the stronger half with uniqueness and an explicit weight.

Significance

Theorem 4.6 says that, as $\lambda$ ranges over the simplex, the lexicographic weighted Tchebycheff program returns exactly the nondominated set, for any feasible region: no convexity, no finiteness, no polyhedral structure. Theorem 4.5 adds that each nondominated vector is the unique output for a weight vector computable from the vector itself, which is what an interactive procedure needs to sample $N$ reliably. The price, as the paper notes, is two optimization stages instead of one; the gain is that no augmentation parameter $\rho$ must be estimated. The result is a standard entry in the textbook treatment of Tchebycheff scalarizations (Steuer, Multiple Criteria Optimization, 1986; Ehrgott, Multicriteria Optimization, 2005).

The result is proved on paper. To our knowledge no machine-checked version exists in Lean or Mathlib, which has no material on Tchebycheff scalarization of multiple objective programs. The formal statements below also pin down two points the printed text leaves loose: the direction of the priority factors, and a closedness assumption that the proof uses without stating it.

Difficulty

The ⇐ direction and the soundness remark are short: a dominating vector is at least as good in the first stage and strictly better in the second. The work is in Theorem 4.5. The obvious argument is that $\bar z$ is the unique minimizer of the first stage with weights $\bar\lambda$; the paper says so. That is true when $\bar z<z^*$ in every coordinate, but false when $\bar z_j=z^*_j$ for some $j$: then $\bar\lambda=e_j$, and every $z\in Z$ with $z_j=z^*_j$ ties with $\bar z$, dominated vectors included. For example, with $Z=\{(5,3),(5,1),(1,10)\}$ and $z^*=(5,10)$, the vectors $(5,3)$ and $(5,1)$ tie. Only the second stage separates them. Showing that it always selects $\bar z$ requires every tied vector to lie below a nondominated vector attaining $z^*_j$, which by the ideal-vector rule must be $\bar z$. That existence step fails for sets that are not closed.

Formalization scope

Criterion vectors are Fin k → ℝ with [NeZero k] ($k\ge1$); objectives are indexed from $0$. $S$, the objectives $f_i$ and the program's variable $\alpha$ are eliminated: $Z$ is a Set (Fin k → ℝ) and the first-stage value is $t_\lambda(z)$ above (the paper's metric uses $|z^*_i-z_i|$, which agrees with $z^*_i-z_i$ on $Z$). $\bar\Lambda$ is Mathlib's stdSimplex ℝ (Fin k). "Minimizes" is global minimization over $Z$; "uniquely minimizes" means every lexicographic minimizer equals $\bar z$ as a criterion vector.

Conventions and added hypotheses:

• The lexicographic program is encoded as the two-stage minimization IsLexMin. The printed "$P_1<<<P_2$" read literally gives the second stage priority; the paper's text on p. 336 and the goal-programming convention it cites give $\alpha$ priority. The two-stage reading is encoded, and the program is not replaced by a weighted sum $P_1\alpha+P_2e^{\mathsf T}(z^*-z)$ with fixed numbers, which would be the augmented program of §3.
• $Z$ compact is an added hypothesis in Theorem 4.5, in the goal, and in the existence half of milestone 3. The paper assumes only that $S$ is bounded, and its "max" in the ideal vector presupposes attainment. Without closedness the weight (4.3) can fail: for $Z=\{(5,3,0),(0,10,0),(0,0,6)\}\cup\{(5,0,4+t):0\le t<1\}$, $z^*=(5,10,6)$ and $\bar z=(5,3,0)\in N$, the program with $\bar\lambda=(1,0,0)$ has no lexicographic minimizer. Closedness is needed by the theorem itself, not only by this proof: adding the points $(5-s^2,\,3+s,\,0)$, $0<s\le1$, to that $Z$ (still bounded, $\varepsilon=0$ still admissible) leaves $\bar z=(5,3,0)\in N$ a lexicographic minimizer for no $\lambda\in\bar\Lambda$, so Theorems 4.5 and 4.6 are false for a bounded, non-closed $Z$. The ⇐ direction, soundness and milestone 1 hold without compactness and are stated without it.
• The ideal vector keeps the paper's $\varepsilon$-rule exactly. Replacing it with a strictly dominating $z^*$ ($\varepsilon>0$ in every coordinate) would remove the case $\bar z_j=z^*_j$ and weaken both theorems; such a formalization does not count.
• In (4.3) and in $\Phi$, division occurs only where the denominator is nonzero. That $\bar\lambda\in\bar\Lambda$ for $\bar z\in N$ is part of Theorem 4.5's conclusion, not an assumption.
• The paper's sentence "the associated weighted Tchebycheff program has a unique solution" (p. 336) is not formalized, since it fails in the tie described above.

Infrastructure needed: dominance and nondominated sets, the ideal vector, the weighted Tchebycheff value, the weights (4.3), and the lexicographic minimizer, all provided as definitions. Proofs will need existence of minimizers of continuous functions on compact sets and a maximal-element argument in the product order on a compact set. Both are reusable for other multiobjective results. Proofs of any item, and faithful statements of Corollaries 4.1 and 4.4 (polyhedral $S$), are welcome.

Selected references

• R. E. Steuer and E.-U. Choo, An interactive weighted Tchebycheff procedure for multiple objective programming, Mathematical Programming 26 (1983) 326–344. https://doi.org/10.1007/BF02591870
• V. J. Bowman, On the relationship of the Tchebycheff norm and the efficient frontier of multiple-criteria objectives, in: Multiple Criteria Decision Making (Jouy-en-Josas 1975), Lecture Notes in Economics and Mathematical Systems 130, Springer, 1976, 76–86. https://doi.org/10.1007/978-3-642-87563-2_5
• E.-U. Choo and D. R. Atkins, Proper efficiency in nonconvex multicriteria programming, Mathematics of Operations Research 8 (1983) 467–470. https://doi.org/10.1287/moor.8.3.467
• A. M. Geoffrion, Proper efficiency and the theory of vector maximization, Journal of Mathematical Analysis and Applications 22 (1968) 618–630. https://doi.org/10.1016/0022-247X(68)90201-1
• M. Ehrgott, Multicriteria Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/3-540-27659-9

Motivation

Every financial application in the rest of this book — terminal wealth maximization, portfolio choice with consumption, index tracking, hedging — takes as given that the underlying market admits no risk-free profit: an arbitrage opportunity. Ruling this out is not a modeling nicety but a structural necessity, since a market with arbitrage has no sensible notion of a fair price at all. Bäuerle and Rieder's Chapter 3 fixes the discrete- and continuous-time market vocabulary the rest of the book builds on, and proves the one structural fact about no-arbitrage that the later chapters actually invoke: that the whole-horizon, global absence of arbitrage is equivalent to a much simpler one-period condition, checked separately at each stage. This reduction — not the deeper fundamental theorem of asset pricing (existence of an equivalent martingale measure), which the book does not prove in this section — is what turns a statement about strategies over the whole time horizon into something checkable stage by stage, exactly the form needed to embed a no-arbitrage assumption into a dynamic-programming argument.

Setting

An $N$-period financial market with $d$ risky assets consists of a probability space $(\Omega,\mathcal{F},\mathbb{P})$ with filtration $(\mathcal{F}_n)_{n=0}^N$, $\mathcal{F}_0$ trivial; a riskless bond with deterministic interest rate $i_n$ on $[n-1,n)$ (so $S^0_n = S^0_{n-1}(1+i_n)$); and $d$ risky assets with relative price changes $\tilde R_n = (\tilde R^1_n,\dots,\tilde R^d_n)$, $\mathcal{F}_n$-measurable and a.s. strictly positive ($S^k_n = S^k_{n-1}\tilde R^k_n$). A portfolio (trading strategy) is an $(\mathcal{F}_n)$-adapted process $\varphi = (\varphi^0_n,\varphi_n)$, $\varphi^0_n \in \mathbb{R}$, $\varphi_n \in \mathbb{R}^d$; $\varphi^k_n$ is the money invested in asset $k$ on $[n,n+1)$. Its value before/after trading at time $n$ is $X_n^- := \varphi^0_{n-1}(1+i_n) + \varphi_{n-1}\cdot\tilde R_n$, $X_n^+ := \varphi^0_n + \varphi_n\cdot e$; $\varphi$ is self-financing if $X_n^- = X_n^+$ a.s. for every interior $n$. An arbitrage opportunity is a self-financing $\varphi$ with $X_0^\varphi = 0$, $X_N^\varphi \geq 0$ a.s., $X_N^\varphi > 0$ with positive probability. The relative risk process $R_n^k := \tilde R_n^k/(1+i_n) - 1$ is the excess return of asset $k$ over the riskless rate.

Formalization targets

Goal — Theorem 3.1.5

$$\text{No arbitrage} \iff \forall\, n < N,\ \forall\, \mathcal{F}_n\text{-measurable } \varphi_n \in \mathbb{R}^d: \quad \varphi_n \cdot R_{n+1} \geq 0 \text{ a.s.} \implies \varphi_n \cdot R_{n+1} = 0 \text{ a.s.}$$

This is the weakest stable statement that captures the reduction: it asserts the equivalence of the global, whole-horizon absence of arbitrage strategies with a one-period static condition on the relative risk vector, without asserting the stronger (and here unproved) existence of a martingale measure.

No further milestone is formalized in this mission: this chapter's only other theorem, Theorem 3.3.1 (binomial-tree weak convergence to Black-Scholes), needs the Skorokhod topology on the space of càdlàg paths, absent from Mathlib and out of scope to construct here — see the Formalization scope section and HARD.md.

Significance

Theorem 3.1.5 is the tool that lets every later chapter's "assume the market has no arbitrage" hypothesis be checked and used one period at a time rather than as a global existential statement over an intractably large space of strategies. It is also the precise, minimal claim this section proves: contrasted with the full fundamental theorem of asset pricing (no arbitrage $\iff$ existence of an equivalent martingale measure, due to Harrison–Kreps 1979 and Dalang–Morton–Willinger 1990 in this discrete-time generality), Theorem 3.1.5 is a strictly weaker, purely measure-theoretic reduction that requires no separating-hyperplane or martingale-measure construction to state (only to prove). The definitions this chunk formalizes alongside it — portfolios, self-financing, arbitrage, and utility functions with the Arrow-Pratt risk-aversion coefficient — are the vocabulary every financial mission of this book (Chapters 4, 6, 9, 11) is built from.

Formalizing it contributes the exact discrete-time, filtration-indexed statement of the reduction — a result absent from the platform (searched "arbitrage", "self-financing", "martingale measure", "utility function"; the one related hit, LinearOptimization.no_arbitrage_iff_state_prices, is a static single-period linear-programming duality statement — no-arbitrage iff nonnegative state prices exist for a fixed return matrix — a different equivalence for a different, non-stochastic model, not reused here).

Difficulty

The direction "local no-free-lunch at every stage $\Rightarrow$ no arbitrage" is the easy one: an arbitrage strategy, unwound via the recursive wealth formula, forces a violation of the local condition at some stage by a stopping-time argument on the first period where the wealth increment is a.s. nonnegative and not a.s. zero. The converse, "an arbitrage opportunity forces the local condition to fail somewhere," is the direction that needs the reduction of the whole-horizon problem to a single period: the natural first attempt (induct forward from $n=0$) does not directly work, because whether a strategy is an arbitrage is a statement about the terminal wealth $X_N$, and a violation at an early stage does not obviously propagate; the book's proof instead identifies, from an arbitrage strategy, the last stage at which the one-period condition fails and constructs a genuinely one-period arbitrage there — an argument that needs care with the a.s.-qualifiers at every step (the difference between "$X \geq 0$ a.s." failing to imply "$X < 0$ with positive probability" only up to null sets is exactly where the measure-theoretic bookkeeping matters).

Formalization scope

The market is represented via DiscreteFinancialMarket, bundling the probability space, filtration, and the two primitives ($i$, $\tilde R$) actually used; price processes $S^0, S^k$ are not separately represented, since they would only be running products of these two primitives with no further role once the relative risk process $R$ is derived. Filtration is represented directly as a monotone family of sub-$\sigma$-algebras with a trivial Fam 0, not via Mathlib's Filtration structure, to avoid instance-juggling that would add no content here. Adaptedness/predictability and the a.s. conditions of every definition are exactly the book's own. Definitions 3.2.1-3.2.2 (the continuous-time portfolio and its self-financing condition, needed by chunk 09b's jump-market model) use an abstract StochasticIntegral operator taken as given data, since Mathlib has no general theory of integration against an arbitrary càdlàg semimartingale (only specific constructions such as Itô integration against Brownian motion); this is a deliberate infrastructure gap flagged for whoever eventually needs to instantiate it, not a hidden simplification of the definition's own content, which states the self-financing equation exactly as the book writes it.

Theorem 3.3.1 is not formalized in this mission and is recorded in HARD.md. The theorem asserts weak convergence of the whole path of the binomial-tree price process to the Black-Scholes-Merton stock price on the Skorokhod space $D[0,T]$ of càdlàg functions with the Skorokhod topology — a materially stronger and more setup-heavy claim than finite-dimensional convergence in distribution, and the book explicitly names this topology (it is not left implicit). Mathlib has no formalization of $D[0,T]$ or the Skorokhod topology, and building either from scratch (the space of càdlàg functions, the Skorokhod metric via time-warpings, the tightness criteria needed for Donsker-type invariance principles) is a substantial undertaking outside the scope of a single milestone; weakening the claim to convergence of finite-dimensional distributions, or silently substituting an unnamed alternative topology (e.g. uniform convergence, under which the claim would in fact be false, since the discretized paths have jumps the limit does not), would misstate the theorem rather than state a smaller piece of it faithfully. A general-purpose Skorokhod-space/Skorokhod-topology formalization in Mathlib — reusable well beyond this book — is the prerequisite contribution that would unlock this result.

No trivializing formalization: NoArbitrage quantifies over all self-financing portfolios (Portfolio M, an unrestricted adapted process, not a finite or parametrized family), and the one-period condition of part b) quantifies over all $\mathcal{F}_n$-measurable $\varphi_n \in \mathbb{R}^d$ — narrowing either quantifier (e.g. to strategies with bounded positions) would state a weaker, easier claim than the book's own theorem.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. M. Harrison and D. M. Kreps, "Martingales and arbitrage in multiperiod securities markets", Journal of Economic Theory, 1979 (the discrete-time fundamental theorem of asset pricing this chapter's Theorem 3.1.5 is a structural lemma toward, not itself proved in this section).

Motivation

Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).

A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$: a state set $Q$, a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$, an initial state $q_0$ and marker states $Q_m \subseteq Q$. Extending $\delta$ to strings gives the generated language $L(\mathcal G)$ (strings along which $\delta$ is defined from $q_0$) and the marked language $L_m(\mathcal G)$ (those that end in $Q_m$). The closure $\bar K$ of a language $K$ is its set of prefixes. Throughout, $\mathcal G$ is trim: $L(\mathcal G) = \bar L_m(\mathcal G)$. A recognizer for a language $K$ is an accessible generator whose marked language is $K$.

A subset $\Sigma_c \subseteq \Sigma$ of events is controllable. A supervisor is $\mathcal S = (S, \phi)$ where $S = (X, \Sigma, \xi, x_0, X_m)$ is an accessible deterministic automaton with possibly infinite state set and $\phi : X \to \{0,1\}^{\Sigma_c}$ is a state feedback map; events outside $\Sigma_c$ are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep and allows $\sigma$ from $(x, q)$ iff $\xi(\sigma, x)$ and $\delta(\sigma, q)$ are defined and $\phi(x)(\sigma) = 1$. Its languages are $L(\mathcal S/\mathcal G)$, $L_m(\mathcal S/\mathcal G)$ (marker set $X_m \times Q_m$) and $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$.

$\mathcal S$ is complete if $S$ never refuses an event that the plant can execute and $\phi$ enables: $s \in L(\mathcal S/\mathcal G)$, $s\sigma \in L(\mathcal G)$ and $\phi(\xi(s, x_0))(\sigma) = 1$ imply $s\sigma \in L(\mathcal S/\mathcal G)$. It is proper if it is complete and $\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G)$.

A projection $\pi : \mathcal S \to \hat{\mathcal S}$ is a surjection $X \to \hat X$ with $\pi(x_0) = \hat x_0$, $X_m = \pi^{-1}(\hat X_m)$, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ wherever $\xi(\sigma, x)$ is defined, and $\hat\phi \circ \pi = \phi$.

For a language $K$, strings $s, s'$ are $\bar K$-equivalent if $st \in \bar K \iff s't \in \bar K$ for all $t$. The automaton $S$ is $\bar K$-reduced if $\bar K$-equivalent strings of $\bar K$ lead to the same state, and $\bar K$-trim if every state is reached by a string of $\bar K$.

Formalization targets

Goal: Theorem 10.1 (quotient structure theorem)

Let $\mathcal S = (S, \phi)$ be complete, $K_1 := L_m(\mathcal S/\mathcal G)$, $K_3 := L(\mathcal S/\mathcal G)$, with $S$ $K_3$-reduced and $K_3$-trim, and let $\hat S^0 = (X^0, \Sigma, \xi^0, x^0_0, X^0)$ be a trim recognizer for $K_3$. Then there are $X^0_m \subseteq X^0$ and $\phi^0$ such that $\mathcal S^0 = ((X^0, \Sigma, \xi^0, x^0_0, X^0_m), \phi^0)$ satisfies

$$\mathcal S^0 \text{ complete},\quad L_m(\mathcal S^0/\mathcal G) = K_1,\quad L(\mathcal S^0/\mathcal G) = K_3,\quad \exists\, \pi : \mathcal S^0 \to \mathcal S,\quad \mathcal S \text{ proper} \Rightarrow \mathcal S^0 \text{ proper}.$$

Milestones

Proposition 8.1 (p. 219): for complete $\mathcal S$ and a projection $\pi : \mathcal S \to \hat{\mathcal S}$, (i) $\pi$ is unique; (ii) $(L_m, L_c, L)(\mathcal S/\mathcal G) = (L_m, L_c, L)(\hat{\mathcal S}/\mathcal G)$; (iii) $\hat{\mathcal S}$ is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.

The displayed steps of the proof of Theorem 10.1 (pp. 223–224): $\pi(\xi^0(s, x^0_0)) := \xi(s, x_0)$ is well defined on $X^0$; it is a projection once $X^0_m := \pi^{-1}(X_m)$ and $\phi^0 := \phi \circ \pi$; $L(\mathcal S^0/\mathcal G) = K_3$ follows from two enablement conditions; $\mathcal S^0$ is complete; and $L_m(\mathcal S^0/\mathcal G) = K_1$.

Significance

Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of $K_3$. Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.

The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, $S$ and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ for all $\sigma, x$, is not available: the page asks for it only where $\xi(\sigma, x)$ is defined, and Proposition 8.1 (ii) holds only because completeness of $\mathcal S$ compensates for transitions that $\hat\xi$ has and $\xi$ lacks. Likewise, the map $\pi$ of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that $\hat S^0$ recognizes $K_3$ with all states marked and that $S$ is $K_3$-reduced.

Formalization scope

The alphabet is a Lean type α with [Fintype α] (the page's $\Sigma$, which is Lean syntax); strings are List α, $s\sigma$ is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and "$\sigma$ enabled at $x$" means $\sigma \notin \Sigma_c$ or $\phi(x)(\sigma) = 1$; the page's $\phi : X \to \{0,1\}^\Sigma$ is the same object under this extension. The closed loop is run from $(x_0, q_0)$ without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.

Standing assumptions that are hypotheses of every theorem: $\Sigma$ finite; $\mathcal G$ trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume $\mathcal S$ complete, $S$ $K_3$-reduced and $K_3$-trim, and a trim recognizer $R$ for $K_3$ with all states marked, and $\mathcal S^0$ is built on that given $R$ rather than on a recognizer chosen by the prover. The conclusion names $K_1$ and $K_3$ as the languages of $\mathcal S$, not as free variables. A projection predicate that drops $\pi(x_0) = \hat x_0$, surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.

Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.

Selected references

• P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
• C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
• W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

Motivation

Most concrete applications of Markov Decision Theory — inventory control, cash management, linear-quadratic regulation, sequential games — have data that does not change from one period to the next: the same state space, action space, transition mechanism and reward apply at every stage, only discounted by a fixed factor $\beta$ per period. Bäuerle and Rieder's Chapter 2, §2.5 specializes the general finite-horizon theory of the previous sections to this stationary case, and §2.6 shows the specialization at work on three classical models: a card game with a famously boring answer, a firm's cash-management problem, and stochastic linear-quadratic control. Together they demonstrate the payoff of the abstract theory: once the Structure Assumption is checked for a stationary model, the general machinery (the Forward Induction Algorithm) produces the concrete optimal policy — a critical-level $(s,S)$-type control for cash management, a linear feedback law for LQ control — with no further case-specific argument.

Setting

A stationary Markov Decision Model is a Markov Decision Model $(E,A,D,Q,r,g)$ (Definition 2.1.1) whose data does not depend on the stage: the reward at absolute time $n$ is $\beta^n r$ and the terminal reward at time $N$ is $\beta^N g$, for a fixed discount $\beta \in (0,1]$. For a policy sequence $\pi = (f_0,\dots,f_{n-1}) \in F^n$ (each $f_k$ a decision rule $E \to A$ with $f_k(x) \in D(x)$), the reward-to-go is $J_n^\pi(x) := \mathbb{E}^\pi_x\bigl[\sum_{k=0}^{n-1} \beta^k r(X_k,f_k(X_k)) + \beta^n g(X_n)\bigr]$ and the value function is $J_n(x) := \sup_{\pi \in F^n} J_n^\pi(x)$. The operators $(Lv)(x,a) := r(x,a) + \beta\int v(x')\,Q(dx'\mid x,a)$, $(Tv)(x) := \sup_{a \in D(x)} (Lv)(x,a)$, $(T^f v)(x) := (Lv)(x,f(x))$ are the stationary counterparts of §2.3's non-stationary operators. The (stationary) Structure Assumption (SAN) asks for sets $\mathrm{I\!M} \subseteq \mathrm{I\!M}(E)$, $\Delta \subseteq F$ with $g \in \mathrm{I\!M}$, $v \in \mathrm{I\!M} \Rightarrow Tv \in \mathrm{I\!M}$, and every $v \in \mathrm{I\!M}$ having a maximizer in $\Delta$.

Formalization targets

Goal — Theorem 2.6.2 (the cash balance problem)

A firm's cash level $x \in \mathbb{R}$ moves under i.i.d. shocks; each period the firm transfers to a new level $a$ at linear cost $c(a-x) = c_u(a-x)^+ + c_d(a-x)^-$, pays a convex, coercive holding cost $L(a)$ ($L(0)=0$), and the level becomes $a - Z_{n+1}$. Modeled as a stationary MDM with $E=A=\mathbb{R}$, $r(x,a) = -c(a-x) - L(a)$, $g \equiv 0$:

$$\exists\, S_n^- \le S_n^+ \ \text{(depending on $n$)}: \quad J_n(x) = \begin{cases} (S_n^- - x)c_u + L(S_n^-) + \beta\,\mathbb{E}[J_{n-1}(S_n^- - Z)] & x < S_n^- \\ L(x) + \beta\,\mathbb{E}[J_{n-1}(x-Z)] & S_n^- \le x \le S_n^+ \\ (x-S_n^+)c_d + L(S_n^+) + \beta\,\mathbb{E}[J_{n-1}(S_n^+ - Z)] & x > S_n^+, \end{cases}$$

with $J_0 \equiv 0$, and the optimal policy transfers up to $S_n^-$ below it, down to $S_n^+$ above it, and does nothing in between. This is the weakest stable statement: it asserts the existence of critical levels with the stated recursive characterization, not any closed form for $S_n^\pm$ itself (which depends on $L$'s exact shape and is not computable in general).

Three milestones build toward and alongside it: the Reward Iteration theorem and stationary Structure Theorem (Theorems 2.5.3-2.5.4, the general machinery instantiated), the trivial-but- sharp red-and-black card game (Theorem 2.6.1), and the stochastic linear-quadratic problem (Theorem 2.6.3, a Riccati-type recursion with random coefficients).

Significance

Theorem 2.6.2 is the textbook derivation of $(s,S)$-type control, the dominant policy structure in inventory theory and cash management: a firm should act only when its state leaves a band, and should act to bring it exactly to the band's edge, never further. Its proof pattern — verify (SAN) with $\mathrm{I\!M}$ the convex functions of at most linear growth, extract the critical levels from the derivative conditions of a one-stage minimization — is the template used across the inventory-control literature for essentially every variant of this problem. Theorem 2.6.1's answer ("no strategy beats stopping immediately") is a genuine, if minimal, comparative-statics fact: a positive-content instance of $\mathrm{I\!M}$ collapsing to functions constant on the game's absorbing set, forcing every action to be a maximizer. Theorem 2.6.3's Riccati-type recursion, with random transition coefficients, generalizes the classical deterministic-coefficient LQR (linear-quadratic regulator) of control theory; the recursion governs mean-variance and quadratic-hedging problems return to in later chapters of this book (Chapters 4 and 6).

None of the three examples' specific results were found on the platform (searched for "comparative statics", "convex Markov decision", the exact model names, and "bang-bang"/"LQR" adjacent terms). BertsekasDP.riccati_completion_of_square is the platform's one close relative to Theorem 2.6.3: it solves the deterministic-coefficient LQR by a completion-of-squares argument, not the random-coefficient recursion here, so it is cited as related work rather than reused. The proofs themselves are complete and self-contained in the book (a few pages each, using only single-variable convex analysis and elementary linear algebra); this mission contributes the formal statement of each, in its full generality (general convex $L$, general random $(A,B)$ coefficient pairs), as the task for a sorry-free proof.

Difficulty

The cash-balance proof's central step is showing the minimizer of the one-stage problem is of critical-level form for every $v$ in the candidate class $\mathrm{I\!M}$ — not just for the particular sequence $J_0, J_1, \dots$ that eventually arises. The obvious shortcut, guessing the form of $J_n$ directly and verifying it solves the Bellman equation by substitution, fails because $S_n^-, S_n^+$ are themselves defined only implicitly, via one-sided derivative conditions on $L(x) + \beta\mathbb{E}[v(x-Z)]$; there is no closed form to substitute except in degenerate special cases (e.g. $L$ quadratic). The genuine content is the general argument (convexity of the one-stage objective forces a unique critical-level minimizer structure, and this structure is preserved under $T$) that lets the induction go through for an arbitrary convex, coercive $L$. For Theorem 2.6.3, the natural first attempt — solve the deterministic LQR recursion and substitute expected coefficient matrices for the random ones — is not obviously valid, since $\mathbb{E}[B^\top Q B] \ne (\mathbb{E}[B])^\top Q\,\mathbb{E}[B]$ in general; the correct recursion genuinely involves the joint second moments of $(A,B)$, which is exactly what the standing positive-definiteness assumption on $\mathbb{E}[B^\top Q B]$ (not on $\mathbb{E}[B]$ itself) is there to make precise.

Formalization scope

The stationary vocabulary (StationaryMarkovDecisionModel, its operators, J, (SAN)) is restated independently of chunk 02a's non-stationary vocabulary — drafts in this series cannot import one another, and the book itself keeps the two notationally separate ($J_n$ vs. $V_n$, related by $V_n(x) = \beta^n J_{N-n}(x)$, a relation this mission does not separately formalize since no listed result needs it). Theorem 2.6.3's stochastic LQ problem is explicitly non-stationary in the book's own text, so a second, NS-prefixed restatement of the non- stationary model and value function (via the Bellman recursion established as Theorem 2.3.8, not the sup-over-policies primitive — the same simplification chunk 02c makes for its own V) is introduced solely for that one theorem. The card game (Theorem 2.6.1) is formalized on the concrete state space $\mathbb{N} \times \mathbb{N}$ and action space Bool, with the model's exact transition density, reward and terminal reward given as hypotheses on an abstract StationaryMarkovDecisionModel, matching the book's own discrete-density notation $q(x'\mid x,a) := Q(\{x'\}\mid x,a)$ (introduced in the text following Theorem 2.5.4) rather than built from an explicit PMF/Kernel construction — a lighter-weight but equally precise formalization, since the density equations pin the kernel exactly. The stochastic LQ problem uses Matrix (Fin m) (Fin m) ℝ and needs a MeasurableSpace (Matrix m n α) instance Mathlib does not provide (Matrix is a non-reducible def for m → n → α); this mission supplies it by transport across the definitional equality. Random matrix moments $\mathbb{E}[F(A,B)]$ are computed entrywise as ordinary Bochner integrals against the joint law of $(A,B)$.

A trivializing formalization is ruled out on two fronts: the cash-balance critical levels $S_n^-, S_n^+$ are existentially quantified as functions of $n$, not fixed constants (dropping the index would silently claim a single band works for every horizon length, which is false in general); and the card game's "every strategy is optimal" is stated as a universally-quantified claim over all policy sequences, not weakened to mere existence of an optimal one. Reusable infrastructure: the jointMatMean/xQx helpers and the MeasurableSpace (Matrix m n α) instance are generic and available to any later chunk needing random-matrix moments (none of the remaining chunks' briefs currently list one, but Chapter 4's mean-variance and LQ-flavored missions may). sorry-free proofs of all five items are welcome contributions; Theorem 2.5.3's short inductive proof (unwinding the accumulator definition against the operator-composition recursion) is likely the easiest entry point.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005 (the classical deterministic-coefficient LQR, BertsekasDP.riccati_completion_of_square on the platform).

Motivation

Single-machine sequencing with deferral costs asks how to order jobs when the price of finishing a job depends on when it finishes. A job completed at time $s$ incurs the cost $P_i(s)$; lateness penalties, holding costs and service-level penalties are special cases. Two objectives are standard: the sum of the costs, studied by McNaughton (Management Science 6(1), 1959) and Lawler (Management Science 11(2), 1964), and the maximum cost, the bottleneck objective, which asks that no single job be charged too much.

At the end of his 1968 paper on minimizing the number of late jobs (Moore, Management Science 15(1)), J. M. Moore added a short section, suggested by E. L. Lawler, showing that the maximum-cost problem reduces to a family of feasibility problems with due-dates. Each such problem is settled by one sort, by Jackson's earliest-due-date rule (J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, UCLA Research Report 43, 1955). This reduction is the unconstrained case of what later became Lawler's algorithm for $1|\mathrm{prec}|f_{\max}$ (Lawler, Management Science 19(5), 1973).

Timeline:

• 1955: Jackson shows that ordering jobs by due-date minimizes the maximum tardiness, so a schedule with no late jobs exists iff the due-date order has none.
• 1959, 1964: McNaughton and Lawler study the sum of deferral costs.
• 1968: Moore (this paper) reduces the maximum deferral cost to Jackson's lemma through the generalized inverses $P_i^*$.
• 1973: Lawler's backward rule handles general non-decreasing costs with precedence constraints.

Setting

A finite nonempty set $J$ of jobs is processed on one machine that starts at time $0$ and runs without idle time or preemption. Job $j$ has processing time $t_j \ge 0$. A schedule $S$ is an ordering of $J$ with each job appearing exactly once, and $C_j^S$ is the completion time of $j$ in $S$: the sum of the processing times of $j$ and of every job before it.

Each job has a deferral cost $P_j : \mathbb R \to \mathbb R$, which is continuous, bounded and non-decreasing. The maximum deferral cost of $S$ is

$$\mathrm{maxCost}(S) = \max_{j \in J} P_j(C_j^S).$$

For a cost level $y$, the generalized inverse $P_j^*(y) \in \mathbb R \cup \{+\infty\}$ is the latest time at which job $j$ can be completed at cost at most $y$. Following the paper's definition (p. 108), with times $s \ge 0$:

• $P_j^*(y) = \max\{s \ge 0 : P_j(s) = y\}$ if that level set is nonempty (this includes the paper's case of an existing inverse);
• $P_j^*(y) = 0$ if $P_j(s) > y$ for all $s \ge 0$;
• $P_j^*(y) = +\infty$ if $P_j(s) < y$ for all $s \ge 0$.

For each $y > 0$, $S_D(y)$ is a schedule ordered by the "due-dates" $D_j = P_j^*(y)$, with ties broken arbitrarily. $S_D(y)$ has no late jobs if $C_j^{S_D(y)} \le P_j^*(y)$ for every $j$.

In Lean these are IsSchedule, completionTime, Pstar, NoLateAt and maxCost in the namespace MooreLateJobs.MaxDeferral.

Formalization targets

Goal: $S_D(y^*)$ is optimal

Let $y^* > 0$ satisfy: (1) $S_D(y^*)$ has no late jobs; (2) for every $0 < y < y^*$, $S_D(y)$ has at least one late job. Then for every schedule $S$ of $J$,

$$\mathrm{maxCost}\bigl(S_D(y^*)\bigr) \le \mathrm{maxCost}(S).$$

This is the last sentence of the section (p. 109). The goal takes $y^*$ with its two properties as given, so it needs no hypothesis beyond the model.

Milestones

1. Lemma (Jackson), p. 105: a schedule with no late jobs exists iff every due-date ordering has none. It is stated for extended-real due-dates, which is how the section uses it.
2. Monotonicity of $P_j^*$, p. 109: $y_1 \le y_2 \Rightarrow P_j^*(y_1) \le P_j^*(y_2)$.
3. A feasible level exists, pp. 108–109: for bounded costs there is $y > 0$ with $S_D(y)$ on time.
4. Existence of $y^*$, p. 109 with footnote 3. If some $S_D(y_1)$ is on time and some $S_D(y_0)$ is not, a level $y^*$ with properties (1) and (2) exists.

Significance

The result. The theorem turns a min–max problem over all $n!$ schedules into a monotone one-parameter feasibility question. Each value of $y$ is checked by a single sort, and the optimal level is the threshold where feasibility switches on. The same threshold structure underlies bottleneck scheduling and the backward rule for $1|\mathrm{prec}|f_{\max}$. Special cases include minimizing the maximum lateness, $P_j(s) = s - d_j$, clipped to be bounded, and minimizing the maximum weighted tardiness.

Formalizing it. The result is classical and proved on paper, but no machine-checked proof of it, or of Jackson's lemma, is known to exist. The mission would produce a checked Jackson lemma for extended-real due-dates, a verified generalized inverse of a monotone continuous function with the paper's case analysis, and the threshold argument connecting them. Jackson's lemma is shared with part I of this series (minimizing the number of late jobs).

Difficulty

The reduction is short on paper. The work is in the edge cases that the paper passes over:

• The generalized inverse. The comparison $C_j \le P_j^*(y)$ agrees with $P_j(C_j) \le y$ only away from the corner case $C_j = 0$ with $P_j(0) > y$. That job is never "late", yet its cost exceeds $y$. The goal must still hold when such jobs exist.
• Monotonicity. The monotonicity of $P_j^*$ needs continuity. It fails if times range over all of $\mathbb R$ instead of $s \ge 0$.
• Attainment. The feasible levels form an up-set of $(0,\infty)$. That its infimum is attained, so that $y^*$ exists, needs right-continuity in $y$ of the feasibility of each of the finitely many schedules.
• Jackson's lemma. The exchange argument must handle due-dates equal to $0$ or $+\infty$ and zero processing times.

Formalization scope

Conventions committed to in Lean:

• Jobs form a type ι with decidable equality, and the job set is J : Finset ι, assumed nonempty in the goal. Processing times are t : ι → ℝ with 0 ≤ t i: this is added, because the page never states it but processing times are durations.
• Costs are P : ι → ℝ → ℝ, each continuous, bounded (∃ M, ∀ s, |P i s| ≤ M) and monotone, as on p. 108. The Introduction's assumption $t_i \le D_i$ has no counterpart, since the problem has no given due-dates, and it is not assumed.
• A schedule is a duplicate-free list whose elements are exactly $J$. Completion times are prefix sums of processing times, starting at $0$.
• Pstar f y : EReal, with every time in the definition ranging over $s \ge 0$. If the level set $\{s \ge 0 : f(s) = y\}$ is unbounded, its "max" does not exist, and the value is fixed to $+\infty$. The final case is "otherwise", which for continuous monotone $f$ is the paper's case (c).
• The family $S_D$ is any SD : ℝ → List ι such that SD y is a due-date-ordered schedule for every $y > 0$. Theorems hold for every such family, so every tie-break is covered.
• "For all $y < y^*$" is read as $0 < y < y^*$, because $S_D(y)$ is defined only for $y > 0$.
• The existence milestone takes footnote 3's hypothesis (some feasible level) in place of boundedness. It also takes the added hypothesis that some level $y_0 > 0$ is infeasible: with all costs identically $0$, every $S_D(y)$ is on time and no $y^* > 0$ has property (2).

The goal is not the trivializing statement "every on-time $S_D(y)$ is optimal", which is false for large $y$. It concerns exactly the threshold level $y^*$. The minimum is over all schedules of $J$, not over the $S_D(y)$ only.

The needed infrastructure is list permutations, prefix sums and Finset.sup', plus basic facts about sSup of closed sets bounded above in ℝ, and the intermediate value theorem. The Jackson lemma and the generalized inverse are reusable beyond this mission. Contributions are welcome on any milestone, in any order. The goal depends only on the Jackson lemma and on properties of Pstar.

Not in scope: the remark that $y^*$ "can be found to whatever accuracy is desired by a binary search technique" (computational), and the sum-of-costs problem the section contrasts itself with.

Selected references

• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Sciences Research Project, UCLA, 1955.
• E. L. Lawler, On Scheduling Problems with Deferral Costs, Management Science 11(2):280–288, 1964. https://doi.org/10.1287/mnsc.11.2.280
• R. McNaughton, Scheduling with Deadlines and Loss Functions, Management Science 6(1):1–12, 1959. https://doi.org/10.1287/mnsc.6.1.1
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544

Motivation

Quadratic minimization problems with a combinatorial sign pattern in their Hessian arise throughout applied mathematics: discretizations of elliptic boundary-value problems such as the Poisson equation, resistor-network energy functionals, and the Dirichlet forms of Markov-process potential theory all produce a symmetric matrix whose off-diagonal entries are nonpositive and whose rows are diagonally dominant (Fukushima, Oshima, and Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994). Such matrices are exactly the diagonally dominant symmetric M-matrices of classical numerical linear algebra (Berman and Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994). Murota's Discrete Convex Analysis (SIAM, 2003) identifies the combinatorial content of this sign pattern with a discrete convexity property — submodularity, and its strengthening translation submodularity — of the associated quadratic form, and shows that passing to the Legendre-Fenchel conjugate of such a quadratic form (i.e., inverting the matrix) transports this property to a dual combinatorial property, an exchange axiom, on the conjugate side. This mission formalizes that correspondence for the special, matrix-algebraic case of quadratic forms — the case in which Murota's book gives a self-contained proof using only the classical Farkas lemma, before generalizing the same conjugacy to a much broader class of functions in Chapter 8.

Setting

Let $V$ be a finite ground set (identified with $\{1,\dots,n\}$ in the book) and let $L = (\ell_{ij})_{i,j\in V}$ be a symmetric real matrix. $L$ has off-diagonal nonpositivity if $\ell_{ij}\le 0$ for all $i\ne j$, and diagonal dominance if $\sum_{j} \ell_{ij}\ge 0$ for every row $i$. The associated quadratic form is $g(p) = \tfrac12 p^\top L p$ for $p \in \mathbb R^V$. For $p,q\in\mathbb R^V$ write $p\vee q$, $p\wedge q$ for the componentwise maximum and minimum. A function $g:\mathbb R^V\to\mathbb R$ is submodular if $g(p)+g(q)\ge g(p\vee q)+g(p\wedge q)$ for all $p,q$, and has translation submodularity if the stronger inequality $g(p)+g(q)\ge g((p-\alpha\mathbf 1)\vee q)+g(p\wedge(q+\alpha\mathbf 1))$ holds for every $\alpha \ge 0$, where $\mathbf 1$ is the all-ones vector (ordinary submodularity is the case $\alpha=0$).

On the conjugate side, for $x\in\mathbb R^V$ write $\operatorname{supp}^+(x)=\{i : x_i>0\}$, $\operatorname{supp}^-(x)=\{i:x_i<0\}$, and let $\chi_i$ denote the $i$-th unit vector ($\chi_0$ denotes the zero vector). A function $f:\mathbb R^V\to\mathbb R$ has the exchange property if for all $x,y\in\mathbb R^V$ and $i\in\operatorname{supp}^+(x-y)$ there exist $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ and $\alpha_0>0$ such that $f(x)+f(y)\ge f(x-\alpha(\chi_i-\chi_j))+f(y+\alpha(\chi_i-\chi_j))$ for every $\alpha\in[0,\alpha_0]$. The Legendre-Fenchel conjugate of $f$ is $f^\bullet(p) = \sup_x\{\langle p,x\rangle - f(x)\}$; two functions $g,f$ are conjugate to each other when $g=f^\bullet$ and $f=g^\bullet$. For positive-definite symmetric $M,L$, the quadratic forms $f(x)=\tfrac12x^\top Mx$ and $g(p)=\tfrac12p^\top Lp$ are conjugate to each other exactly when $M$ and $L$ are matrix inverses of one another.

Formalization targets

Goal (Theorem 2.11). For conjugate strictly convex quadratic forms $g$ and $f$ as above,

$$g \text{ has translation submodularity} \iff f \text{ has the exchange property.}$$

This is the mission's capstone: the statement leaves the correspondence at the level of the two named combinatorial properties, without hard-coding which of the two properties is verified in a given application, so it survives exactly as strongly as the underlying conjugacy fact does.

Supporting milestones, in the order the book develops them: Proposition 2.4 (off-diagonal nonpositivity plus diagonal dominance implies positive semidefiniteness); Proposition 2.6 (off-diagonal nonpositivity is equivalent to plain submodularity of $g$); Theorem 2.7 (the full sign pattern is equivalent to translation submodularity of $g$); Proposition 2.9 (conjugate quadratic forms correspond exactly to inverse matrix pairs); Theorem 2.12 (a nine-way equivalence, for a nonsingular symmetric $M$, among membership in the matrix class $\mathcal L^{-1}$, two sign-consistency inequalities on the columns of $M$ together with their strict forms, two directional-derivative reformulations of the exchange property together with their strict forms, and the exchange property itself together with its strict form); Proposition 2.13 (the Farkas lemma in equality form, together with the strict variant valid for a nonsingular coefficient matrix); and Proposition 2.14 (the class $\mathcal L^{-1}$ is closed under taking principal submatrices).

Significance

The M-natural exchange property is the function-level analogue of the base-exchange axiom for matroids, and translation submodularity is the analogue, on the "primal" side, of ordinary submodularity for set functions; Chapter 2's quadratic-form case is the historical and pedagogical entry point for the general conjugacy Chapter 8 proves for the full M-convex/ L-convex function classes. Establishing it here, in the self-contained matrix-algebraic setting, isolates exactly which properties of a quadratic form are combinatorial (tied to the coordinate axes) rather than purely convex-analytic (rotation-invariant): submodularity and the exchange property are not preserved by an orthogonal change of variables, in contrast to ordinary convexity, which Proposition 2.4 shows the same sign pattern also implies.

Formalizing this mission produces the first Lean statement, in this project's namespace, of a genuine conjugacy theorem between a primal-side and a dual-side combinatorial convexity property for a concrete function class; nothing of this kind is yet proved (or, so far as the platform's own search shows, formalized at all) elsewhere on the platform. The nine-way equivalence of Theorem 2.12 is a substantial independent contribution beyond the goal itself, since it is what makes the goal's proof possible via elementary linear algebra rather than the general convex-analytic machinery Chapter 8 needs.

Difficulty

The naive approach to Theorem 2.11 tries to derive the exchange property for $f$ directly from the defining supremum in the conjugate relation $f = g^\bullet$, differentiating under the sup; this fails because the exchange property compares $f$ along a specific combinatorial direction $\chi_i - \chi_j$ tied to two coordinates, not along an arbitrary direction, and no naive first-order argument isolates the right pair $(i,j)$ without already knowing the sign pattern of $M = L^{-1}$. The book's actual route is Theorem 2.12: it reduces the exchange property to a column-wise sign-consistency statement on $M$ itself (conditions (b)/(c)) via the identity $f'(x;d) = x^\top Md$, and closes the loop back to membership in $\mathcal L^{-1}$ using the Farkas lemma applied to the linear system $ML = I$ — a genuinely matrix-algebraic argument that does not generalize verbatim to non-quadratic M-/L-convex functions, which is exactly why Chapter 8 needs a different (convex-analytic) proof for the general case.

Formalization scope

Vectors and matrices are indexed by a general finite type V ([Fintype V] [DecidableEq V]) rather than a fixed Fin n, matching this project's convention elsewhere and letting Proposition 2.14's principal-submatrix statement reuse the class predicate at the restricted index type directly. Quadratic forms are real-valued ((V → ℝ) → ℝ, using Matrix.mulVec and dotProduct) since this chapter's functions are always finite everywhere; the Legendre-Fenchel conjugate is EReal-valued via sSup, since a supremum over an infinite domain need not be finite in general even though it is finite here. Every min(0, \dots)-based condition in Theorem 2.12 and the exchange axioms is unfolded as the logically equivalent disjunction over the finitely many terms achieving the minimum, rather than reified via Finset.inf/WithTop machinery — a faithful, checked-equivalent simplification, not a narrowing (see MODERATION_NOTES.md). "Nonsingular" is Matrix.det ≠ 0. No numeric constant needs instantiation anywhere in this mission. The formalization does not trivialize: the goal's exchange property is stated for the specific combinatorial direction $\chi_i - \chi_j$ with $i\in \operatorname{supp}^+(x-y)$, $j \in \operatorname{supp}^-(x-y)\cup\{0\}$ — not an arbitrary direction, which would reduce the exchange property to a restatement of ordinary convexity and discard the entire combinatorial content the mission is about.

Infrastructure needed: Matrix.PosDef/Matrix.PosSemidef/Matrix.IsSymm (present in Mathlib); everything else (submodularity, translation submodularity, the exchange axioms, the sign-consistency conditions) is defined fresh in DiscreteConvex.CombinatorialB. A solution to the goal will likely want Proposition 2.9, Theorem 2.12, and the Farkas lemma (Proposition 2.13) as lemmas; contributions completing any of the seven milestones independently, or supplying the Schur-complement induction behind Proposition 2.4, are welcome.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003, DOI 10.1137/1.9780898718508, Chapter 2.
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994.
• M. Fukushima, Y. Oshima, M. Takeda, Dirichlet Forms and Symmetric Markov Processes, De Gruyter, 1994.
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27.

Motivation

Monotone variational inequalities cover convex minimisation, convex–concave saddle-point problems, Nash equilibria of monotone games and complementarity problems, and they are the standard model for these in optimization and operations research. First-order methods for them (extragradient, forward–backward–forward, reflected and projected gradient methods) need a stepsize below $1/L$, where $L$ is a global Lipschitz constant of the operator. That constant is often unknown, too pessimistic, or nonexistent: in composite minimisation with a locally smooth term, or in saddle-point problems with bilinear-plus-nonlinear couplings, the operator is only locally Lipschitz. The usual remedy is a linesearch, which costs extra operator or prox evaluations per iteration and complicates the complexity accounting.

Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities (preprint 2018, Optimization Online 6598; published in Mathematical Programming, 2020, doi:10.1007/s10107-019-01416-w) proposes the Explicit Golden Ratio Algorithm (EGRAAL): its stepsizes are computed in closed form from the last two iterates, it uses one evaluation of $F$ and one proximal step per iteration, and it needs neither a Lipschitz constant nor a linesearch. This mission formalizes its main convergence theorem, Theorem 2 of the preprint.

Setting

Let $\mathcal E$ be a finite-dimensional real inner product space with norm $\|\cdot\|=\sqrt{\langle\cdot,\cdot\rangle}$. Let $g:\mathcal E\to(-\infty,+\infty]$ with domain $\operatorname{dom} g=\{x: g(x)<+\infty\}$, and $F:\operatorname{dom} g\to\mathcal E$. The variational inequality (1) asks for

$$z^*\in\mathcal E\quad\text{with}\quad \langle F(z^*),z-z^*\rangle+g(z)-g(z^*)\ge0\quad\forall z\in\mathcal E. \tag{1}$$

Its solution set is $S$. The standing assumptions are: (C1) $S\ne\emptyset$; (C2) $g$ is proper, convex and lower semicontinuous; (C3) $F$ is monotone on $\operatorname{dom} g$, $\langle F(u)-F(v),u-v\rangle\ge0$ for $u,v\in\operatorname{dom}g$.

The proximal operator is $\operatorname{prox}_g(w)=\operatorname{argmin}_x\{g(x)+\tfrac12\|x-w\|^2\}$. Write $\varphi=\frac{\sqrt5+1}{2}$ for the golden ratio. Algorithm 1 (EGRAAL) takes $z^0,z^1\in\mathcal E$, $\lambda_0>0$, a parameter $\phi\in(1,\varphi]$ and a cap $\bar\lambda>0$, sets $\bar z^0=z^1$, $\theta_0=1$, $\rho=\frac1\phi+\frac1{\phi^2}$, and for $k\ge1$ computes

$$\lambda_k=\min\Big\{\rho\lambda_{k-1},\ \frac{\phi\theta_{k-1}}{4\lambda_{k-1}}\frac{\|z^k-z^{k-1}\|^2}{\|F(z^k)-F(z^{k-1})\|^2},\ \bar\lambda\Big\},\qquad \bar z^k=\frac{(\phi-1)z^k+\bar z^{k-1}}{\phi},$$ $$z^{k+1}=\operatorname{prox}_{\lambda_k g}\big(\bar z^k-\lambda_kF(z^k)\big),\qquad \theta_k=\frac{\lambda_k}{\lambda_{k-1}}\phi,$$

with the convention $0/0=+\infty$ in the middle term. The paper uses the bifunction $\Psi(u,v)=\langle F(u),v-u\rangle+g(v)-g(u)$.

Formalization targets

Goal: Theorem 2

If $F$ is locally Lipschitz continuous and (C1)–(C3) hold, then for every run of Algorithm 1 there is $z^*\in S$ with

$$z^k\to z^*\qquad\text{and}\qquad \bar z^k\to z^*.$$

Nothing is fixed beyond the paper's parameter ranges: $\phi\in(1,\varphi]$, $\bar\lambda>0$, $\lambda_0>0$ and the starting points are arbitrary. The two sequences share one limit.

Milestones

1. Eq. (4), the prox-inequality: $\bar x=\operatorname{prox}_g w\iff\langle\bar x-w,x-\bar x\rangle\ge g(\bar x)-g(x)$ for all $x$.
2. Eq. (18), the estimates the step rule gives: $\lambda_k\le\rho\lambda_{k-1}$, $\theta_k\le1+\frac1\phi$, and $\lambda_k^2\|F(z^k)-F(z^{k-1})\|^2\le\frac{\theta_k\theta_{k-1}}4\|z^k-z^{k-1}\|^2$.
3. Eq. (24), an identity that follows from the averaging step: $\|z^{k+1}-z\|^2=\frac\phi{\phi-1}\|\bar z^{k+1}-z\|^2-\frac1{\phi-1}\|\bar z^k-z\|^2+\frac1\phi\|z^{k+1}-\bar z^k\|^2$.
4. Eq. (27), the energy inequality, for $z\in\operatorname{dom}g$ and $k\ge2$.
5. Lemma 2: along bounded runs, $(\lambda_k)$ and $(\theta_k)$ are bounded and bounded away from $0$.
6. Lemma 1 (Bauschke–Combettes, Theorem 5.5): a Fejér monotone sequence whose cluster points lie in a nonempty set $C$ converges to a point of $C$.

Significance

The result. Theorem 2 shows that a monotone variational inequality with a locally Lipschitz operator can be solved by a method whose stepsizes adapt to the local curvature of $F$ at no extra cost: one $F$ evaluation and one prox step per iteration, and no global constant and no backtracking. Because $F$ is only ever evaluated at the prox outputs $z^k\in\operatorname{dom}g$, the method also applies when $F$ is undefined or badly behaved outside the feasible set, where reflected-gradient methods can fail. The same analysis gives an ergodic $O(1/k)$ rate and, under an error bound, an $R$-linear rate (§2.2 of the preprint; not part of this mission). The paper also derives fixed-point algorithms for demi-contractive operators from it.

Formalizing it. The theorem has a published proof; to our knowledge no machine-checked version exists, and Mathlib has no proximal operator, no theory of monotone variational inequalities and no Fejér-monotonicity lemma. This mission produces a formal convergence proof for an adaptive first-order method with a nonsmooth convex term, together with reusable pieces: the prox-inequality for extended-real-valued convex functions, a finite-dimensional Fejér convergence lemma, and a formal model of an adaptive-step algorithm with the $0/0=+\infty$ rule.

Difficulty

The usual convergence argument for projected or extragradient methods bounds the cross term $\langle F(z^k)-F(z^{k-1}),z^k-z^{k+1}\rangle$ using a global Lipschitz constant and a fixed stepsize. Here neither exists. The stepsize at iteration $k$ depends on the iterates, and the energy that decreases changes from step to step, since it involves $\theta_{k-1}$. Local Lipschitz continuity gives a usable constant only once the iterates are known to be bounded, and boundedness has to come from the energy inequality. Stepsizes that tend to $0$ would also break the argument (Lemma 2 excludes this for bounded runs). The last step, identifying cluster points as solutions, needs lower semicontinuity of $g$ and a limit in the prox-inequality along a subsequence with convergent stepsizes.

Formalization scope

$\mathcal E$ is a real InnerProductSpace with FiniteDimensional ℝ E. $g$ is a map E → EReal; (C2) is a structure: $g$ never takes the value $\bot$, is finite somewhere, has a convex epigraph in $E\times\mathbb R$, and is LowerSemicontinuous on $E$. $F$ is a total map E → E, and every hypothesis on it (monotonicity, Lipschitz bounds) is restricted to $\operatorname{dom}g$. The variational inequality is stored as $g(z^*)\le\langle F(z^*),z-z^*\rangle+g(z)$, with $z^*\in\operatorname{dom}g$, which avoids extended-real subtraction. $\operatorname{prox}_{\lambda g}$ is an argmin predicate, so it never produces a junk value. The algorithm is a predicate on the four sequences, written for index $k+1$. The rule $0/0=+\infty$ is a case split: if $F(z^k)=F(z^{k-1})$ the step is $\min\{\rho\lambda_{k-1},\bar\lambda\}$. No condition such as $F(z^1)\ne F(z^0)$ or $\lambda_0\le\bar\lambda$ is imposed.

"Locally Lipschitz" is formalized as Lipschitz on every bounded subset of $\operatorname{dom}g$. This is the property the proof of Lemma 2 uses. It agrees with local Lipschitz continuity when $\operatorname{dom}g$ is closed (for example $g=\delta_C$ for a closed convex $C$, or $g$ finite everywhere) and is stronger otherwise. Eq. (27) is stated for $z\in\operatorname{dom}g$, where $F(z)$ and $\Psi(z,z^k)$ are defined. Lemma 1 carries the hypothesis $C\ne\emptyset$ of its cited source, without which it is false.

The statements are not vacuous: $g\equiv0$, $F\equiv0$ satisfy (C1)–(C3) and the Lipschitz hypothesis, and admit a run of Algorithm 1 with $\lambda_k=\min\{\rho\lambda_{k-1},\bar\lambda\}$. A proof of Theorem 2 must hold for every run with the paper's parameters, not only for such degenerate data.

Contributions welcome: the prox-inequality and the existence of the prox for proper convex lsc $g$ (both reusable beyond this mission), the Fejér lemma, the algebraic estimates (18) and (24), and the energy inequality (27). Once these are in place, Lemma 2 and the cluster-point argument complete Theorem 2.

Selected references

• Y. Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint, Optimization Online 6598, 2018. https://optimization-online.org/wp-content/uploads/2018/05/6598.pdf ; published in Mathematical Programming 184 (2020), 383–410. https://doi.org/10.1007/s10107-019-01416-w
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011 (Theorem 5.5). https://doi.org/10.1007/978-1-4419-9467-7
• G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Ekonomika i Matematicheskie Metody 12 (1976), 747–756.
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM Journal on Optimization 25 (2015), 502–520. https://doi.org/10.1137/14097238X