All missions

Limiting the size of a loss, not its probability

A probability constraint in a stochastic linear program asks that a random linear inequality hold with high probability. It counts every violation the same, however large, and the feasible set it defines is in general not convex, as Klein Haneveld's examples show (Klein Haneveld 1986). Integrated chance constraints replace the probability of a shortfall with its expected size. That single change gives convex feasible sets under no distributional assumption beyond existence of expected values. The models are due to Klein Haneveld, and were investigated further by Klein Haneveld and van der Vlerk, whose paper is the source of the polyhedral representations (2006). This mission formalizes the treatment in Kall and Mayer, Stochastic Linear Programming (2005), Chapter 2, §4.1, which is one of a series of missions on that book.

Setting

Let $\xi$ be a random vector with values in $\Xi$ and law $P$. Let $T(\xi)$ be a random $s\times n$ matrix, $h(\xi)\in\mathbb R^s$ a random vector, and, for a decision $x\in\mathbb R^n$,

$$\zeta(x,\xi)=T(\xi)x-h(\xi).$$

Write $z^+=\max\{0,z\}$ and $z^-=\max\{0,-z\}$, componentwise on vectors. Throughout, the expected values of $T(\xi)$ and $h(\xi)$ exist.

When $s=1$, write $\zeta(x,\xi)=t(\xi)^{\mathrm T}x-h(\xi)$. The separate integrated probability functions are

$$K(x)=\mathbb E_\xi[\zeta^+(x,\xi)],\qquad H(x)=\mathbb E_\xi[\zeta^-(x,\xi)].$$

For general $s$, the joint integrated probability functions are

$$K_J(x)=\mathbb E_\xi\big[\max_{1\le i\le s}\zeta_i^+(x,\xi)\big],\qquad H_J(x)=\mathbb E_\xi\big[\max_{1\le i\le s}\zeta_i^-(x,\xi)\big].$$

A variant fixes $\alpha$ and bounds the expected positive part by the fraction $\alpha$ of $\mathbb E_\xi[|\zeta|]$. With $\bar t=\mathbb E_\xi[t(\xi)]$ and $\bar h=\mathbb E_\xi[h(\xi)]$ it leads to the evaluation function

$$K_\alpha(x)=\alpha(\bar t x-\bar h)+(1-2\alpha)\mathbb E_\xi[\zeta^+(x,\xi)].$$

A finite discrete distribution has realizations $\hat\xi^1,\dots,\hat\xi^N$ with probabilities $p_k>0$, $\sum_k p_k=1$. Write $T^k=T(\hat\xi^k)$, $h^k=h(\hat\xi^k)$, let $t^k_i$ be the $i$-th row of $T^k$, and let $\mathcal N=\{1,\dots,N\}$.

Formalization targets

Goal: Theorem 4.3

For a finite discrete distribution and $\gamma\ge 0$, the set $\mathcal S_J(\gamma)=\{x\mid K_J(x)\le\gamma\}$ is polyhedral, and with $\mathcal I=\{1,\dots,s\}$,

$$\{x\mid K_J(x)\le\gamma\}=\bigcap_{\mathcal K\subset\mathcal N}\ \bigcap_{l\in\mathcal I^{\mathcal K}}\Big\{x\ \Big|\ \sum_{k\in\mathcal K}p_k\big(t^k_{l_k}x-h^k_{l_k}\big)\le\gamma\Big\}.$$

Milestones

1. Proposition 4.1. If $\mathbb E[\vartheta]$ exists, then $\mathbb E[(\vartheta-z)^+]=\int_z^\infty(1-F_\vartheta(t))\,dt$ and $\mathbb E[(\vartheta-z)^-]=\int_{-\infty}^zF_\vartheta(t)\,dt$.
2. Proposition 4.2. $H$, $K$ and $\mathbb E_\xi[|\zeta|]=H+K$ are convex on $\mathbb R^n$.
3. Theorem 4.1. For a finite discrete distribution and $\gamma\ge 0$, $\{x\mid K(x)\le\gamma\}=\bigcap_{\mathcal K\subset\mathcal N}\{x\mid\sum_{k\in\mathcal K}p_k(t^kx-h^k)\le\gamma\}$, and this set is polyhedral.
4. (4.13)–(4.15). Three equivalent forms of the $\alpha$-variant, the identity $K_\alpha=(1-\alpha)K-\alpha H$, and convexity for $\alpha<\tfrac12$, concavity for $\alpha>\tfrac12$, affinity for $\alpha=\tfrac12$.
5. Theorem 4.2. For a finite discrete distribution and $\alpha\in[0,\tfrac12]$, the set $\{x\mid K_\alpha(x)\le 0\}$ is polyhedral with the analogous representation.
6. Proposition 4.3. $H_J$ and $K_J$ are convex on $\mathbb R^n$.

Significance

The convexity results say that an expected-shortfall constraint can be added to a convex program with no assumption on the distribution, and with a random technology matrix. This is in sharp contrast with probability functions, whose generalized concavity needs restrictive assumptions and fails for finite discrete distributions in general. The polyhedral representations go further: for scenario models, integrated chance constraints are finitely many linear inequalities, $2^N-1$ in the separate case and $(s+1)^N-1$ in the joint case. Inequalities of this form are what a dual decomposition method generates one at a time.

All results here are proved in the literature. The mission contributes machine-checked versions of them, in a shared development with the other missions on this book. No formalization of integrated chance constraints was found on the platform when this mission was drafted.

Difficulty

The representations rest on one elementary observation: a sum of positive parts is a maximum over subsets, and a maximum over $i$ inside a sum is a maximum over tuples. The work is in the passage from the expectation, which is a Bochner integral against a sum of Dirac measures, to the finite sum, and in exhibiting the intersection as a single matrix inequality.

The tail formulas of Proposition 4.1 require more. The book's proof is an integration by parts for Stieltjes integrals, and it needs the limits $yP(\vartheta>y)\to 0$ and $xF_\vartheta(x)\to 0$ at infinity. Reusing a layer-cake formula on $(\vartheta-z)^+$ avoids this, but it does not avoid working out the two improper integrals and proving that they exist.

The convexity statements are not pointwise statements alone. Passing from pointwise convexity to the expectation needs integrability of each integrand, which has to be derived from integrability of the entries of $T(\xi)$ and $h(\xi)$; the Bochner integral of a non-integrable function is $0$, so this step cannot be skipped.

Formalization scope

$\mathbb R^n$ is Fin n → ℝ, with $0$-based indices. The law of $\xi$ is a probability measure P on a measurable space Ξ. The book's affine form of $T(\xi)$ and $h(\xi)$ is not used in the chapter, so T and h are arbitrary functions with integrable entries; the book's case is Ξ = ℝʳ. Positive and negative parts are written max 0 z and max 0 (-z). The finite discrete law is discreteLaw, the sum of ENNReal.ofReal (p k) • Measure.dirac (ξhat k), and K, KJ, KAlpha are expectations against it: the finite sums (4.8) and (4.20) are consequences, not definitions, which rules out a trivial formalization. The maximum over rows is Finset.sup' over the nonempty Fin s, so $s\ge 1$ has no junk value at $s=0$. A polyhedral set is IsPolyhedron from the published development VanderbeiLP.StrictComp: a finite system $Ax\le b$, with $m=0$ allowed.

Theorem 4.2 is stated with $\alpha\in[0,\tfrac12]$. The book's printed hypothesis "$\gamma\ge 0$, $\mathcal S(\gamma)$" is copied from Theorem 4.1, and the representation fails for $\alpha>\tfrac12$.

A complete development needs a tail formula for expectations, integrability of finite maxima of integrable functions, and integration against finite sums of Dirac measures. Those facts are reusable in the other missions on this book. Contributions of any of the milestones are welcome, in any order; Theorem 4.3 depends on none of the convexity results.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer/Springer, 2005, Chapter 2, §4.1. https://doi.org/10.1007/b105472
• W. K. Klein Haneveld, Duality in Stochastic Linear and Dynamic Programming, Lecture Notes in Economics and Mathematical Systems 274, Springer, 1986. https://doi.org/10.1007/978-3-642-51697-9
• W. K. Klein Haneveld and M. H. van der Vlerk, Integrated chance constraints: reduced forms and an algorithm, Computational Management Science 3 (2006), 245–269. https://doi.org/10.1007/s10287-005-0007-3

Motivation

A two-stage stochastic linear program models a decision taken before uncertain data are revealed, followed by a corrective (recourse) decision taken afterwards. Production planning under uncertain demand, capacity expansion under uncertain loads and network design under uncertain traffic all have this form. The first-stage decision $x$ is chosen now; once the random vector $\xi$ is observed, a second-stage linear program repairs any infeasibility at minimal cost. The quantity the planner minimizes is the first-stage cost plus the expected cost of the repair, the expected recourse $\mathcal Q(x)$.

Before any algorithm for such a problem can be justified (cutting planes, decomposition, bounding by discrete approximations), one needs to know that the objective is a sensible function: finite, convex and Lipschitz continuous. For a finite number of scenarios this is classical linear programming. For a general distribution of $\xi$ it requires an integrability argument. This mission formalizes that foundation as it is presented in Chapter 3, §2.1 of Kall and Mayer's textbook (Kall & Mayer 2005, ISBN 0-387-23385-7). The results go back to Wets (Wets 1974) and Walkup and Wets (1967) and are standard material in every stochastic programming textbook.

Setting

Let $\xi$ be a random vector in $\mathbb R^r$ with distribution $\mathbb P_\xi$, and let $\Xi=\operatorname{supp}\mathbb P_\xi$ be its support, the smallest closed set of probability one. The second-stage data depend affinely on $\xi$ (equation (2.1)):

$$T(\xi)=T+\sum_{j=1}^r T^j\xi_j,\qquad h(\xi)=h+\sum_{j=1}^r h^j\xi_j,\qquad q(\xi)=q+\sum_{j=1}^r q^j\xi_j,$$

with $T(\xi)\in\mathbb R^{m_2\times n_1}$, $h(\xi)\in\mathbb R^{m_2}$, $q(\xi)\in\mathbb R^{n_2}$. The recourse matrix $W\in\mathbb R^{m_2\times n_2}$ is deterministic (fixed recourse). For a first-stage decision $x\in\mathbb R^{n_1}$ the recourse function is the optimal value of the second-stage LP

$$Q(x;T(\xi),h(\xi),q(\xi))=\min\{q^{\mathsf T}(\xi)y\mid Wy=h(\xi)-T(\xi)x,\ y\ge 0\},$$

equal to $+\infty$ if the LP is infeasible and $-\infty$ if it is unbounded. The expected recourse is $\mathcal Q(x)=\int_\Xi Q(x;T(\xi),h(\xi),q(\xi))\,\mathbb P_\xi(d\xi)$.

Two assumptions are in force throughout:

• Assumption 2.1 (complete fixed recourse): $\{Wy\mid y\ge 0\}=\mathbb R^{m_2}$, so the second-stage LP is feasible for every $x$ and every $\xi$;
• Assumption 2.2: $\{u\mid W^{\mathsf T}u\le q(\xi)\}\neq\emptyset$ for every $\xi\in\Xi$, so the second-stage LP is dual feasible on the support.

The standing moment assumption is $\xi\in L^2$.

Formalization targets

Goal: Theorem 2.3

Under Assumptions 2.1 and 2.2 and $\xi\in L^2$:

$$\mathcal Q(x)\in\mathbb R\ \text{for every }x,\qquad \mathcal Q\ \text{is convex},\qquad |\mathcal Q(x^{(1)})-\mathcal Q(x^{(2)})|\le L\,\|x^{(1)}-x^{(2)}\|\ \text{for some }L .$$

The constant $L$ is not fixed: the statement asserts only that one exists, so the goal does not depend on any particular bound.

Milestones

1. Lemma 2.1: complete recourse holds if and only if $\operatorname{rank}W=m_2$ and the system $Wy=0$, $y_{i_k}\ge 1$, $y\ge 0$ is feasible for a set of $m_2$ linearly independent columns.
2. Lemma 2.2: for every $x$ there is an optimal recourse $y(\cdot)\in L^2$ with $Q(x;\xi)=q^{\mathsf T}(\xi)y(\xi)$ on $\Xi$.
3. Theorem 2.1: $Q(\cdot;\xi)$ is finite, convex and Lipschitz with a constant $D(\xi)\in L^1$.
4. Lemma 2.3: if $\min\{c^{\mathsf T}x\mid Ax=b,x\ge 0\}$ is solvable for every $b$, its value $\varphi$ is convex and $\partial\varphi(b)$ is the set of optimal dual solutions.
5. Theorem 2.2: $\partial_xQ(\hat x;\xi)=\{-T^{\mathsf T}(\xi)\hat u\mid\hat u\ \text{dual optimal}\}$.
6. Corollary 2.1: the conclusions of Theorem 2.3 hold with $\xi\in L^1$ when $q(\xi)$ and $(h(\xi),T(\xi))$ are independent.
7. Proposition 2.1: with deterministic $q$, $\xi\mapsto Q(x;T(\xi),h(\xi))$ is convex.
8. Theorem 2.4: with deterministic $q$, $Q(x;T(\bar\xi),h(\bar\xi))\le\mathcal Q(x)$ for $\bar\xi=\mathbb E\xi$ (the Jensen lower bound).

Significance

Theorem 2.3 makes the deterministic equivalent $\min\{c^{\mathsf T}x+\mathcal Q(x)\mid Ax=b,\ x\ge 0\}$ a convex program with a Lipschitz objective. Convexity gives that local minima are global and that subgradient-based and cutting-plane methods apply; Lipschitz continuity bounds the subgradients and controls the error of approximating $\mathcal Q$. Theorem 2.2 identifies those subgradients as dual solutions of the second-stage LP, which is how the L-shaped method generates its cuts. Proposition 2.1 and Theorem 2.4 give the Jensen lower bound, the starting point for the successive discrete approximation methods developed later in the chapter.

All results here are classical and proved in the source. None of them, to our knowledge, is formalized for a general (not finitely supported) distribution. Related platform items treat finitely many scenarios or other conventions. The work of this mission is to formalize the known proofs. The parametric LP facts (the value function of an LP is piecewise linear on finitely many bases, the dual characterization of its subdifferential) are reusable far beyond stochastic programming.

Difficulty

For finitely many scenarios, each claim reduces to finitely many LPs. The general case has two obstacles. First, measurability and integrability: $\mathcal Q(x)$ is an integral of an extended-real function. One must show that $\xi\mapsto Q(x;\xi)$ is measurable and that it is integrable, and the second needs a growth bound. On each decision region $Q(x;\xi)=q_B(\xi)^{\mathsf T}B^{-1}(h(\xi)-T(\xi)x)$ is quadratic in $\xi$, so $\xi\in L^1$ is not enough in general; this is why $L^2$ (or independence, Corollary 2.1) is assumed. Second, the Lipschitz constant must be integrable: a constant uniform in $\xi$ does not exist when $q$ and $T$ are random, so the pointwise constant $D(\xi)$ of Theorem 2.1 must itself be shown to be in $L^1$. Lemma 2.2's measurable optimal selection has the same character: an optimal $y(\xi)$ exists for each $\xi$, but building a measurable, square-integrable selection requires the finite partition of $\Xi$ into decision regions.

Formalization scope

Vectors are Fin k → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The distribution $\mathbb P_\xi$ is a probability measure μ on Fin r → ℝ (the canonical space, $\xi$ the identity), and $\Xi$ is μ.support. $\xi\in L^2$ is MemLp id 2 μ, $\xi\in L^1$ is Integrable id μ. The recourse function is an EReal infimum, so $\pm\infty$ are represented exactly. The expected recourse is the Bochner integral of its real part, and the goal states explicitly that the recourse value is finite almost surely and integrable, so the real-valued encoding hides no divergent integral. Lipschitz bounds use the Euclidean norm. Finiteness in Theorems 2.1 and 2.3 is stated for every $x\in\mathbb R^{n_1}$, which contains the book's $x\in B_1$.

Reused published definitions: KallMayer.Recourse.LPValue (with SolvableEveryRHS, DualOptimizers), CompleteRecourse, PointwiseRecourse, ExpectedRecourse, and the subdifferential StochasticProg.RecourseKKT.subdifferential. The mission adds only the affine data structure (2.1). Contributions of reusable lemmas are welcome: the finite basis decomposition of an LP value function, measurability of LP value functions in the data, and the chain rule for subdifferentials under affine maps.

Selected references

• P. Kall and J. Mayer, Stochastic Linear Programming: Models, Theory, and Computation, Kluwer/Springer, International Series in Operations Research & Management Science 80, 2005, Chapter 3, §2.1, pp.198–211. ISBN 0-387-23385-7
• R. J.-B. Wets, Stochastic programs with fixed recourse: the equivalent deterministic program, SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
• D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM Journal on Applied Mathematics 15 (1967), 1299–1314. https://doi.org/10.1137/0115113
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Why matroids and the Greedy Algorithm

The Greedy Algorithm builds a set one element at a time, always adding the heaviest element that keeps the set feasible. For the forests of a graph it finds a maximum-weight forest (Kruskal's algorithm), but for the matchings of a graph it can fail: on a 4-cycle with edge weights 9, 7, 8, 3 it picks the edges of weight 9 and 3 when the edges of weight 7 and 8 are better. Matroids are the abstraction of the families on which greedy works. They were introduced by Whitney (1935); the optimality of greedy on matroids is due to Rado (1957) and was rediscovered by Edmonds (1970), who also gave the linear description of the convex hull of independent sets that is the goal of this mission.

This mission formalizes §8.1 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), pp. 273–280. It is the twelfth mission of a series on the book; later missions treat matroid intersection (§8.3) and the matroid intersection polytope (§8.5), which build on the objects defined here.

Timeline:

• 1935: Whitney defines matroids as an abstraction of linear independence.
• 1957: Rado shows that the greedy algorithm finds a maximum-weight independent set of a matroid.
• 1970–1971: Edmonds proves that the polytope $\{x \ge 0 : x(A) \le r(A)\}$ is the convex hull of independent sets, and that greedy optimality characterizes matroids.

Setting

Let $S$ be a finite set and $\mathcal I$ a family of subsets of $S$, the independent sets. The pair $M=(S,\mathcal I)$ is a matroid if

• (M0) $\emptyset \in \mathcal I$;
• (M1) if $J' \subseteq J \in \mathcal I$ then $J' \in \mathcal I$;
• (M2) for every $A \subseteq S$, every maximal independent subset of $A$ has the same cardinality.

A pair satisfying (M0) and (M1) only is an independence system. A maximal independent subset of $A$ is a basis of $A$; its size is the rank $r(A)$. The bases of $S$ are the bases of $M$.

For weights $c \in \mathbb R^S$ the weight of $J$ is $c(J)=\sum_{e\in J} c_e$, and for $x \in \mathbb R^S$ and $A \subseteq S$, $x(A)=\sum_{e\in A} x_e$. The characteristic vector $\chi^J$ of $J \subseteq S$ has $\chi^J_e = 1$ for $e \in J$ and $0$ otherwise.

The Greedy Algorithm: set $J=\emptyset$; while there is $e \notin J$ with $c_e>0$ and $J\cup\{e\}\in\mathcal I$, choose such an $e$ with $c_e$ maximum and replace $J$ by $J\cup\{e\}$. Ties are broken arbitrarily.

The linear program attached to a matroid with rank function $r$ is

$$\text{maximize } \sum_{e\in S} c_e x_e \quad\text{subject to}\quad x(A)\le r(A)\ (A\subseteq S),\qquad x_e \ge 0\ (e\in S). \tag{8.1}$$

Formalization targets

Goal: Edmonds' Matroid Polytope Theorem (Theorem 8.5)

For every matroid $(S,\mathcal I)$ with rank function $r$,

$$\operatorname{conv}\{\chi^J : J \in \mathcal I\} = \{x \in \mathbb R^S : x \ge 0,\ x(A) \le r(A) \text{ for all } A \subseteq S\}.$$

Both inclusions are part of the goal.

Milestones

• Proposition 8.1 (matching matroid): for a graph $G=(V,E)$, the sets $J\subseteq V$ covered by some matching are the independent sets of a matroid on $V$.
• Theorem 8.2: on a matroid, the Greedy Algorithm returns a maximum-weight independent set, for every $c\in\mathbb R^S$.
• Theorem 8.3: an independence system is a matroid if and only if the Greedy Algorithm returns an optimal independent set for every $c \in \mathbb R^S$.
• Theorem 8.4: the characteristic vector of the greedy set is an optimal solution of (8.1).
• Corollary 8.6: an independent set $J$ is maximum-weight iff (a) $c_e \ge 0$ for $e\in J$, (b) $c_e\le 0$ when $e\notin J$ and $J\cup\{e\}\in\mathcal I$, (c) $c_e\le c_f$ when $e\notin J$, $f\in J$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I$.
• Corollary 8.7: a basis $J$ is a maximum-weight basis iff condition (c) holds.

Significance

The Matroid Polytope Theorem turns the combinatorial problem of finding a maximum-weight independent set into a linear program over an explicit inequality system, and it is the prototype for the polyhedral descriptions that follow in the book: the forest polytope (Theorem 8.8), from which the spanning-tree description of Theorem 2.8 follows, and the matroid intersection polytope (Theorem 8.20). Theorem 8.3 characterizes matroids by an algorithmic property, which is why matroids appear wherever greedy methods are analysed. Corollaries 8.6 and 8.7 give local certificates of optimality, used in Section 8.5 for weighted matroid intersection.

All results are classical and proved in the book. None is formalized on Prove2Me, and Mathlib, which has a substantial Matroid library (bases, rank, closure, duality), contains neither the greedy theorem nor the matroid polytope. A formalization supplies the polyhedral layer missing from that library and the bridge between the axioms (M0)–(M2) and linear programming.

Difficulty

The inclusion of the convex hull in the polyhedron is immediate: $\chi^J(A)=|J\cap A|\le r(A)$. The reverse inclusion is the content, and the obvious attempt, writing a feasible $x$ directly as a convex combination of characteristic vectors, has no evident inductive structure: the constraint system has one inequality per subset of $S$, and a fractional $x$ can be tight on many overlapping sets at once. Any route has to relate the exponential system $x(A)\le r(A)$ to the combinatorics of (M2), and has to pass from statements about linear objectives to an equality of sets in $\mathbb R^S$; Mathlib contains neither LP duality for such a system nor the polytope-theoretic facts linking optimal vertices to convex hulls in the form needed.

For Theorem 8.3 the nontrivial direction is the converse: if (M2) fails on some set $A$, one must produce weights for which greedy goes wrong, and the formal statement must account for the nondeterminism of tie-breaking.

Formalization scope

• The ground set $S$ is a finite type α; subsets are Finset α; the family $\mathcal I$ is a predicate I : Finset α → Prop. (M0)–(M1) are the published definition SubsamplingSM.Offline.IsIndepSystem; IsMatroid adds (M2) literally (any two bases of the same set have the same size). This is the book's axiom system, not Mathlib's Matroid, to which it can be bridged.
• rank I A is the largest size of an independent subset of $A$, which for a matroid is the size of every basis of $A$.
• Vectors live in α → ℝ; constraints of (8.1) are imposed for every subset $A$; the rank is cast to ℝ.
• The Greedy Algorithm is a relation: GreedyStep allows every admissible choice among ties, and IsGreedyOutput is any set reachable from $\emptyset$ at which the loop stops. Theorems 8.2 and 8.4 are stated for every run. Theorem 8.3 is stated in both readings (every run, some run), which covers every tie-breaking rule.
• Graphs are finite multigraphs (ends : E → Sym2 V), loops and parallel edges allowed; matchings contain no loops.
• Trivial cases are not excluded: the empty ground set and loops of the matroid ($r(\{e\})=0$, forcing $x_e=0$) are covered by the statements.

Useful contributions: a bridge from IsMatroid to Mathlib's IndepMatroid/Matroid (which gives rank submodularity and exchange properties), LP weak duality and complementary slackness for (8.1), and a lemma reducing equality of a polytope with a convex hull to optimality of hull points for every linear objective. These are reusable in the matroid intersection missions of this series.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley-Interscience, 1998, §8.1. https://doi.org/10.1002/9781118033142
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications (Gordon and Breach, 1970), 69–87. https://doi.org/10.1007/3-540-36478-1_2
• J. Edmonds, Matroids and the greedy algorithm, Mathematical Programming 1 (1971), 127–136. https://doi.org/10.1007/BF01584082
• R. Rado, A note on independence functions, Proceedings of the London Mathematical Society 7 (1957), 300–320. https://doi.org/10.1112/plms/s3-7.1.300
• H. Whitney, On the abstract properties of linear dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182

Motivation

Many combinatorial optimization problems ask for a largest set that is simultaneously "independent" in two different senses. A matching in a bipartite graph $G=(V,E)$ with bipartition $\{V_1,V_2\}$ is a set of edges in which every node of $V_1$ meets at most one edge and every node of $V_2$ meets at most one edge. A branching of a digraph is an arc set that is a forest in the underlying graph and has each node as the head of at most one arc. Each condition on its own defines a matroid, a structure for which the greedy algorithm is optimal. The matroid intersection problem asks for a maximum common independent set of two matroids on the same ground set.

Edmonds (Edmonds 1970) proved that the maximum size of a common independent set is given by a min–max formula in terms of the two rank functions, and gave a polynomial-time algorithm. The theorem contains König's theorem on bipartite matchings as the special case of two partition matroids. This mission formalizes §8.2–8.3 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), which develops this result from the matroid axioms. It is the thirteenth mission of a series covering the book's capstone theorems; the twelfth treats the matroid polytope and the fourteenth the matroid intersection polytope.

Timeline:

• 1935: Whitney introduces matroids.
• 1965: Edmonds and Fulkerson show that matching matroids are transversal matroids.
• 1970: Edmonds proves the Matroid Intersection Theorem and the intersection polytope theorem ("Submodular functions, matroids, and certain polyhedra").
• 1975: Lawler's textbook gives the augmenting-path algorithm in the form used here; the auxiliary "exchange" digraph becomes standard.

Setting

Let $S$ be a finite set and $\mathcal I$ a family of subsets of $S$, called independent sets. The pair $M=(S,\mathcal I)$ is a matroid if (M0) $\emptyset\in\mathcal I$; (M1) subsets of independent sets are independent; (M2) for every $A\subseteq S$, every maximal independent subset of $A$ has the same cardinality. A maximal independent subset of $A$ is a basis of $A$, and its size is the rank $r(A)$. A circuit is a minimal dependent set.

For a matroid $M$, a set $B\subseteq S$ and a basis $J$ of $B$, the contraction $M/B$ has ground set $S\setminus B$ and independent sets $\{J'\subseteq S\setminus B : J'\cup J\in\mathcal I\}$.

Two matroids $M_1=(S,\mathcal I_1)$ and $M_2=(S,\mathcal I_2)$ on the same set $S$ have rank functions $r_1,r_2$; a set in $\mathcal I_1\cap\mathcal I_2$ is a common independent set. For $A\subseteq S$ write $\bar A=S\setminus A$.

Given a common independent set $J$, the auxiliary digraph $G(M_1,M_2,J)$ has node set $S\cup\{r,s\}$ and arcs: $es$ for $e\notin J$ with $J\cup\{e\}\in\mathcal I_1$; $re$ for $e\notin J$ with $J\cup\{e\}\in\mathcal I_2$; $ef$ for $e\notin J$, $f\in J$ with $J\cup\{e\}\notin\mathcal I_1$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I_1$; and $fe$ for $e\notin J$, $f\in J$ with $J\cup\{e\}\notin\mathcal I_2$ and $(J\cup\{e\})\setminus\{f\}\in\mathcal I_2$. A chord of a dipath with node sequence $v_0,\dots,v_k$ is an arc $v_iv_j$ with $i<j-1$.

Formalization targets

Goal: Theorem 8.14 (Matroid Intersection Theorem)

$$\max\{|J| : J\in\mathcal I_1\cap\mathcal I_2\}=\min\{r_1(A)+r_2(\bar A) : A\subseteq S\}.$$

Both matroids are arbitrary (loops allowed, any ranks), and $S$ may be empty.

Milestones

• Theorem 8.9. For $J\in\mathcal I$ and $e\in S$, $J\cup\{e\}$ contains at most one circuit.
• Theorem 8.11. $M/B$ is a matroid, does not depend on the choice of the basis $J$ of $B$, and has rank function $r'(A)=r(A\cup B)-r(B)$ for $A\subseteq S\setminus B$.
• Weak duality (§8.3). For $J\in\mathcal I_1\cap\mathcal I_2$ and $A\subseteq S$, $|J|\le r_1(A)+r_2(\bar A)$.
• Theorem 8.15 (Augmenting Path Theorem). (a) If $G(M_1,M_2,J)$ has no $(r,s)$-dipath, $J$ is maximum, and every $A\subseteq S$ with no arc leaving $A\cup\{r\}$ satisfies $|J|=r_1(A)+r_2(\bar A)$. (b) If there is an $(r,s)$-dipath, $J$ is not maximum, and for a chordless $(r,s)$-dipath $r,e_1,f_1,\dots,e_{m+1},s$, $J\,\triangle\,\{e_1,f_1,\dots,e_{m+1}\}\in\mathcal I_1\cap\mathcal I_2$.
• Lemma 8.16. If $e\in C\subseteq A$ and $C$ is a circuit, then $r(A\setminus\{e\})=r(A)$.

Significance

The Matroid Intersection Theorem is one of the main min–max theorems of combinatorial optimization. It contains König's theorem (two partition matroids), the characterization of maximum branchings, and Rado's theorem on independent transversals, and it is the cardinality case of the weighted matroid intersection theory of §8.5, whose polyhedral form is the subject of the next mission. The Augmenting Path Theorem turns the min–max formula into an algorithm with polynomially many independence tests, and its part (a) gives the optimality certificate $A$ explicitly.

All results of this mission are classical and fully proved in the book. Mathlib has a matroid library (circuits, fundamental circuits, contraction, rank), and it contains the uniqueness of the fundamental circuit (Matroid.IsCircuit.eq_fundCircuit_of_subset), which is Theorem 8.9 in Mathlib's language. To our knowledge Mathlib has neither the matroid intersection theorem nor the augmenting path theorem. The platform has an exchange-graph augmentation statement for shortest walks with oracles (CountingMatroid.Analysis.ShortestExchangeAugmentation.shortest_exchange_augmentation). That is a different statement: it covers shortest walks, while Theorem 8.15 covers chordless dipaths and also the certificate of part (a). The work here is to formalize the book's proofs or to bridge the book's axiomatic matroids to Mathlib's library.

Difficulty

Weak duality takes one line. The other inequality does not follow from any local exchange argument. The book gives two proofs: a short induction on $|S|$ that contracts and deletes one element and then applies submodularity of the rank functions, and the algorithmic proof through Theorem 8.15. In part (b), symmetric difference along an arbitrary augmenting dipath can destroy independence. Chordlessness is what lets the circuit-by-circuit argument with Lemma 8.16 go through, and the book's Exercise 8.37 shows the condition cannot be dropped. Part (a) needs, for each element outside $J$, the unique circuit of Theorem 8.9 to lie inside the right side of the cut.

Formalization scope

The ground set is a finite type S, all of which is the ground set. A matroid is the structure CombOpt.MatroidIntersection.Matroid S: a predicate Indep : Finset S → Prop bundled with the axioms (M0)–(M2) (IsMatroid). (M2), maximal independent subsets (IsMaxIndepIn) and circuits (IsCircuit) reuse the published definitions of the Edmonds matroid-partition mission (EdmondsPartition.Main), which state the same notions. This is the book's axiom system, not Mathlib's _root_.Matroid; on finite ground sets the two describe the same matroids, and a bridge to Mathlib is welcome. rank Indep A is the size of a basis of A with values in ℕ; Ā is the complement Aᶜ. The contraction lives on the subtype {x // x ∉ B}, and its rank formula is stated as $r'(A)+r(B)=r(A\cup B)$, which avoids truncated subtraction. The auxiliary digraph is the arc relation auxArc M₁ M₂ J on nodes AuxNode S (r, s, elem e). A dipath is a node list (IsDipath), chordless means no arc $v_iv_j$ with $i+1<j$ (IsChordless), and the elements visited are innerElems.

The goal states existence of a pair $(J,A)$ with $|J|=r_1(A)+r_2(\bar A)$ together with weak duality for all pairs. A goal stating only one inequality, or only existence of some $J$ and $A$ without the inequality, would not be the theorem.

Contributions welcome: proofs of the milestones, the book's induction proof of Theorem 8.14 (which also needs submodularity of rank, Exercise 8.21), a proof through Theorem 8.15, and an equivalence between CombOpt.MatroidIntersection.Matroid and Mathlib's Matroid on finite types.

Selected references

• W. J. Cook, W. H. Cunningham, W. R. Pulleyblank, A. Schrijver, Combinatorial Optimization, Wiley-Interscience, 1998, §8.2–8.3. https://doi.org/10.1002/9781118033142
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications (Gordon and Breach, 1970), 69–87; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 2003. https://doi.org/10.1007/3-540-36478-1_2
• E. L. Lawler, Matroid intersection algorithms, Mathematical Programming 9 (1975), 31–56. https://doi.org/10.1007/BF01681329
• H. Whitney, On the abstract properties of linear dependence, American Journal of Mathematics 57 (1935), 509–533. https://doi.org/10.2307/2371182

Motivation

In the classical stochastic multi-armed bandit a decision maker is scored by the sum of the rewards it collects. Many applications score the collected rewards differently: a portfolio manager cares about the conditional value at risk (CVaR) or the Sharpe ratio of the returns, a clinical trial about a quantile, a risk-averse controller about mean–variance. Such criteria are not sums, and the regret analysis of upper-confidence-bound (UCB) policies does not apply to them directly.

Cassel, Mannor and Zeevi (arXiv:1806.01380v3; Mathematics of Operations Research, 2023) observe that essentially every criterion that is invariant to the order of the rewards is a function $U$ of the empirical distribution of the rewards, and they give conditions on $U$ under which a single optimistic policy, U-UCB, has regret $O(\log T/T)$, the rate of the classical setting. The paper builds on the $(\alpha,\psi)$-UCB analysis of Bubeck and Cesa-Bianchi (2012) and on earlier work on risk-averse bandits (mean–variance, CVaR) that treated one criterion at a time.

Setting

There are $K$ arms. Arm $i$ has a reward law $F^{(i)}$, an arbitrary probability distribution on $\mathbb R$, and an i.i.d. reward sequence $X_{i,1},X_{i,2},\dots$; all rewards are mutually independent, and a randomization variable $V$ is independent of them. An admissible policy chooses the arm $\pi_t$ of round $t$ as a measurable function of $V$ and of the past arms and rewards. The pull count of arm $i$ is $\tau_i(t)$, and the reward observed in round $t$ is $X_{\pi,t}=X_{i,\tau_i(t)}$ on $\{\pi_t=i\}$.

The empirical distribution of $x_1,\dots,x_t$ is $\hat F_t=\frac1t\sum_{s\le t}\mathbb I_{[x_s,\infty)}$. The policy's empirical distribution after $T$ rounds is $\hat F^\pi_T$, built from $X_{\pi,1},\dots,X_{\pi,T}$, and arm $i$'s is $\hat F^{(i)}_t$, built from $X_{i,1},\dots,X_{i,t}$. Distribution functions live in a real vector space $L$ of functions on $\mathbb R$ carrying a seminorm $\|\cdot\|$, chosen to suit $U$. An empirical distribution performance measure (EDPM) is a map $U:L\to\mathbb R$; the decision maker maximizes $\mathbb E\,U(\hat F^\pi_T)$.

Write $D^\Delta$ for the mixtures $\sum_ip_iF^{(i)}$ of the arm laws, $i^*$ for an arm maximizing $U(F^{(i)})$, $\Delta_i=U(F^{(i^*)})-U(F^{(i)})$, $D=\max_{i,j}\|F^{(i)}-F^{(j)}\|$ and $\rho=\max_{i\ne i^*}\|F^{(i^*)}-F^{(i)}\|/\Delta_i$. The pseudo empirical distribution is $F^\pi_T=\frac1T\sum_i\tau_i(T)F^{(i)}$.

• $U$ is stable with parameters $\upsilon,b>0$, $q\ge1$ if $|U(F)-U(G)|\le b(\|F-G\|+\|F-G\|^q)$ for $F\in D^\Delta$, $G\in L$, and $\mathbb P(\|\hat F^{(i)}_t-F^{(i)}\|\ge x)\le2e^{-\upsilon tx^2}$.
• $U$ is smooth with parameter $\beta\ge0$ (and $M_0=\infty$) if at every $F\in D^\Delta$ there is a bounded linear functional $\partial U(F)$ with $|U(G)-U(F)-\partial U(F)\cdot(G-F)|\le\frac12\beta\|G-F\|^2$ for all $G\in L$.
• $U$ has a linear gap with parameter $\eta>0$ if $U(F)\le U(F^{(i^*)})-\frac1\eta\|F-F^{(i^*)}\|$ on $D^\Delta$.

U-UCB pulls each arm once and then plays $\arg\max_i\big[U(\hat F^{(i)}_{\tau_i(t-1)})+\varphi^{-1}(\gamma\log t/\tau_i(t-1))\big]$, where $\varphi(y)=\min\{\upsilon(y/2b)^2,\upsilon(y/2b)^{2/q}\}$.

Formalization targets

Goal: Theorem 4 (p.10)

There is a horizon $T_1$, depending only on the problem parameters, such that for every run of U-UCB, every admissible policy $\pi'$ and every $T\ge T_1$,

$$\mathbb E\,U(\hat F^{\pi'}_T)-\mathbb E\,U(\hat F^{U\text{-}UCB}_T)\le\frac{L\rho}T\sum_{i\ne i^*}\Big(\frac{\gamma\Delta_i\log T}{\varphi(\Delta_i/2)}+\frac{\gamma+6}{\gamma-2}\Delta_i\Big)+\frac{12\beta K^2\log KT}{\upsilon T},\qquad L=b(1+D^{q-1}).$$

The paper states this for the regret $R_{U\text{-}UCB}(T)$, measured against a finite-horizon oracle $\pi^*(T)\in\arg\max_\pi\mathbb E\,U(\hat F^\pi_T)$. Such an oracle need not exist, so the goal is stated against every admissible comparator; where the oracle exists, choosing it gives the printed statement. The paper's "for all $T\ge T_1$, which is polynomial in problem parameters" is read as: one $T_1$ that depends only on $K,\upsilon,b,q,\beta,\eta,\gamma,D,\rho$ and the gaps, uniform over instances, U-UCB tie-breaking rules and comparators. The paper's explicit condition (29) has $\log T$ on both sides and does not by itself support its printed proof, so "polynomial" has no literal content to formalize. As in Theorem 2, whose bound Theorem 4 prints, $\gamma>2$ and $\Delta_i>0$ for $i\ne i^*$ are assumed.

Milestones

In the order the proof uses them: the tail bound of Lemma 2 for $\|\hat F^\pi_T-F^\pi_T\|$; the integral of Lemma 7 and the moment bounds of Lemma 6; three steps of the proof of Theorem 3 (unbiasedness $\mathbb E\hat F^\pi_T=\mathbb EF^\pi_T$, the vanishing of $\mathbb E[\partial U(F)\cdot(\hat F^\pi_T-F^\pi_T)]$, the bound on the second-order remainder $\delta_1$); Lemma 1 and the distance form of its proof; the concentration inequality (26); the pull-count bound of the proof of Theorem 2; and Theorem 2, the pseudo-regret bound of U-UCB.

Significance

Theorem 4 reduces regret analysis under a non-cumulative criterion to three checks on $U$ in a chosen seminorm. The paper uses it in §5 to obtain $O(\log T/T)$ regret for mean–variance, for CVaR under density assumptions, and for other criteria, and identifies cases where only $O(1/\sqrt T)$ follows. Without the smoothness and linear-gap conditions the framework gives only the weaker bound of Remark 1.

The result is proved in the paper; none of it is machine-checked. The platform has the classical $(\alpha,\psi)$-UCB pseudo-regret bound (RegretBandits.Stochastic.alpha_psi_ucb_pseudo_regret), which is the linear special case of Theorem 2 in a different model. This mission adds a policy-level regret theorem for criteria that are not sums, together with a reusable model of randomized non-anticipating policies over an independent reward stack. Formalizing it also has to repair the proof: the printed proof of Theorem 3 (p.26) bounds $\|\partial U(F^\pi_T)-\partial U(F)\|$ by $\beta\|F^\pi_T-F\|$, which Definition 2 does not give. A counterexample to that step has two point-mass arms, the seminorm $|f(1/2)|+|f(2)|$ and $U=\beta' f(1/2)f(2)$, and gives the factor $2\beta$; Definition 2 does give $3\beta$. Theorem 3 is therefore not posed. Its verified ingredients are milestones, and the goal, whose threshold $T_1$ absorbs the larger constant, is unaffected.

Difficulty

The pseudo regret is handled by the standard UCB argument (Theorem 2). The difficulty is the horizon gap $\mathbb E[U(\hat F^\pi_T)-U(F^\pi_T)]$. The first idea, applying the modulus of continuity to $\|\hat F^\pi_T-F^\pi_T\|$, loses a factor $\sqrt T$ (Proposition 1) even for linear $U$, and gives only $O(1/\sqrt T)$. The $O(\log T/T)$ rate needs the first-order term $\mathbb E[\partial U(F)\cdot(\hat F^\pi_T-F^\pi_T)]$ to vanish for an adaptive policy. That holds pointwise in $x$ by non-anticipation. Passing the expectation through a functional that is only bounded for a seminorm is not automatic and needs a separate argument. The remaining cross term must then be absorbed by the linear gap, which ties $T_1$ to $\eta$, $\beta$ and the pull-count bound.

Formalization scope

Arms are Fin K. The reward stack X i k is the paper's $X_{i,k+1}$, mutually independent (iIndepFun), with arbitrary laws: no moment or support assumption. The randomization V takes values in an arbitrary measurable space and is independent of the stack. A policy is a family of jointly measurable decision rules of V and the history, so the comparator class contains every non-anticipating randomized policy. Pull counts reuse the published ImprovedLinBandits.UCBDelta.pullCount. Distribution functions are functions $\mathbb R\to\mathbb R$; $L$ is any submodule containing every indicator $\mathbb I_{[a,\infty)}$ and every distribution function, with a Seminorm (not a norm). The stability, smoothness and gap parameters are explicit arguments. A differential is any bounded linear functional with the quadratic bound, which determines it uniquely. U-UCB ties and the order of the initial pulls are broken by any non-anticipating rule. The paper's standing assumption that expectations exist is encoded as Borel measurability of $U$ and of the seminorm along empirical distributions; no integrability of rewards is assumed. Expectations of $L$-valued quantities are taken pointwise or after applying a functional, never as integrals in $L$. Logarithms are natural, and $\varphi$, $\varphi^{-1}$ and $D^{q-1}$ use Real.rpow.

The hypotheses are not vacuous. A verification file proves that a two-armed, non-degenerate instance satisfies stability, smoothness, the linear gap and the measurability assumption, and that it has an explicit U-UCB run.

A complete development needs: the measurability of the arm process; the unbiasedness argument under non-anticipation; tail-sum formulas for the moments; the UCB counting argument; and the corrected $3\beta$ cross-term estimate. The policy model and the empirical-distribution tail bounds are reusable for other bandit missions. Proofs of the milestones, and an independent statement of Theorem 3 at a constant Definition 2 supports, are welcome.

Selected references

• A. Cassel, S. Mannor, A. Zeevi, A General Framework for Bandit Problems Beyond Cumulative Objectives, arXiv:1806.01380v3, 2021; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1806.01380v3
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. https://arxiv.org/abs/1204.5721
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• A. W. van der Vaart, Asymptotic Statistics, Cambridge University Press, 2000. https://doi.org/10.1017/CBO9780511802256

Motivation

A transposition exchanges two neighboring stretches of a sequence without changing the order inside either stretch. In comparative genomics, such an operation models moving a contiguous sequence of genes to another position. When each gene occurs once, a genome can be represented by a permutation. The minimum number of transpositions needed to transform one ordering into another gives a measure of rearrangement distance. Bulteau, Fertin and Rusu study the computational difficulty of finding this minimum in Sorting by Transpositions is Difficult, §1.

The operation permits blocks of arbitrary positive lengths. Efficiently checking one proposed rearrangement does not settle the difficulty of finding a shortest sequence. The paper establishes that the associated decision problem is NP-hard. This mission formalizes that result and its intermediate statements using the supplied, pinned arXiv version, whose theorem numbering is used throughout.

Permutations, breakpoints and deletion systems

Fix a positive integer $n$. A sentinel permutation is a bijection $\pi$ of $\{0,\ldots,n\}$ with $\pi(0)=0$ and $\pi(n)=n$. For $0<i<j<k\le n$, the transposition $\tau_{i,j,k}$ exchanges the entries in the intervals $[i,j)$ and $[j,k)$. Applying a move means replacing $\pi$ by $\pi\circ\tau_{i,j,k}$. The transposition distance $d_t(\pi)$ is the minimum length of a sequence of such moves ending at the identity; an empty sequence is permitted. These are the conventions of Definitions 1–3, pp. 2–3.

An adjacency at position $x$, where $1\le x\le n$, means $\pi(x)=\pi(x-1)+1$. Every other such position is a breakpoint. Write $d_b(\pi)$ for their number, including the position adjacent to the final sentinel. The decision problem asks whether $d_t(\pi)\le k$ for a supplied integer budget $k$.

The paper also defines a 3DT-instance: a finite alphabet partitioned into oriented triples, with its symbols injected into the positions $1,\ldots,n$. Unoccupied positions are dots. A triple is well ordered if its cyclic orientation agrees with the increasing order of its occupied positions. A 3DT-step deletes that triple and transports all remaining positions by an associated inverse transposition. The span remains fixed. An instance is collapsible if some finite sequence of steps deletes every triple. These definitions include the empty alphabet and zero-step collapse (Definitions 4–9, pp. 4–6).

A block decomposition divides the positions into consecutive intervals. Variables pair two oriented triples distributed between distinct source and target blocks. Four concrete block words, called copy, and, or and var, specify local transition systems. Their names describe the activation behavior asserted by the paper; that behavior is not assumed in their definitions (§3, pp. 11–27).

Formalization targets

Let $S$ be the language of valid encodings of permutations and signed budgets that admit a sorting sequence within budget. The goal is the unconditional assertion

$$\forall A\text{ finite and nonempty},\quad \forall L\in\mathrm{NP}_A,\qquad L\le_p S.$$

Here $\le_p$ means polynomial-time many-one reducibility, with membership equivalence on every input word. This is Theorem 21, p. 34. It concerns every legal input permutation and every integer budget. It does not assume that SAT is NP-complete as an extra hypothesis.

The fifteen milestones retain the source's complete statements. Properties 3 and 4 describe adjacency preservation and the breakpoint lower bound. Property 6, Lemmas 7–8 and Theorem 9 concern the relation between a 3DT-instance and an equivalent permutation. In particular,

$$I\text{ collapsible}\quad\Longleftrightarrow\quad d_t(\pi)=|T|=d_b(\pi)/3.$$

Properties 12–13 describe changes to block membership and variable placement. Properties 14–17 specify the exact possible local activation orders of all four block types, including realizability. Lemma 18 asserts validity after any finite run from an assembling and collapsibility once no external variables remain. Theorems 19 and 20 retain both the semantic claims and the uniform polynomial running-time clauses for their concrete constructions (pp. 12–34).

Significance

NP-hardness classifies the difficulty of exact sorting by these moves: a polynomial algorithm for the full decision problem would provide polynomial algorithms for every language in NP. It does not by itself rule out approximation algorithms or efficient algorithms on restricted instances. The paper distinguishes these issues in its conclusion, p. 35.

The formalization supplies explicit definitions of block moves, fixed-span deletion systems, local activation graphs, assembling syntax and the two source constructions. These objects can support later work on sorting bounds and genome rearrangements. The mathematical result is established in the cited paper; the sixteen Lean theorem items are statements awaiting proofs. The existing platform SAT-completeness theorem remains an Open external dependency.

Difficulty

Counting breakpoints gives a lower bound, but does not generally determine the minimum number of moves. Nor does every deletion system admit an equivalent permutation: the paper explicitly gives an example without one on p. 10. Thus the claims about particular assemblings carry substantial content.

Faithful statements must distinguish local activation possibilities from restrictions imposed by a particular surrounding network. They must also retain the difference between variable placement and full variable validity. A construction with polynomial output length alone does not establish the running-time assertion. These distinctions require explicit transition rules, concrete constructors and a machine model with counted execution steps.

Formalization scope

Finite alphabets use injective natural-number labels; triple lists are duplicate-free and their enumeration is auxiliary. Assemblings allow arbitrary relabeling. Dot positions and the two sentinels remain present throughout. Distance is an infimum in the extended natural numbers, avoiding a default value on an empty feasible set; every legal source permutation is sortable and its finite minimum is attained. Breakpoint inequalities use multiplication by three, preserving exact division.

The sorting language uses a published self-delimiting binary-number encoder. Its code includes the entire permutation and a signed binary budget. Malformed codes and negative budgets reject. The SAT normalization handles empty conjunctions, empty clauses, repeated literals and sparse variable names. Two-leaf chains use one gate; single-variable feedback uses a direct wire. The final conjunction uses $\Gamma_\gamma$, the intended reading confirmed on p. 29 of the source.

Polynomial time uses the published CookPvsNP finite-alphabet Turing-machine definitions. Construction correctness is never included as a premise or data field. Contributions may establish the stated milestones and the structural facts needed to connect their concrete definitions, while preserving the full decision language and every clause of the source claims.

Selected references

• Laurent Bulteau, Guillaume Fertin and Irena Rusu, Sorting by Transpositions is Difficult. Supplied artifact: arXiv:1011.1157v1, 2010. Published as Sorting by Transpositions Is Difficult, SIAM Journal on Discrete Mathematics, 2012, DOI:10.1137/110851390. All theorem numbers and pages above refer to the supplied v1 artifact.

Why core pricing

Online ad platforms sell a limited number of lines of ad space to advertisers whose ads come in several shapes and sizes, so their preferences over the space are combinatorial and often complementary (Niazadeh et al., arXiv:1610.03564v4, §1). The Vickrey–Clarke–Groves auction can earn little revenue on such preferences. Core-selecting auctions (Ausubel and Milgrom 2006) keep the welfare-maximizing allocation and choose payments so that no group of bidders, together with the seller, would prefer to deviate.

The obstacle is computational. The core is cut out by one constraint for each coalition of bidders, and earlier work computes core outcomes with heuristics or with computationally intensive convex and linear programming methods, which are a poor fit for a real-time ad auction (§1, p.4). The paper's Theorem 1 replaces this with a simple deterministic algorithm that uses a winner determination routine as a black box. Its experiments on Bing auction data are out of scope for this mission.

Setting

There are $n$ bidders $N=\{1,\dots,n\}$ and $m$ items. A bid profile assigns each bidder $i$ a valuation $b_i$ on bundles of items, normalized by $b_i(\emptyset)=0$, with all values in $[0,1]$. No monotonicity is assumed. An allocation is a tuple of pairwise disjoint bundles $\{x_i\}_{i\in N}$, and $w(S)$ is the maximum of $\sum_i b_i(x_i)$ over allocations that give items only to agents in $S$.

A non-negative utility vector $\{\pi_i\}_{i\in N}$ is in the core if

$$w(N)-\sum_{i\in N}\pi_i\ \ge\ w(S)-\sum_{i\in S}\pi_i\qquad\text{for all } S\subseteq N.$$

The left side is the seller's revenue $\pi_0$. A vector $\pi$ is $\epsilon$-bidder optimal if it is in the core and no core point $\pi'\ge\pi$ exceeds $\pi$ by more than $\epsilon$ in some coordinate.

WIN-ORAC is the only access to the bids: given truncations $\pi$, it returns the maximum welfare $w(N,\{\max(b_i(.)-\pi_i,0)\})$ under the truncated bids, and a winning set. Algorithm 1 starts at $\pi=0$ with all bidders active, and repeatedly raises the utilities of the active bidders uniformly until a core constraint nearly binds. The subroutine Core-Search finds this point by bisection on $[0,1]$, up to $\epsilon/|S|$ per bidder. Bidders outside the next winning set are then frozen.

Formalization targets

Goal: Theorem 1

There are absolute constants $C_1,C_2>0$ such that for all $n,m$, every bid profile, every oracle meeting the specification, and every $\epsilon>0$, Algorithm 1 halts with an $\epsilon$-bidder optimal core point, having made at most

$$(n+1)+n\lceil\log_2(n/\epsilon)\rceil_+$$

oracle calls and spent additional time at most $n((2n+1)+n\lceil\log_2(n/\epsilon)\rceil_+)$. For $n\ge1$ and $\epsilon\le n/2$, these are at most $C_1\,n\log(n/\epsilon)$ and $C_2\,n^2\log(n/\epsilon)$.

Milestones, in the order of the paper's proof

1. Lemma 1 and the display in its proof: a core point and a maximum welfare allocation give a core outcome, and $\pi_i\le w(N)-w(N\setminus\{i\})\le b_i(x^*_i)$.
2. Lemma 2 and eq. (5): winners under truncated bids are most binding constraints, the converse, and the identity between the oracle's value and $\max_S(w(S)-\sum_S\pi_i)$. The resulting core test follows.
3. The Core-Search guarantee, and Proposition 1, Parts (1)–(3), with the persistence of $\epsilon$-tightness.
4. Lemma 3: at most $n$ iterations.
5. The certificate step and the two counts in the proof of Theorem 1.

Significance

The result gives a core point with $O(n\log(n/\epsilon))$ oracle calls, against $O((n/\epsilon)\log n)$ for Vaidya's cutting-plane method as the paper recounts on p.20, and it is a deterministic and combinatorial computation. The dependence on $\epsilon$ is what makes it usable in a time-sensitive auction. Lemma 2 is of independent use: it says a single winner determination call separates over the exponentially many core constraints.

The statement has not been machine-checked before. Formalizing it adds three things beyond the paper's proof. It fixes the algorithm as a defined transition system, with oracle calls and additional time counted at the call sites, so the complexity claim is a theorem about an actual run. It corrects statements that are false as printed: Proposition 1(1) and the second display on p.14 (the endpoint $\Delta_h=1$ is never tested, so $\bar\pi$ can be a core point), and the oracle count on p.20 (off by one, and without a ceiling). Theorem 1 itself survives these corrections. It also makes explicit which winner notion each bullet of Lemma 2 needs.

Difficulty

The arithmetic is short. The difficulty is in the invariants of the run. The natural argument says $\bar\pi$ leaves the core, so the next winner set must lose an active bidder; this fails exactly when $\Delta_h$ stays at its untested initial value $1$, and that case needs a separate argument through the bound $\pi_i\le b_i(x^*_i)$ and the zero-value convention. A second trap is the choice of winner set: an optimal allocation may hand out bundles of zero truncated value, and an oracle allowed to do so can keep the algorithm running forever. Finally, the invariants are joint: core membership, tightness of all recorded constraints, the identity $S_t=\bigcap_{t'<t}T_{t'}$ and the correctness of the stored value $w(N)$ have to be carried together along a run in which two nested loops alternate.

Formalization scope

Bidders are Fin n, bundles are Finset (Fin m), and $n=0$, $m=0$ are allowed. Allocations and welfare are the published ComplementFreeCA.CFRounding.IsAllocation and welfare. w is a Finset.sup', so it has no junk value. The core is stated through (3), with $\pi_0:=w(N)-\sum_i\pi_i$.

The oracle is a function q of the truncation, and "any set" on line 4 is a universal quantifier over q, constrained by IsWinOrac at $\pi\ge0$. The transition function step has no access to the bids, so the oracle count cannot be evaded, and the iteration count is not hard-wired: the loops are real. The field log is ghost. The return on line 11 is read as the else branch of line 6. Additional time is the counter ticks, with unit-cost operations. The hypothesis IsBidProfile must stay: $\Delta_h=1$ is valid only because values are in $[0,1]$.

IsWinOrac is satisfiable for every bid profile, so the goal is not vacuous; a trivial algorithm is excluded because the theorem is about this step.

A complete development needs invariants of the run, a bisection count, and elementary estimates on $\lceil\log_2\rceil$. Lemma 2 and the core test do not depend on the algorithm and may be reusable for other core-selecting rules. Definition 7, the dynamic program, §4 and the appendices are out of scope. Proofs of any milestone are welcome in any order, as are shorter routes through the invariants.

Selected references

• R. Niazadeh, J. Hartline, N. Immorlica, M. R. Khani, B. Lucier, Fast Core Pricing for Rich Advertising Auctions, preprint, 2020. https://arxiv.org/abs/1610.03564v4
• L. M. Ausubel, P. Milgrom, The Lovely but Lonely Vickrey Auction, in Combinatorial Auctions, MIT Press, 2006. https://doi.org/10.7551/mitpress/9780262033428.003.0002
• R. W. Day, S. Raghavan, Fair Payments for Efficient Allocations in Public Sector Combinatorial Auctions, Management Science 53(9), 2007. https://doi.org/10.1287/mnsc.1060.0662