Erdős Problem 338

### What is the conjecture

https://www.erdosproblems.com/338

The restricted order of a basis is the least integer $t$ (if it exists) such that every large integer is the sum of at most $t$ distinct summands from $A$. What are necessary and sufficient conditions that this exists? Can it be bounded (when it exists) in terms of the order of the basis? What are necessary and sufficient conditions that this is equal to the order of the basis?

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading the conjecture at https://www.erdosproblems.com/338 and inspecting related formalized conjectures in the formal-conjectures repository. Determine how its restricted-order definitions and questions should be represented in Lean; done means the conjecture has been added as a suitable formal statement.

Written by the indexing model from the issue text.