The two compressions of Lemma 2, and the closure theorem

• pChain p: chains b, b p, b p², … with p ∤ b;
• pqChain p q (p < q): chains b p^D, b p^(D-1) q, …, b q^D with p, q ∤ b.

Both satisfy the window condition Cons, so compression keeps every |A S t| from decreasing. Taking a compression-stable set of minimal element sum gives exists_closed, the content of Lemma 2 of the second proof.

noncomputable def RunsOfMultiples.pChain {p : ℕ} (hp : Nat.Prime p) : ChainSys ℕ

Chains along a single prime p.

Equations

• One or more equations did not get rendered due to their size.

theorem RunsOfMultiples.pChain_cons {p : ℕ} (hp : Nat.Prime p) (t b : ℕ) : (pChain hp).Cons t b

theorem RunsOfMultiples.pChain_div {p : ℕ} (hp : Nat.Prime p) {x : ℕ} (hx : 0 < x) (hpx : p ∣ x) : (pChain hp).vld ((pChain hp).key x) ((pChain hp).pos x - 1) ∧ (pChain hp).pos x - 1 < (pChain hp).pos x ∧ (pChain hp).elt ((pChain hp).key x) ((pChain hp).pos x - 1) = x / p

x / p sits one position below x on the p-chain of x.

theorem RunsOfMultiples.pow_mul_pow_mono {a b : ℕ} (hab : a ≤ b) {d u v : ℕ} (huv : u ≤ v) (hvd : v ≤ d) : a ^ (d - u) * b ^ u ≤ a ^ (d - v) * b ^ v

theorem RunsOfMultiples.pq_factorization {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) {b D u : ℕ} (hb : 0 < b) (hbp : ¬p ∣ b) (hbq : ¬q ∣ b) : (b * p ^ (D - u) * q ^ u).factorization p = D - u ∧ (b * p ^ (D - u) * q ^ u).factorization q = u

noncomputable def RunsOfMultiples.pqChain {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) : ChainSys (ℕ × ℕ)

Chains along a pair of primes p < q (fixed total exponent).

Equations

• One or more equations did not get rendered due to their size.

theorem RunsOfMultiples.pqChain_cons {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) (t : ℕ) (k : ℕ × ℕ) : (pqChain hp hq hpq).Cons t k

theorem RunsOfMultiples.pqChain_shift {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) {a : ℕ} (ha : 0 < a) (hqa : q ∣ a) : (pqChain hp hq hpq).vld ((pqChain hp hq hpq).key a) ((pqChain hp hq hpq).pos a - 1) ∧ (pqChain hp hq hpq).pos a - 1 < (pqChain hp hq hpq).pos a ∧ (pqChain hp hq hpq).elt ((pqChain hp hq hpq).key a) ((pqChain hp hq hpq).pos a - 1) = a / q * p

a / q * p sits one position below a on the (p, q)-chain of a.

theorem RunsOfMultiples.ChainSys.gap {κ : Type} [DecidableEq κ] {C : ChainSys κ} {T : Finset ℕ} (hT : ∀ n ∈ T, 0 < n) {n u : ℕ} (hn : n ∈ T) (hu : u < C.pos n) (hout : C.elt (C.key n) u ∉ T) : C.occ T (C.key n) ≠ Finset.range (C.occ T (C.key n)).card

If a chain has an occupied position pos n and an empty valid position below it, the chain's occupied set is not an initial segment.

theorem RunsOfMultiples.divClosed_of_step {T : Finset ℕ} (hT : ∀ n ∈ T, 0 < n) (hstep : ∀ x ∈ T, ∀ (p : ℕ), Nat.Prime p → p ∣ x → x / p ∈ T) : DivClosed T

One-step divisor closure implies divisor closure.

theorem RunsOfMultiples.exists_closed (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : ∃ (T : Finset ℕ), (∀ a ∈ T, 0 < a) ∧ T.card = S.card ∧ DivClosed T ∧ ShiftClosed T ∧ ∀ (t : ℕ), (A S t).card ≤ (A T t).card

Lemma 2: every finite set of positive integers can be replaced by a set of the same size, closed under divisors and under replacing a prime factor by a smaller prime, without decreasing any run count |A S t|.