Read-backs: attainment and comparison of optimal cover values

Throughout, the following notation is used for the objects the three statements refer to. $E$ and $S$ are two types (indices for elements and for sets, respectively), each carrying a finiteness assumption. For $s \in S$ we write $A_s \subseteq E$ for the finite subset of $E$ named by the first field of the bundled argument, and $c(s) \in \mathbb{R}$ for the real number named by its second field. For $e \in E$ we write

$$\mathrm{cont}(e) \;=\; \{\, s \in S \;:\; e \in A_s \,\},$$

the (finite) set of indices whose set contains $e$.

A cover is a finite subset $C \subseteq S$ such that every $e \in E$ satisfies $e \in A_s$ for at least one $s \in C$; its cost is $\sum_{s \in C} c(s)$, each member of $C$ counted once.

A fractional cover is an arbitrary real-valued function $x : S \to \mathbb{R}$ satisfying both

$$x(s) \ge 0 \ \ \text{for every } s \in S, \qquad \sum_{s \in \mathrm{cont}(e)} x(s) \ \ge\ 1 \ \ \text{for every } e \in E;$$

its cost is $\sum_{s \in S} c(s)\, x(s)$, summed over all of $S$, not merely over the support of $x$.

---

PrimalDualOnline.SetCover.exists_optIntegral

Binders, instances and the bundled argument. The statement quantifies over two implicitly given types $E$ and $S$ in arbitrary universes, and assumes four typeclass instances: $E$ is a finite type, $S$ is a finite type, equality on $E$ is decidable, and equality on $S$ is decidable. (The two decidability instances are what allow $\mathrm{cont}(e)$ to be formed as a finite subset of $S$ by filtering; they restrict the types only to the extent of requiring a decision procedure for equality.) There is then one explicit argument $I$, a bundled set-cover instance over $E$ and $S$, which packages exactly four things:

1. a family $A : S \to$ (finite subsets of $E$), i.e. $A_s$ for each $s$;
2. a cost function $c : S \to \mathbb{R}$;
3. a proof of nonnegativity of cost: $0 \le c(s)$ for every $s \in S$;
4. a proof of coverability: for every $e \in E$ there exists some $s \in S$ with $e \in A_s$.

Fields 3 and 4 are therefore hypotheses of the statement, carried inside $I$ rather than written as separate assumptions. The conclusion mentions only fields 1 and 2.

The conclusion. There exists a real number $v$ which is the least element of the set of achievable integral cover costs

$$V_{\mathrm{int}} \;=\; \Bigl\{\, w \in \mathbb{R} \;:\; \text{some cover } C \text{ satisfies } \textstyle\sum_{s \in C} c(s) = w \,\Bigr\}.$$

Expanded into its two component clauses, the assertion is that there is a $v \in \mathbb{R}$ with:

• (Membership / attainment.) There exists a finite subset $C_0 \subseteq S$ such that every element $e \in E$ belongs to $A_s$ for at least one $s \in C_0$, and

$$\sum_{s \in C_0} c(s) \;=\; v .$$

• (Lower bound.) For every finite subset $C \subseteq S$ with the property that every $e \in E$ belongs to $A_s$ for some $s \in C$,

$$v \;\le\; \sum_{s \in C} c(s).$$

1. Attainment vs. infimum vs. boundedness. The statement asserts attainment: a minimum. The membership clause says $v$ is itself the cost of an actual cover, and the lower-bound clause says no cover is cheaper. This is strictly more than asserting that an infimum exists, and strictly more than asserting that the set of cover costs is bounded below: the value is realized by a witness $C_0$. It is not phrased as a greatest-lower-bound property, and it does not assert that the minimizing $C_0$ is unique.

2. Provenance and load-bearing status of the two side conditions.

• Nonnegativity of cost ($0 \le c(s)$ for all $s$) is present, as field 3 of the bundled argument $I$, not as a loose hypothesis. Its role in this particular statement: the range of the quantifier in both clauses is the collection of finite subsets of $S$, and since $S$ is a finite type there are only finitely many such subsets, so $V_{\mathrm{int}}$ is a finite set of reals regardless of the signs of the $c(s)$. Dropping nonnegativity therefore does not make either clause unsatisfiable; with negative entries the least element would simply be a possibly negative number, attained at some cover that includes the cheap sets. In that sense the condition is not what makes this statement's two clauses hold.
• Every element lies in some set (coverability) is present, as field 4 of the bundled argument $I$. It bears on the membership clause. If it were dropped and some $e_0 \in E$ had $e_0 \notin A_s$ for every $s \in S$, then no finite $C \subseteq S$ could cover $e_0$, so $V_{\mathrm{int}}$ would be empty; the membership clause $v \in V_{\mathrm{int}}$ would then be unsatisfiable for every real $v$, and the existence claim would fail. The lower-bound clause, by contrast, would become vacuously true for every $v$ (there being no cover to compare against). The one situation in which dropping coverability changes nothing is $E$ empty, where coverability is vacuous anyway.

3. (Not applicable; this item concerns the comparison statement.)

4. Hypotheses relative to the comparison statement. This statement's assumptions are exactly the four typeclass instances and the single bundled argument $I$. It carries no hypothesis that the comparison statement lacks: the comparison statement has the identical prefix of binders and instances and the identical bundled argument, and then adds two real variables and two hypotheses about them. Nothing here is assumed about fractional covers, about a second value, or about the relationship between the two notions.

5. Degenerate cases silently included.

• $E$ empty. The covering condition is vacuous, so every finite $C \subseteq S$ — including $C = \emptyset$ — qualifies, and $V_{\mathrm{int}}$ contains $\sum_{s \in \emptyset} c(s) = 0$. Coverability (field 4) is vacuously satisfiable, so such instances exist for any $A$ and any nonnegative $c$.
• $S$ empty. Coverability demands an $s \in S$ for each $e \in E$, so a bundled instance with $S$ empty can exist only when $E$ is empty as well. In that case the only finite subset of $S$ is $\emptyset$ and $V_{\mathrm{int}} = \{0\}$.
• $c \equiv 0$. Nonnegativity holds; every cover has cost $0$, so $V_{\mathrm{int}} \subseteq \{0\}$ and the asserted $v$ is $0$, attained by any cover whatsoever.
• Individual zero-cost sets. Adding a set $s$ with $c(s) = 0$ to a cover leaves the cost unchanged, so the witness $C_0$ in the membership clause need not be minimal with respect to inclusion and need not be unique; the covering condition demands only that $C_0$ cover, never that every member of $C_0$ be needed.
• Unbounded entries. Not applicable here; the quantifier ranges over finite subsets of $S$, with no numerical entries.

What is NOT asserted. Nothing about fractional covers, linear-programming relaxations, duals or packings. No uniqueness: the claim is a bare existential over $v$, not a unique-existence claim, and no uniqueness of the attaining cover $C_0$ is claimed. No bound on the value — no upper bound, no lower bound such as $v \ge 0$, no relation to $\sum_{s \in S} c(s)$ or to any other quantity. No claim that $C_0$ is inclusion-minimal, of minimum cardinality, or computable, and no algorithm, procedure or complexity claim. Nothing about greedy or primal-dual constructions, about $\mathrm{cont}(e)$, about frequencies, or about approximation ratios. No statement that the value is positive, rational, or nonzero.

---