Finite subset selection for the residue cover. A minimal modulus crosses its target by at most one prime factor. A change of containment then occurs across a single deletion edge.

theorem CCDN.exists_minimal_product_subset (P : Finset ℕ) {X U : ℝ} (hX : 1 < X) (hP : ∀ p ∈ P, 0 < ↑p) (hU : ∀ p ∈ P, ↑p ≤ U) (hprod : X ≤ ∏ p ∈ P, ↑p) : ∃ R ⊆ P, R.Nonempty ∧ X ≤ ∏ p ∈ R, ↑p ∧ (∀ T ⊂ R, ∏ p ∈ T, ↑p < X) ∧ ∏ p ∈ R, ↑p < U * X

If a finite set P of positive integers bounded by U has product at least X > 1, then it contains a nonempty subset R with product at least X and less than U X, all of whose proper subsets have product less than X.

theorem CCDN.exists_subset_erase_boundary {α : Type u_1} [DecidableEq α] (R : Finset α) (W : Finset α → Prop) (hempty : ¬W ∅) (hR : W R) : ∃ T ⊆ R, ∃ p ∈ T, W T ∧ ¬W (T.erase p)

Any property false at the empty node and true at a terminal node changes across a one-element subset edge.