Read-back — set-cover declaration bundle (PrimalDualOnline.SetCover)

Ambient context shared by every declaration

Every declaration in this bundle is stated over two ambient types $E$ and $S$, each in an arbitrary universe, introduced by section-level binders together with three instance assumptions: $E$ is a finite type, $S$ is a finite type, and equality on $E$ is decidable. These are implicit arguments of each declaration that mentions the corresponding type. Six declarations additionally require decidable equality on $S$ as a further instance argument: containing, IsFractionalCover, frequency, maxFrequency, IsOptFractional, and indicator; the other declarations do not require it.

Throughout I write $A_s$ for the value at $s$ of the family named sets — a total function assigning to each index $s : S$ a finite subset $A_s \subseteq E$ — and $c_s$ for the value at $s$ of cost, a total function $S \to \mathbb{R}$. Nothing in the ambient context constrains either function: $A_s$ may be empty for some or all $s$, the sets may coincide or overlap arbitrarily, and $c_s$ may be zero, positive, or negative unless a particular declaration says otherwise. $C$ always denotes a finite subset of $S$, $x : S \to \mathbb{R}$ a weight on indices, $y : E \to \mathbb{R}$ a weight on elements, and $\rho$ a real number. Both $E$ and $S$ may be empty types; no declaration assumes either is nonempty, and no declaration relates their sizes.

All seventeen items in the file are definitions or one structure. There is no theorem and no lemma anywhere in the bundle: the file proves nothing and asserts nothing about any of the notions it introduces; it only introduces vocabulary. The file imports general tactic support, ordered-semiring big-operator lemmas over finite sets, and bounds on harmonic numbers, but no declaration mentions harmonic numbers, logarithms, set cardinalities $|A_s|$, or any numeric approximation factor; the only approximation-like quantity in the bundle is the free real parameter $\rho$ of IsGreedyCertificate, which that definition leaves entirely unconstrained.

---

containing

Given decidable equality on $S$ in addition to the ambient instances, a family $s \mapsto A_s$ of finite subsets of $E$, and an element $e : E$, this defines the finite subset of $S$

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

obtained by filtering the universal finite set of all indices (available because $S$ is assumed finite) by the predicate "$e$ belongs to $A_s$"; decidability of that predicate comes from decidable equality on $E$. The filtering ranges over the whole of $S$, not over any candidate subcollection, so this is the collection of all indices whose set contains $e$. It may be empty — exactly when $e$ lies in no $A_s$, which includes the case $S$ empty and the case where every $A_s$ is empty. No cost function appears, so no constraint on the sign of any cost is imposed, and the definition does not require that every element lie in some set: it merely records which indices, possibly none, contain $e$.

Coverable

Given a family $s \mapsto A_s$, this is the proposition

$$\forall\, e \in E,\ \exists\, s \in S,\ e \in A_s,$$

that every element of the ambient element type belongs to at least one member of the family; the existential ranges over all of $S$. This is the one predicate whose entire content is "every element lies in some set". It is purely propositional, built from finite-set membership, and uses no decidability beyond the ambient instances; no cost function appears, so nothing about the sign of any cost is constrained. Degenerate cases: if $E$ is empty the statement holds vacuously for any family, including the family sending every index to the empty set and including $S$ empty; if $E$ is nonempty and $S$ is empty, or more generally if some element belongs to no $A_s$, it is false. The existential is unweighted and says nothing about how many sets contain a given element.

NonnegCost

Given a cost function $s \mapsto c_s$ into the reals, this is the proposition

$$\forall\, s \in S,\ 0 \le c_s,$$

that every index has nonnegative cost. The inequality is non-strict, so zero-cost indices are permitted, including a cost identically zero; the statement is vacuously true when $S$ is empty. It concerns costs only: it says nothing about the family, nothing about coverage, and in particular does not require that every element lie in some set.

SetCoverInstance

This structure takes four parameters written out in its own signature: two explicit type arguments $E$ and $S$, and two instance arguments, finiteness of $E$ and finiteness of $S$. (It does not take decidable equality on $E$ or on $S$.) An inhabitant of $\mathrm{SetCoverInstance}(E, S)$ bundles exactly four components and nothing else:

1. sets — a total function from $S$ to finite subsets of $E$, i.e. the family $s \mapsto A_s$;
2. cost — a total function $S \to \mathbb{R}$, i.e. $s \mapsto c_s$;
3. cost_nonneg — a proof of $\mathrm{NonnegCost}(\mathrm{cost})$, unfolded: $0 \le c_s$ for every $s \in S$;
4. coverable — a proof of $\mathrm{Coverable}(\mathrm{sets})$, unfolded: every $e \in E$ belongs to $A_s$ for at least one $s \in S$.

So an inhabitant is a finite element type, a finite index type, a set family over them, a real cost per index, a nonnegativity guarantee for all costs, and a coverability guarantee for all elements. There is no requirement that the sets be nonempty or pairwise distinct, no cardinality or frequency bound, no strict positivity of costs (only nonnegativity), and no stored optimum. If $E$ is empty the coverability field is vacuous, so inhabitants exist for any family with any nonnegative cost; if $S$ is empty the cost field's condition is vacuous and an inhabitant exists precisely when $E$ is also empty, the coverability field being otherwise unsatisfiable; a cost identically zero yields legitimate inhabitants.

Whether the structure is consumed in this file. Checking every other declaration one by one: containing takes a bare family and an element; Coverable a bare family; NonnegCost a bare cost; IsCover a bare family and $C$; coverCost a bare cost and $C$; IsFractionalCover a bare family and $x$; fractionalCost a bare cost and $x$; IsDualPacking a bare family, a bare cost and $y$; packingValue only $y$; frequency a bare family and an element; maxFrequency a bare family; IsOptIntegral a bare family, a bare cost and a real $v$; IsOptFractional a bare family, a bare cost and a real $v$; indicator only $C$; IsGreedyCertificate a bare family, a bare cost, $C$, $y$ and $\rho$; IsPrimalDualCertificate a bare family, a bare cost, $C$ and $y$. No declaration in this file takes a SetCoverInstance as an argument, and none projects any of its four fields. The dependency runs only inward: the structure's field types mention NonnegCost and Coverable, and those two predicates are themselves used nowhere else in the file. Within this file the structure is therefore inert — defined and never consumed. In particular the cost nonnegativity and the coverability it packages are not transported into any other definition here; every other definition either requires such a hypothesis separately or does not require it at all.

IsCover

Given a family $s \mapsto A_s$ and a finite subset $C \subseteq S$, this is the proposition

$$\forall\, e \in E,\ \exists\, s \in C,\ e \in A_s,$$

that every element of $E$ belongs to at least one set indexed by a member of $C$. The existential is restricted to $C$, unlike Coverable, where it ranges over all of $S$. This is the "every element lies in some set" condition localised to $C$. No cost function occurs, so no sign constraint on costs is imposed or implied. Degenerate cases: if $E$ is empty the statement holds for every $C$, including $C = \varnothing$ and including $S$ empty; if $E$ is nonempty then $C = \varnothing$ makes it false, the inner existential over an empty collection being false, and likewise if $S$ is empty. Multiplicity is irrelevant — an element covered by many members of $C$ satisfies the condition exactly as one covered by a single member — and there is no minimality, irredundancy, or distinctness requirement on $C$.

coverCost

Given a cost function $s \mapsto c_s$ and a finite subset $C \subseteq S$, this is the real number

$$\mathrm{coverCost}(c, C) \;=\; \sum_{s \in C} c_s,$$

a plain finite sum over the members of $C$, counting each member once regardless of how many elements it covers. It is defined for every finite subset $C$, whether or not $C$ covers anything: no coverage condition appears, so it does not require that every element lie in some set. It imposes no sign condition on cost — with negative $c_s$ the value may be negative, and enlarging $C$ may decrease the total. If $C$ is empty (in particular if $S$ is empty, forcing $C$ empty) the value is the empty sum $0$; if the cost is identically zero the value is $0$ for every $C$; zero-cost indices contribute nothing and may be added to or removed from $C$ without changing the value.

IsFractionalCover

Given decidable equality on $S$, a family $s \mapsto A_s$, and a weight vector $x : S \to \mathbb{R}$, this is the conjunction of two conditions:

$$\bigl(\forall\, s \in S,\ 0 \le x_s\bigr) \quad\text{and}\quad \Bigl(\forall\, e \in E,\ 1 \le \sum_{s \,:\, e \in A_s} x_s\Bigr),$$

where the inner sum ranges over $\mathrm{containing}(A,e)$ — that is, over all indices of the whole type $S$ whose set contains $e$, with containing unfolded. So the weights are nonnegative and, for each element, the total weight of the sets containing it is at least $1$. The sign constraint here is on $x$, not on cost: no cost function is an argument, so the definition neither assumes nor implies anything about the sign of any cost. The second clause is the fractional analogue of "every element lies in some set" and does entail it: if some $e$ belonged to no $A_s$, its sum would be the empty sum $0$ and $1 \le 0$ would fail. There is no upper bound of $1$ on the weights — $x_s$ may exceed $1$, may be arbitrarily large, the per-element covering sums may far exceed $1$, and $\sum_s x_s$ is unbounded. Degenerate cases: if $E$ is empty the second clause is vacuous and the condition reduces to nonnegativity of $x$ alone, so $x \equiv 0$ qualifies; if $S$ is empty, or more generally if some element lies in no set, the second clause is unsatisfiable whenever $E$ is nonempty, so no $x$ qualifies; the zero vector qualifies only when $E$ is empty.

fractionalCost

Given a cost function $s \mapsto c_s$ and a weight vector $x : S \to \mathbb{R}$, this is the real number

$$\mathrm{fractionalCost}(c, x) \;=\; \sum_{s \in S} c_s\, x_s,$$

a sum over the entire index type $S$ (legitimate because $S$ is finite), not over a subcollection and not over the support of $x$. No hypothesis restricts $x$ or $c$: the definition applies to arbitrary real vectors, so it does not assume nonnegative cost, does not assume nonnegative weights, imposes no coverage requirement, and its value may be negative. If $S$ is empty the value is $0$; if the cost is identically zero the value is $0$ for every $x$; an index of zero cost contributes nothing however large its weight, and an index of zero weight contributes nothing however large its cost.

IsDualPacking

Given a family $s \mapsto A_s$, a cost function $s \mapsto c_s$, and an element weighting $y : E \to \mathbb{R}$, this is the conjunction

$$\bigl(\forall\, e \in E,\ 0 \le y_e\bigr) \quad\text{and}\quad \Bigl(\forall\, s \in S,\ \sum_{e \in A_s} y_e \;\le\; c_s\Bigr):$$

the element weights are nonnegative, and for every index — all of $S$, not merely some subcollection — the total weight of the elements of $A_s$ does not exceed that index's cost. The definition does not assume nonnegative cost but it implies it: for each $s$, the sum $\sum_{e \in A_s} y_e$ is a finite sum of nonnegative terms by the first clause, so $0 \le \sum_{e \in A_s} y_e \le c_s$ and hence $0 \le c_s$ for every $s$; any $y$ satisfying this condition therefore witnesses $\mathrm{NonnegCost}(c)$, and the condition is unsatisfiable whenever some cost is negative. It does not require that every element lie in some set: an element belonging to no $A_s$ is constrained only by $0 \le y_e$ and may carry arbitrarily large weight. Degenerate cases: if $E$ is empty every $A_s$ is empty, each sum is $0$, and the condition reduces to $0 \le c_s$ for all $s$; if $S$ is empty the second clause is vacuous and the condition reduces to nonnegativity of $y$; if $A_s = \varnothing$ for a particular $s$ that index's constraint reduces to $0 \le c_s$; if $c_s = 0$ for some $s$ — in particular if the cost is identically zero — then with $y \ge 0$ the constraint forces $y_e = 0$ for every $e \in A_s$.

packingValue

Given an element weighting $y : E \to \mathbb{R}$, this is the real number

$$\mathrm{packingValue}(y) \;=\; \sum_{e \in E} y_e,$$

the sum of the weights over the entire element type, using finiteness of $E$. It takes no family and no cost, so it constrains neither the sign of cost nor coverage, and it does not require $y$ to be nonnegative — on an arbitrary real vector its value may be negative. If $E$ is empty the value is the empty sum $0$. Every element of $E$ is counted, including elements belonging to no set of the family.

frequency

Given decidable equality on $S$, a family $s \mapsto A_s$, and an element $e : E$, this is the natural number

$$f_A(e) \;=\; \bigl|\{\, s \in S \;:\; e \in A_s \,\}\bigr|,$$

the cardinality of $\mathrm{containing}(A,e)$ — the number of indices of the whole type $S$ whose set contains $e$. Being a natural number it is automatically nonnegative, and it equals $0$ exactly when $e$ belongs to no set of the family, in particular when $S$ is empty or when every $A_s$ is empty. No cost appears, so there is no constraint on the sign of any cost, and the definition does not require that every element lie in some set — the value $0$ is precisely the record of an element that lies in none.

maxFrequency

Given decidable equality on $S$ and a family $s \mapsto A_s$, this is the natural number

$$\Delta(A) \;=\; \sup_{e \in E} f_A(e) \;=\; \max_{e \in E}\, \bigl|\{\, s \in S : e \in A_s \,\}\bigr|,$$

the supremum, taken over the universal finite set of all elements of $E$, of the frequencies above. Because it is a finite supremum in the naturals, whose least element is $0$, an empty supremum takes the value $0$ rather than being undefined. It is a natural number, hence nonnegative by type; no cost function appears, so there is no constraint on the sign of any cost; and it does not require that every element lie in some set.

When it is $0$. Exactly when every element has frequency $0$, i.e. when no element of $E$ lies in any $A_s$. Concretely: (i) $E$ empty — the supremum is over an empty range and takes its default value $0$, for any family whatsoever, including $S$ empty; (ii) $S$ empty with $E$ arbitrary, since then no index exists to contain anything; (iii) $S$ nonempty but $A_s = \varnothing$ for every $s$. Cases (ii) and (iii) with $E$ nonempty are exactly the failure of Coverable, so a coverable family over a nonempty $E$ has $\Delta(A) \ge 1$ — though the file states no such connection.

What the declarations mentioning it reduce to. No other declaration in the file mentions maxFrequency: no definition's body refers to it, and the free parameter $\rho$ of IsGreedyCertificate is never tied to it or to any frequency. Within this file maxFrequency is defined and unused, so the $\Delta(A) = 0$ cases affect nothing else in the bundle. Correspondingly frequency is used only inside maxFrequency, and containing is used only inside frequency and in the covering clause of IsFractionalCover.

IsOptIntegral

Given a family $s \mapsto A_s$, a cost function $s \mapsto c_s$, and a real number $v$, this asserts that $v$ is the least element of the set of achievable cover costs:

$$v \;=\; \min\;\Bigl\{\, w \in \mathbb{R} \;:\; \exists\, C \subseteq S \text{ finite},\ \bigl(\forall e \in E,\ \exists s \in C,\ e \in A_s\bigr) \wedge \textstyle\sum_{s \in C} c_s = w \,\Bigr\},$$

with the cover condition and the cost sum unfolded. "Least element" is a two-part condition: $v$ is itself achieved by some covering collection (membership in the set) and $v \le w$ for every achievable cover cost $w$ (lower bound); both halves matter, so the optimum must be attained rather than merely approached. The definition does not assume nonnegative cost and does not imply it: with negative costs a least element still exists whenever any cover exists, since $S$ is finite and so only finitely many values are achievable; the optimum may then be negative and may be attained by a redundant $C$ whose extra negative-cost members lower the total. It does require, for satisfiability, that every element lie in some set: if no $C \subseteq S$ covers $E$ the defining set is empty and no real $v$ satisfies the condition, so the predicate is then unsatisfiable. Degenerate cases: if $E$ is empty every $C$ is a cover, so $v$ is the minimum of $\sum_{s\in C} c_s$ over all finite subsets of $S$ — which is $0$ when all costs are nonnegative and otherwise the sum of the negative costs; if $S$ is empty the only candidate is $C = \varnothing$, so the predicate holds exactly at $v = 0$ when $E$ is empty and for no $v$ when $E$ is nonempty; if the cost is identically zero the predicate holds exactly at $v = 0$ provided some cover exists, and for no $v$ otherwise; zero-cost indices may be added freely to an optimal $C$ without changing $v$.

IsOptFractional

Given decidable equality on $S$, a family $s \mapsto A_s$, a cost function $s \mapsto c_s$, and a real number $v$, this asserts that $v$ is the least element of the set of achievable fractional-cover costs:

$$v \;=\; \min\;\Bigl\{\, w \in \mathbb{R} \;:\; \exists\, x : S \to \mathbb{R},\ \bigl(\forall s,\ 0 \le x_s\bigr) \wedge \Bigl(\forall e,\ 1 \le \textstyle\sum_{s : e \in A_s} x_s\Bigr) \wedge \textstyle\sum_{s \in S} c_s x_s = w \,\Bigr\},$$

with the fractional-cover condition and the cost functional unfolded. Again "least element" means both that $v$ is attained by some feasible $x$ and that $v \le w$ for every feasible value, so this asserts that the infimum is achieved, not merely that it is a lower bound. Weights are required nonnegative but are not bounded above by $1$; arbitrarily large weights are feasible. The definition does not assume nonnegative cost but implies it whenever it holds: suppose $c_{s_0} < 0$ for some $s_0$; the predicate requires the value set to be nonempty, so some feasible $x$ exists, and for every $t \ge 0$ the vector $x + t\,\mathbf{1}_{s_0}$ is still feasible — nonnegativity is preserved and each element's covering sum only increases — with cost $\sum_s c_s x_s + t\,c_{s_0} \to -\infty$ as $t \to \infty$; the value set is then unbounded below and has no least element, a contradiction. Hence $\mathrm{IsOptFractional}$ holding for some $v$ forces $0 \le c_s$ for all $s$. It likewise requires, for satisfiability, that every element lie in some set, since otherwise no feasible $x$ exists (an uncovered element's covering sum is the empty sum $0 \not\ge 1$) and the value set is empty. Degenerate cases: if $E$ is empty, feasibility reduces to $x \ge 0$, so with nonnegative costs $x \equiv 0$ is feasible and the predicate holds exactly at $v = 0$, while with some negative cost it holds for no $v$ by the unboundedness argument; if $S$ is empty it holds exactly at $v = 0$ when $E$ is empty and for no $v$ when $E$ is nonempty; if the cost is identically zero it holds exactly at $v = 0$ provided some feasible $x$ exists; a single zero-cost index may carry unbounded weight at no cost.

indicator

Given decidable equality on $S$ and a finite subset $C \subseteq S$, this is the function $S \to \mathbb{R}$

$$\mathbf{1}_C(s) \;=\; \begin{cases} 1 & \text{if } s \in C,\\ 0 & \text{if } s \notin C,\end{cases}$$

a real-valued $0/1$ vector on the index type; the decidable-equality-on-$S$ instance is what makes the membership test $s \in C$ decidable. It takes no family and no cost, so it constrains neither the sign of cost nor coverage. If $C$ is empty — in particular if $S$ is empty — the function is identically $0$. No declaration in this file applies indicator to anything: it appears neither in IsFractionalCover nor in IsOptFractional nor anywhere else, and the file contains no statement relating $\mathbf{1}_C$ to fractional covers or relating coverCost to fractionalCost. Within this file it is inert.

IsGreedyCertificate

Given a family $s \mapsto A_s$, a cost function $s \mapsto c_s$, a finite subset $C \subseteq S$, an element weighting $y : E \to \mathbb{R}$, and a real number $\rho$ — five explicit arguments, together with the ambient implicit type and instance arguments — this is the conjunction of four conditions:

1. $C$ is a cover: every $e \in E$ lies in $A_s$ for some $s \in C$;
2. $y$ is nonnegative: $0 \le y_e$ for every $e \in E$;
3. exact cost matching: $\displaystyle \sum_{s \in C} c_s \;=\; \sum_{e \in E} y_e$, the cost of $C$ equalling (not merely bounding) the total element weight, the right-hand sum being over all of $E$;
4. $\rho$-relaxed dual feasibility: $\displaystyle \sum_{e \in A_s} y_e \;\le\; \rho\, c_s$ for every $s \in S$.

The parameter $\rho$ is an arbitrary real: the definition places no constraint on it — it need not be positive, need not be at least $1$, and is not related to $\mathrm{maxFrequency}$ or to any other quantity in the file. The definition does not assume nonnegative cost; what it implies depends on $\rho$, since clauses 2 and 4 give $0 \le \sum_{e \in A_s} y_e \le \rho\,c_s$ and hence $0 \le \rho\,c_s$ for every $s$. Thus if $\rho > 0$ it implies $0 \le c_s$ for all $s$; if $\rho < 0$ it implies $c_s \le 0$ for all $s$, so only families with all costs nonpositive admit a certificate with negative $\rho$; and if $\rho = 0$, clause 4 becomes $\sum_{e \in A_s} y_e \le 0$ for every $s$, which with clause 2 forces $y_e = 0$ for every element lying in any $A_s$, whereupon clause 1 — which places every element of $E$ in some $A_s$ with $s \in C$ — forces $y \equiv 0$ on all of $E$, so the right-hand side of clause 3 is $0$ and the predicate collapses to: $C$ covers $E$, $y$ is identically zero, and $\sum_{s \in C} c_s = 0$ (individual member costs may be nonzero and cancel). Clause 1 is the "every element lies in some set" requirement, localised to $C$. Further degenerate cases: if $E$ is empty, clause 1 holds for every $C$, clause 3 reduces to $\sum_{s\in C} c_s = 0$ (its right side an empty sum), and clause 4 to $0 \le \rho\,c_s$ for all $s$; if $C$ is empty and $E$ nonempty, clause 1 fails; if both are empty, clause 3 reads $0 = 0$; if $S$ is empty, clause 4 is vacuous and clauses 1 and 3 force $E$ empty with nothing required of $y$ beyond nonnegativity; if $c_s = 0$ for a particular $s$, clause 4 forces $y_e = 0$ for every $e \in A_s$ whatever $\rho$ is; if the cost is identically zero then, given clause 1, the predicate holds precisely when $y \equiv 0$, for every covering $C$ and every $\rho$. No clause asserts any relation between $\sum_{s\in C} c_s$ and any optimum: the definition mentions neither IsOptIntegral nor IsOptFractional, and nothing in the file connects them.

IsPrimalDualCertificate

Given a family $s \mapsto A_s$, a cost function $s \mapsto c_s$, a finite subset $C \subseteq S$, and an element weighting $y : E \to \mathbb{R}$ — four explicit arguments plus the ambient implicit and instance arguments — this is the conjunction of three conditions:

1. $C$ is a cover: every $e \in E$ lies in $A_s$ for some $s \in C$;
2. $y$ is a dual packing for the family and the cost, i.e. IsDualPacking unfolded: $0 \le y_e$ for every $e \in E$, and $\displaystyle \sum_{e \in A_s} y_e \le c_s$ for every $s \in S$ — the bound holding at all indices, with coefficient exactly $1$;
3. tightness on the chosen collection: $\displaystyle \sum_{e \in A_s} y_e \;=\; c_s$ for every $s \in C$, each selected index's constraint being met with equality.

There is no clause equating $\sum_{s \in C} c_s$ with $\sum_{e \in E} y_e$: unlike IsGreedyCertificate, this definition mentions neither packingValue nor coverCost, and it asserts no inequality against any optimum. It does not assume nonnegative cost but implies it, exactly as in IsDualPacking: each $\sum_{e \in A_s} y_e$ is a sum of nonnegative terms, so $0 \le c_s$ for every $s \in S$ (not only for $s \in C$), and the predicate is unsatisfiable when any cost is negative. Clause 1 is the "every element lies in some set" requirement, localised to $C$. Degenerate cases: if $E$ is empty, clause 1 is vacuous and every $A_s$ is empty, so clause 2 reduces to $0 \le c_s$ for all $s$ while clause 3 forces $c_s = 0$ for every $s \in C$ — with $E$ empty only zero-cost indices may appear in $C$; if $C$ is empty, clause 3 is vacuous and clause 1 requires $E$ empty; if $S$ is empty, clauses 2 and 3 are vacuous and clause 1 requires $E$ empty; if $A_s = \varnothing$ for some $s \in C$, clause 3 forces $c_s = 0$; if $c_s = 0$ for some $s$, clause 2 with nonnegativity forces $y_e = 0$ throughout $A_s$, and when such an $s$ lies in $C$ clause 3 is then automatic; if the cost is identically zero, the predicate holds precisely when $C$ covers $E$ and $y$ vanishes on $\bigcup_s A_s$, which by clause 1 is all of $E$, so $y \equiv 0$.

---

Cross-cutting summary

Sign of cost, declaration by declaration. Assumed outright: NonnegCost (its whole content) and the cost_nonneg field of SetCoverInstance. Implied without being assumed: IsDualPacking and IsPrimalDualCertificate, where a nonnegative $y$ bounded above by $c_s$ gives $0 \le c_s$ for every $s \in S$; IsOptFractional, where a negative cost makes the feasible value set unbounded below so that no least element can exist; and IsGreedyCertificate conditionally on $\rho$ — $\rho > 0$ gives $c \ge 0$ everywhere, $\rho < 0$ gives $c \le 0$ everywhere, and $\rho = 0$ gives no sign information but forces $y \equiv 0$ and $\sum_{s \in C} c_s = 0$. Neither assumed nor implied: containing, Coverable, IsCover, coverCost, IsFractionalCover (which constrains the sign of $x$ instead), fractionalCost, packingValue, frequency, maxFrequency, IsOptIntegral, indicator.

"Every element lies in some set", declaration by declaration. Asserted over all of $S$: Coverable. Asserted over the given collection $C$: IsCover, and clause 1 of both IsGreedyCertificate and IsPrimalDualCertificate. Asserted in a fractional form that entails it: IsFractionalCover, and hence the feasibility condition inside IsOptFractional. Required only for satisfiability, via the existential over covers: IsOptIntegral and IsOptFractional are false for every $v$ when no cover, respectively no fractional cover, exists. Not required at all: containing, NonnegCost, coverCost, fractionalCost, IsDualPacking (elements in no set are constrained only by $y_e \ge 0$), packingValue, frequency, maxFrequency, indicator. Packaged as a field: SetCoverInstance, through coverable.

Nature of the coverage relation. Coverage is not a separately declared $\mathrm{Prop}$-valued relation on $S \times E$; it is finite-set membership $e \in A_s$, where $A_s$ is the finite subset of $E$ produced by the total function sets. Membership in a finite subset is a proposition, and the quantified statements built from it — Coverable, IsCover, and the clauses of both certificate predicates — are ordinary propositions requiring no decidability. Decidability is needed only where membership must be computed into data: forming $\mathrm{containing}(A,e)$ by filtering the universal finite set of $S$ needs the membership predicate to be decidable, which follows from decidable equality on $E$, and needs $S$ finite; indicator needs decidability of $s \in C$ for a finite subset of $S$, which follows from decidable equality on $S$. Decidable equality on $S$ is demanded as an extra instance argument by containing, frequency, maxFrequency, IsFractionalCover, and IsOptFractional. Every sum or supremum over a whole type — $\sum_{s \in S}$ in fractionalCost, $\sum_{e \in E}$ in packingValue, the supremum over $E$ in maxFrequency, the filter over $S$ in containing — relies on the ambient finiteness instances.

Degenerate cases across the bundle. $E$ empty: Coverable and IsCover hold for every family and every $C$; IsFractionalCover reduces to $x \ge 0$; packingValue and every sum over $E$ is $0$; maxFrequency is $0$; IsDualPacking reduces to $0 \le c_s$ for all $s$; IsPrimalDualCertificate forces $c_s = 0$ for every $s \in C$; IsGreedyCertificate reduces to $\sum_{s\in C} c_s = 0$ together with $0 \le \rho\,c_s$; IsOptIntegral becomes the minimum of $\sum_{s\in C} c_s$ over all subsets of $S$; IsOptFractional holds exactly at $v = 0$ when costs are nonnegative. $S$ empty: $\mathrm{containing}$ is empty, all frequencies and maxFrequency are $0$, coverCost and fractionalCost are $0$, Coverable, IsCover and IsFractionalCover are unsatisfiable unless $E$ is empty, and both optimality predicates hold only at $v = 0$ with $E$ empty. $C$ empty: coverCost is $0$; IsCover holds only if $E$ is empty; the tightness clause of IsPrimalDualCertificate is vacuous; IsGreedyCertificate requires $\sum_{e \in E} y_e = 0$. Cost identically zero: permitted by NonnegCost and by SetCoverInstance; makes every coverCost and fractionalCost zero; forces $y$ to vanish on all covered elements in IsDualPacking, IsGreedyCertificate and IsPrimalDualCertificate; both optima equal $0$ when feasible. Individual zero-cost indices: forced by IsDualPacking to have $y_e = 0$ throughout $A_s$; addable to or removable from $C$ without changing coverCost; able to carry unbounded fractional weight at no cost in IsFractionalCover and IsOptFractional; automatically satisfying the tightness clause of IsPrimalDualCertificate once $y$ vanishes on $A_s$. $\rho$ zero or negative: both permitted by IsGreedyCertificate, with the consequences above — $\rho = 0$ collapsing the certificate to a zero dual and a zero-total-cost cover, $\rho < 0$ requiring all costs nonpositive. Weights above $1$ in a fractional cover: permitted without restriction, IsFractionalCover imposing only $x_s \ge 0$ and a lower bound of $1$ on each element's covering sum, with no upper bound on any $x_s$, on any covering sum, or on $\sum_s x_s$.