Lemma II.1 — $a_i + b_i \ge 0$ along the run of Algorithm 1

Let $\mathcal N$ be a finite ground set, $f : 2^{\mathcal N} \to \mathbb R$ a submodular function, i.e. $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$, and $u_1, \dots, u_n$ an enumeration of $\mathcal N$ (each element exactly once). Run Algorithm 1 (DeterministicUSM) in this order, producing the states $(X_i, Y_i)$, and let

be the two marginal gains the algorithm compares in iteration $i$. Then for every $1 \le i \le n$,

In words, in every iteration at least one of the two options (adding $u_i$ to $X$, removing $u_i$ from $Y$) does not decrease the value of its solution. The lemma is used in the proof of Lemma II.2.

Formalization Note The element $u_i$ is l[i - 1] and the state before iteration $i$ is state f l (i - 1). Nonnegativity of $f$ is not needed and is not assumed. The paper's submodularity sentence in the introduction ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") is a slip, since for $u \in B \setminus A$ it would force monotonicity; the formalization uses the equivalent lattice form of the paper's footnote 1, via the referenced definition NonmonotoneSubmod.Shared.Submodular.