The compression proof: shared definitions

The compression proof (docs/first-missing-multiple.pdf) compresses S to a set T with the same cardinality and no fewer runs (|A S t| ≤ |A T t| for all t) that is

• (i) closed under divisors (DivClosed), and
• (ii) closed under replacing a prime factor q by a smaller prime p (ShiftClosed).

def RunsOfMultiples.DivClosed (T : Finset ℕ) : Prop

(i): every divisor of an element of T belongs to T.

Equations

• RunsOfMultiples.DivClosed T = ∀ a ∈ T, ∀ (d : ℕ), d ∣ a → d ∈ T

def RunsOfMultiples.ShiftClosed (T : Finset ℕ) : Prop

(ii): if a ∈ T, q ∣ a and p < q are primes, then a / q * p ∈ T.

Equations

• RunsOfMultiples.ShiftClosed T = ∀ a ∈ T, ∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → p < q → q ∣ a → a / q * p ∈ T