---

Statement and complete proof

Use the coprime divisor setting of Lemma 4.3. If $V\subseteq T$, then

$$Q_N(V)=N\prod_{d\in V}\left(1-\frac1d\right) \ge N\prod_{d\in T}\left(1-\frac1d\right)=Q_N(T).$$

Every additional factor $1-1/d$ lies strictly between zero and one, so adjoining the elements of $T\setminus V$ cannot increase the product. Both displayed values of $Q_N$ are integers by the product-divides-$N$ fact in Lemma 4.3. This proves the assertion, including $V=\varnothing$.

The direction matters: fewer selected classes leave more points uncovered. This handles a hypothetical covering which uses only some of the divisors listed in a certificate.

Source and dependencies

Canonical v1, p. 6, §4.4, the named capacity_prod_relax input. The pinned Capacity.lean, lines 174–206, has the inequality in this direction. Its nearby prose saying that dropping members lowers the product is reversed; the formal statement and the proof above increase it. This is a wording correction, not a new capacity theorem.

Bears on

• Problem 7.