bibkey: shannon2023a363956 authors: Scott R. Shannon year: 2023 title: OEIS A363956 — least unused multiples indexed by distinct prime factors doi: null url: https://oeis.org/A363956 claim: The entry conjectures that its greedy sequence is a permutation of the positive integers. strata_touched:

• D5/S3/Arith/OmegaGreedyPermutation license: citation-only triage: anchor

OEIS A363956

The seeds are 1 and 2. Each subsequent term is the smallest positive unused multiple of the omega-th prime, where omega counts the distinct prime factors of the preceding term. The entry explicitly conjectures that every positive integer occurs. It records a(210667)=17; this finite observation does not prove or refute the conjecture.

Verified locator

doi: null url: https://oeis.org/A363956

Revision 10 of https://oeis.org/A363956/internal, dated July 1, 2023, labels the permutation claim a conjecture without a proof. The related entries https://oeis.org/A363504/internal and https://oeis.org/A351495/internal also state their permutation claims as conjectures. A363504 counts factors with multiplicity; A351495 selects the smallest prime absent from the preceding term. Neither variant is formalized here.

Proof scope

Mathlib supplies prime enumeration, prime supports, finite images and finite-fiber arguments. The queue-exhaustion proof is a repository derivation; no publication priority is claimed.

Repository derivation

An infinitely selected prime queue exhausts its positive multiples: a missing multiple would bound all those distinct outputs in a finite interval. If queue 2 were selected only finitely often, there would be only finitely many prime outputs. Every selected prime has appeared or is immediately output, so the queue range would be finite. Some queue would be selected infinitely often, making the distinct-prime-factor counts unbounded, a contradiction. Thus every positive even number appears. Infinitely many even numbers have each fixed positive number of distinct prime factors, so every prime queue is selected infinitely often. Prime divisors then give all integers greater than one. The seed supplies one. The Lean sequence is defined by the original minimum rule, and its full forbidden history and injectivity are proved separately.

Unverified scope

The linked term files, plots, revision histories and cross-references beyond the two explicitly read neighbors were not opened (ASSUMED-UNVERIFIED). The user’s 200000-term computation was not rerun or used as proof evidence. No claim is made about fixed points, growth rates or the Omega variant.