Erdős problem 349
For and any , is not a good pair: every term lies in the finite interval (since ), so every subset sum is bounded by the constant , and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the and integer-coefficient cases.
Sources
FormalConjectures/ErdosProblems/
349.lean
Retained formal statement
**The dyadic fiber at .** For every , the pair is good: the sequence is additively complete because at index it equals the exact power , so its range contains all powers of two, which already form an additively complete set. Uses monotonicity IsAddComplete.mono.
∀ (k : ℕ), Erdos349.IsGoodPair (1 / 2 ^ k) 2