Define f:S -> D by induction:
f(s0) = 0, f(s1) = 1
and for k > 1, let
bk = max { sj | j < k, sj < sk }
tk = min { sj | j < k, sk < sj }
f(sk) = (f(bk) + f(tk))/2
It can be show that f is an increasing injection.
Now assume that S is dense,
.. . ie for all a,b in S, some x in S with a < x < b.
Assume also f(sj) = (p-1)/2^m, f(sk) = p/2^m, p,m in N.
As sj < sk, there's some n with sn = s_n in (sj,sk).
Let n = min{ n | sn in (sj,sk) }.
Problem: how to prove j,k < n. I doubt there's a counter example.
----
The following seems to produce a proof:
Consider the infinite binary tree T associated with the
partially ordered set of dyadic subintervales of [0,1). That
is, [0,1) is the root; [0,1/2) and [1/2,1) are its offspring;
[0,1/4) and [1/4,1/2) are the offspring of [0,1/2), etc.
Label all the nodes of T with the midpoint of the associated
interval: 1/2 at the root, 1/4 and 3/4 its offspring, etc.
Your recursive definition of f associates s2 with 1/2 (the label
of the root), s3 with either 1/4 or 3/4 (the label of one of its
offspring), etc. We can then think of f as taking S to nodes of T.
Step 1: verify (by induction) the sort of obvious fact that the
node f(sk) is the offspring of f(sj) for some j < k.
We can therefore think of f as building subtrees T_n of T, with
T_n obtained by attaching one offspring f(sn) to a node of
T_{n-1}.
Arrange T into levels, where the root is level 1 and level m
is labeled with all odd multiples of 2^m.
Now suppose p is even but not equal to 2^m. Then (p-1)/2^m
labels a node at level m and p/2^m will be at an earlier level.
Step 2: Show that p/2^m is the first common ancestor of nodes
(p-1)/2^m and (p+1)/2^m. Thus sj = (p-1)/2^m is a descendent
of sk = p/2^m and so k < j.
Step 3: The only nodes of T with labels between (p-1)/2^m and
p/2^m must be descendents of sj=(p-1)/2^m and therefore added
at a later stage than sj, that is n > j > k.
The case p=2^m can be treated separately (and is, if anything,
easier). The case where p is odd can be handled symmetrically.
Dan
To reply by email, change LookInSig to luecking