Generalization of Browder's F.P. Theorem?

Generalization of Browder's F.P. Theorem?

[Peter McBurney]

Hello --

Does anyone know of a generalization of Browder's Fixed Point Theorem
from R^n to arbitrary topological spaces, or to categories of same?


*****************

Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
subset of R^n, and let

	f: [0,1] x S --> S

be a continuous function.   Then the set of fixed points

	 { (x,s) | s = f(x,s), x \in [0,1] and s \in S }

contains a connected subset A such that the intersection of A with {0} x
S is non-empty and the intersection of A with {1} x S is non-empty.


*****************

Many thanks,







-- Peter McBurney
University of Liverpool, UK

Re: Generalization of Browder's F.P. Theorem?

[Steven J Vickers]

I'm intrigued by Peter McBurney's question [below]. It looks rather like a
question of the constructive content of Brouwer's fixed point theorem.

Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
topos of sheaves over [0,1], f is just a continuous endomap of S. If
Brouwer's theorem were constructively true then f would have a fixpoint,
and that would come out as a continuous section of the projection [0,1]xS
-> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
[0,1]} would be as required.

However, the proof of Brouwer that I've seen is not constructive - it goes
by contradiction. So maybe the requirements on A are a way of getting
constructive content in Brouwer's result.

What is known constructively about Brouwer's fixed point theorem?

Steve Vickers.

Peter McBurney wrote:

> Hello --
>
> Does anyone know of a generalization of Browder's Fixed Point Theorem
> from R^n to arbitrary topological spaces, or to categories of same?
>
> *****************
>
> Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
> subset of R^n, and let
>
>         f: [0,1] x S --> S
>
> be a continuous function.   Then the set of fixed points
>
>          { (x,s) | s = f(x,s), x \in [0,1] and s \in S }
>
> contains a connected subset A such that the intersection of A with {0} x
> S is non-empty and the intersection of A with {1} x S is non-empty.
>
> *****************
>
> Many thanks,
>
> -- Peter McBurney
> University of Liverpool, UK

Re: Generalization of Browder's F.P. Theorem?

[Prof. Peter Johnstone]

On Thu, 16 Jan 2003, Steven J Vickers wrote:

>
> I'm intrigued by Peter McBurney's question [below]. It looks rather like a
> question of the constructive content of Brouwer's fixed point theorem.
>
> Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
> topos of sheaves over [0,1], f is just a continuous endomap of S. If
> Brouwer's theorem were constructively true then f would have a fixpoint,
> and that would come out as a continuous section of the projection [0,1]xS
> -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
> g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
> [0,1]} would be as required.
>
> However, the proof of Brouwer that I've seen is not constructive - it goes
> by contradiction. So maybe the requirements on A are a way of getting
> constructive content in Brouwer's result.
>
> What is known constructively about Brouwer's fixed point theorem?
>
> Steve Vickers.
>
Similar thoughts had occurred to me. Brouwer's theorem is clearly
not constructive, since it doesn't hold (even locally) continuously in
parameters (consider a path in the space of endomaps of [0,1]
passing through the identity, where the fixed point `flips' from
one end of the interval to the other as it does so). However, Browder's
result would seem to suggest that the `locale of fixed points of f'
(that is, the equalizer of f and the identity in the category of
locales) might be consistent (that is, `inhabited') in general,
even though it may not have any points. It's certainly conceivable
that that might be true constructively, though I can't see how to
prove it -- but it isn't the full content of Browder's theorem.

Peter Johnstone

Re: Generalization of Browder's F.P. Theorem?

[Michael Barr]

In Errett Bishop's Constructive Analysis (anyone who is interested in
analysis over a topos absolutely must know this book), he proves that for
any continuous endomorphism f of a disk and for every eps > 0, there is a
point x in the disk for which |f(x) - x| < eps.  A couple of points should
be made.  First f has to be constructible and eps has to be provably
positive.  For Bishop, a real number is an equivalence class of pairs of
RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n -
a_m/b_m| < 1/m + 1/n and a function is constructive if it is a machine for
turning one such sequence into another.  To be continuous, it there must
be a function delta(eps) that produces for each eps > 0, a delta(eps) such
that |x - y| < delta(eps) implies that |f(x) - f(y)| < eps.  (In fact,
there is a non-constructive proof that every constructive function is
continuous.)

Bishop then claims, without proof as far as I can see, that there is a
fixed point free endomorphism of the disk.  What this means is that when
you extend this function to all reals, any fixed point is not a
constructible real number.

On Thu, 16 Jan 2003, Steven J Vickers wrote:

>
> I'm intrigued by Peter McBurney's question [below]. It looks rather like a
> question of the constructive content of Brouwer's fixed point theorem.
>
> Suppose S is (homeomorphic to) an n-cell. Then in the internal logic of the
> topos of sheaves over [0,1], f is just a continuous endomap of S. If
> Brouwer's theorem were constructively true then f would have a fixpoint,
> and that would come out as a continuous section of the projection [0,1]xS
> -> [0,1]. More precisely, it would be a map g: [0,1] -> S such that f(x,
> g(x)) = g(x) for all x. If this existed then the set A = {(x, g(x))| x in
> [0,1]} would be as required.
>
> However, the proof of Brouwer that I've seen is not constructive - it goes
> by contradiction. So maybe the requirements on A are a way of getting
> constructive content in Brouwer's result.
>
> What is known constructively about Brouwer's fixed point theorem?
>
> Steve Vickers.
>
> Peter McBurney wrote:
>
> > Hello --
> >
> > Does anyone know of a generalization of Browder's Fixed Point Theorem
> > from R^n to arbitrary topological spaces, or to categories of same?
> >
> > *****************
> >
> > Theorem (Browder, 1960):  Suppose that S is a non-empty, compact, convex
> > subset of R^n, and let
> >
> >         f: [0,1] x S --> S
> >
> > be a continuous function.   Then the set of fixed points
> >
> >          { (x,s) | s = f(x,s), x \in [0,1] and s \in S }
> >
> > contains a connected subset A such that the intersection of A with {0} x
> > S is non-empty and the intersection of A with {1} x S is non-empty.
> >
> > *****************
> >
> > Many thanks,
> >
> > -- Peter McBurney
> > University of Liverpool, UK
>
>
>
>

Re: Generalization of Browder's F.P. Theorem?

[Andrej Bauer]

Michael Barr <barr@barrs.org> writes:
> For Bishop, a real number is an equivalence class of pairs of
> RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n -
> a_m/b_m| < 1/m + 1/n ...

Actually, Bishop purposely avoids taking a real to be an equivalence
class of sequences, presumably because he does not want to assume the
axiom of countable choice.

A sequence as described above is sometimes called a "fundamental
sequence". Two such sequences x = (a_n/b_n) and y = (c_n/b_n) are
said to "coincide", written x ~ y iff

                   |a_n/b_n - c_m/d_m| < 2/n + 2/m,

where I might have gotten the right-hand side slightly wrong.

Now there are two possibilities:

(1) we say that a real is an equivalence class of fundamental
sequences under the relation ~, or

(2) we say that a real _is_ a fundamental sequence, where two reals
are claimed "equal" if they coincide (the approach taken by Bishop).

The first alternative gives us what is usually called "Cauchy reals".

The difference between the two is apparent when we attempt to show
that every Cauchy sequence of reals has a limit. In the first case we
are given a sequence of equivalence classes of fundamental sequences.
In order to construct a fundamental sequence representing the limit we
need to _choose_ a representative from each equivalence class.

In the second case a Cauchy sequence of reals is a sequence of
fundamental sequences, so no choice is required.

There seems to be an open question in regard to this, advertised by
Alex Simpson and Martin Escardo: find a topos in which Cauchy reals
are not Cauchy complete (i.e., not every Cauchy sequence of reals has
a limit). For extra credit, make it so that the Cauchy completion of
Cauchy reals is strictly smaller than the Dedekind reals.

Has this been advertised on this list already? Or was it the FOM list?

[If anyone replies to this, I suggest you start a new discussion thread.]

Andrej Bauer

Cauchy completeness of Cauchy reals

[Martin Escardo]

Andrej Bauer writes:
 > find a topos in which Cauchy reals
 > are not Cauchy complete (i.e., not every Cauchy sequence of reals has
 > a limit). For extra credit, make it so that the Cauchy completion of
 > Cauchy reals is strictly smaller than the Dedekind reals.

One small clarification: Regarding the extra credit, there doesn't
seem to be a reasonable "absolute" way of defining the completion in
question. E.g.  the various, constructively different, notions of
metric completion already assume the existence of some given complete
reals. However, one can always embed the Cauchy reals into the
Dedekind reals, which are always Cauchy complete, and then look at the
smallest "subset" containing this which is closed under limits of
Cauchy sequences (where Cauchy sequences are defined as in Andrej's
message). We sometimes call this, somewhat verbosely, "the Cauchy
completion of the Cauchy reals within the Dedekind reals".  But notice
that this is the same as what one gets starting from the rationals
within the Dedekind reals and then closing under limits and hence
could be called the "Cauchy completion of the rationals within the
Dedekind reals".

NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
Simpson and I characterized "the Cauchy completion of the rationals
within the Dedekind reals" as a free algebra (to be precise, we
started from the algebras as a primitive notion and later found this
construction of the free one). But this has already been discussed in
postings in the past few years.

Martin Escardo

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

Martin Escardo wrote:

>NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
>Simpson and I characterized "the Cauchy completion of the rationals
>within the Dedekind reals" as a free algebra
>
and vaughan pratt and i characterized the cauchy reals as a final
coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. in
fact, freyd came up with his characterization of the closed interval
while commenting on our first paper, where vaughan and i worked with the
semiopen interval.

but it is fair to say that the algebraic approach allows easier
algebraic operations on reals. (i only managed to multiply them in one
of our coalgebras, and in a very inefficient way.)

-- dusko

BTW have you seen the book:

    Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and
Fabrication of Life
    by Robert Rosen (Columbia University Press 1991)

it was referenced in a biology paper, i found it in the biology library,
and it's full of categories. (yes, i kno, people often do that to sound
complicated, but this seems like honest work, perhaps even inspiring,
although it does not go very deep.)

Category Theory in Biology

[Peter McBurney]

Dusko --


>
> BTW have you seen the book:
>
>     Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and
> Fabrication of Life
>     by Robert Rosen (Columbia University Press 1991)
>
> it was referenced in a biology paper, i found it in the biology library,
> and it's full of categories. (yes, i kno, people often do that to sound
> complicated, but this seems like honest work, perhaps even inspiring,
> although it does not go very deep.)


An earlier book of Rosen's applying category theory to biology (or
rather, speaking more carefully, exploring how one might conceive of
applying category theory to biological domains) was:

"Anticipatory Systems:  Philosophical, Mathematical and Methodological
Foundations"  (Pergamon Press, Oxford, UK 1985)


You may also be interested in this work by Andree Ehresmann and
Jean-Paul Venbremeersch on a category-theoretic account of evolving
systems, such as those found in biological domains:

	http://perso.wanadoo.fr/vbm-ehr/


  Peter McBurney
  Department of Computer Science
  University of Liverpool

Re: Cauchy completeness of Cauchy reals

[Martin Escardo]

Dusko Pavlovic writes:
 > >NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
 > >Simpson and I characterized "the Cauchy completion of the rationals
 > >within the Dedekind reals" as a free algebra
 > >
 > and vaughan pratt and i characterized the cauchy reals as a final
 > coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280.

I forgot to mention this --- I apologize. In your paper, you work in
Set. Do you think your construction works in any topos? If so, what
would "Cauchy reals" mean precisely in this general context? Thanks.

ME

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

>
>
>Set. Do you think your construction works in any topos?
>
the coalgebraic structures are defined using just arithmetic. in the
first one, there is the "no infinite sequences of 1s" condition, which i
am reminded depends on markov's principle; but that is just used in the
explanation. i don't think there are other constraints.

>If so, what
>would "Cauchy reals" mean precisely in this general context?
>
it means fundamental sequence, with the equivalence relation in the
"lazy" mode, a la bishop, as described in andrej bauer's message.

if my last night's posting makes sense, then these constructivist cauchy
reals make a whole lot of difference, because they really let you avoid
the choice and get limits.

-- dusko

Re: Cauchy completeness of Cauchy reals

[Prof. Peter Johnstone]

On Fri, 24 Jan 2003, Dusko Pavlovic wrote:

> >
> >
> >Set. Do you think your construction works in any topos?
> >
> the coalgebraic structures are defined using just arithmetic. in the
> first one, there is the "no infinite sequences of 1s" condition, which i
> am reminded depends on markov's principle; but that is just used in the
> explanation. i don't think there are other constraints.
>
> >If so, what
> >would "Cauchy reals" mean precisely in this general context?
> >
> it means fundamental sequence, with the equivalence relation in the
> "lazy" mode, a la bishop, as described in andrej bauer's message.
>
I'm sorry, but this won't do. In a topos, equality is equality; you can't
treat it "lazily". So a Cauchy real has to be an equivalence class of
Cauchy sequences, and there is in general no way of choosing a
canonical representative for it. Markov's principle would, I think
(I haven't checked the details), suffice to give a canonical
representation as a binary expansion with no infinite sequence of
1's, and then Dusko's argument would suffice to show that the Cauchy
reals are Cauchy complete. But there are many toposes where Markov's
principle fails.

I doubt very much whether the Cauchy reals occur
as a final coalgebra for anything, in any topos where they fail to
coincide with the Dedekind reals, simply because the Dedekind reals
are likely to be a coalgebra for the same endofunctor (and they're
more "final" than the Cauchy reals). Incidentally, Peter Freyd and
I worked out how to do his coalgebra construction constructively,
and I showed that its final coalgebra is the Dedekind interval in any
topos -- the proof is in the Elephant, at the end of section D4.7.

Peter Johnstone

Re: Cauchy completeness of Cauchy reals

[Alex Simpson]

Peter Johnstone writes:

> I'm sorry, but this won't do. In a topos, equality is equality; you
> can't
> treat it "lazily". So a Cauchy real has to be an equivalence class of
> Cauchy sequences, and there is in general no way of choosing a
> canonical representative for it. Markov's principle would, I think
> (I haven't checked the details), suffice to give a canonical
> representation as a binary expansion with no infinite sequence of
> 1's,

In fact not. Markov's principle holds in the effective topos, and
there, unless I'm much mistaken, it is not even true that the map from
binary representations to Cauchy (= Dedekind) reals in [0,1] is epi,
let alone split epi.

Alex Simpson

Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209

Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt]

Dear toposophers,

With constructivity of real arithmetic back on the front burner for the
moment, let P be the ring of bounded power series a0 + a1.x + a2.x^2 + ...
with integer coefficients a_i, where the bound is, for each such series,
an integer c such that |a_i| < c (3/2)^i / i^(3/2).

Let 1-2x generate the ideal I of P.  Then the quotient ring P/I turns out
to be the field of reals [AMM 105(1998), p.769].

This is more constructive than it might appear, being just an obscure
(or clear depending on your upbringing) way of representing reals in a
redundant binary notation.  The ring P permits fast arithmetic essentially
by deferring carries.  Carries are "propagated" when needed by quotienting
by I, which works by collapsing every formal power series to one all of
whose coefficients other than a0 are either 0 or 1 and which has infinitely
many 0s (equivalently, no infinite run of 1's).

In this view of things, a real is understoood as an integer (a0) plus a
binary fraction in [0,1) (the rest of some "binary" formal power series,
meaning one with a_i = 0 or 1 for i > 0 and infinitely many 0s).  A general
formal power series without this restriction to 0 and 1 then constitutes
a redundant representation of a real, which can be made irredundant when
needed (e.g. when comparing with <) by quotienting by I.

An intuitively clear but less constructive view is to evaluate each series at
x = 1/2, the root of 1-2x, noting that any series bounded as above converges
absolutely there.  Series identified by I are those that evaluate to the
same real at x = 1/2.

What is nonconstructive about this is that direct evaluation of an infinite
series at a point requires infinite time, no matter how large and parallel
the infinite circuit computing it may be.

In contrast, P and P/I are more constructive in the following sense.
Addition and subtraction in P require circuit depth O(1) using an infinite
circuit whose gates perform integer addition and subtraction (just do it
coordinatewise).  Reduction mod I takes longer, but there is a variant of
the above in which it is fast enough.  Instead of the field R we settle
for just the group R, and instead of |a_i| < c (3/2)^i / i^(3/2) we settle
for simply |a_i| < c.  In this case any given series can be reduced (same
generator 1-2x) to the above normal form in circuit depth log_2(c) (nice
exercise), a finite quantity despite the series itself being of infinite
length and fluctuating arbitrarily within ±c.

Multiplication is problematic for two reasons.  First it obliges the weaker
bound, complicating reduction.  Secondly it is a convolution, complicating
arithmetic even when carry propagation is deferred.  I don't see obvious
solutions to either of these problems.  On the other hand I have no a priori
reason to suppose that these circuit-theoretic complications of passing
from R as a group to R as a ring or field would be reflected in suitably
constructive topos-theoretic developments of these notions.

Vaughan Pratt

Re: Cauchy completeness of Cauchy reals

[Vaughan Pratt]

While I'm comfortable with coalgebraic presentations of the continuum, as
well as such algebraic presentations as the field P/I (P being a ring of
certain polynomials, I the ideal of P generated by 1-2x) that I mentioned
a week or so ago, I'm afraid I'm no judge of constructive approaches to
formulating Dedekind cuts.  Would a toposopher (or a constructivist of
any other stripe) view the following variants as all more or less equally
constructive, for example?

1.  Define a (closed) interval in the reals as a disjoint pair (L,R)
consisting of an order ideal L and an order filter R, both in the rationals
standardly ordered, both lacking endpoints.  Order intervals by pairwise
inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'.
Define the reals to be the maximal elements in this order.  Define an
irrational to be a real for which (L,R) partitions Q.

2.  Ditto but with the reals defined instead to be intervals for which
Q - (L U R) is a finite set.  ("Finite set" rather than just "finite" to
avoid the other meaning of "finite interval."  The order plays no role
in this definition, maximality of reals in the order being instead a
theorem.)

3.  As for 2 but with "finite" replaced by "cardinality at most 1".
The predicate "rational" is identified with the cardinality of Q - (L U R).

Vaughan

Re: Cauchy completeness of Cauchy reals

[Prof. Peter Johnstone]

On Mon, 3 Feb 2003, Vaughan Pratt wrote:
>
> While I'm comfortable with coalgebraic presentations of the continuum, as
> well as such algebraic presentations as the field P/I (P being a ring of
> certain polynomials, I the ideal of P generated by 1-2x) that I mentioned
> a week or so ago, I'm afraid I'm no judge of constructive approaches to
> formulating Dedekind cuts.  Would a toposopher (or a constructivist of
> any other stripe) view the following variants as all more or less equally
> constructive, for example?
>
> 1.  Define a (closed) interval in the reals as a disjoint pair (L,R)
> consisting of an order ideal L and an order filter R, both in the rationals
> standardly ordered, both lacking endpoints.  Order intervals by pairwise
> inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'.
> Define the reals to be the maximal elements in this order.  Define an
> irrational to be a real for which (L,R) partitions Q.
>
> 2.  Ditto but with the reals defined instead to be intervals for which
> Q - (L U R) is a finite set.  ("Finite set" rather than just "finite" to
> avoid the other meaning of "finite interval."  The order plays no role
> in this definition, maximality of reals in the order being instead a
> theorem.)
>
> 3.  As for 2 but with "finite" replaced by "cardinality at most 1".
> The predicate "rational" is identified with the cardinality of Q - (L U R).
>
No constructivist (of whatever stripe) would be happy talking about
Q - (L U R), as in your second and third definitions, since he wouldn't
want to assume that L and R were complemented as subsets of Q.
Your first definition, if I understand it correctly, is equivalent to
what most toposophers would call the MacNeille reals -- that is, the
(Dedekind-MacNeille) order-completion of Q. If you "positivize" the
second and third (which would appear to be equivalent, for any sensible
notion of finiteness) by saying "Whenever p and q are rationals with
p < q, then either p \in L or q \in R", you get the Dedekind reals,
which are a proper subset of the MacNeille reals (though they
coincide iff De Morgan's law holds) but have rather better algebraic
properties.

Peter Johnstone

Re: Cauchy completeness of Cauchy reals

[Mamuka Jibladze]

> NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex
> Simpson and I characterized "the Cauchy completion of the rationals
> within the Dedekind reals" as a free algebra (to be precise, we
> started from the algebras as a primitive notion and later found this
> construction of the free one). But this has already been discussed in
> postings in the past few years.
>
> Martin Escardo

Does one get any known versions of reals by performing the Cauchy or
Dedekind construction starting with initial algebras I for non-decidable
lifts L
instead of the NNO? It would be then also natural to interpret Cauchy
sequences and completeness using appropriate I-indexed families, of course.

Even for "integers" Z one has at least three different options:
taking I^op+1+I, taking the colimit of I->LI->LLI->..., each map being
the unit, or taking the colimit of the corresponding I-indexed diagram.
It would be strange if these turn out to be isomorphic. Is any of them an
initial
algebra for some simple functor?

Similarly there are various possibilities for rationals - taking fractions,
i.e. a quotient
of ZxZ, or colimit of all multiplication maps Z->Z, or of the corresponding
Z-indexed
diagram.

Actually I have not followed the ongoing research for a while, so maybe my
questions
are outdated. I would be grateful for any references to related work.

Mamuka Jibladze

Re: Cauchy completeness of Cauchy reals

[Ross Street]

With all this talk about real numbers, perhaps readers would be
interested in my little paper (reporting an idea of Steve Schanuel):

	An efficient construction of the real numbers,
	Gazette Australian Math. Soc. 12 (1985) 57-58.

which may be hard to find. However, a recent report of an
undergraduate vacation project can be obtained at

	http://www.maths.mq.edu.au/~street/efficient.pdf

This project convinced me that this construction is a good one for
teaching undergraduates.

Others have had this idea too.  In particular, the following was
recently posted on the math arXiv:

	Norbert A'Campo, A natural construction of the real numbers,
		arXiv:math.GN/0301015 v1  3 Jan 2003.

With regards,
	Ross

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

Andrej Bauer wrote:

>There seems to be an open question in regard to this, advertised by
>Alex Simpson and Martin Escardo: find a topos in which Cauchy reals
>are not Cauchy complete (i.e., not every Cauchy sequence of reals has
>a limit). For extra credit, make it so that the Cauchy completion of
>Cauchy reals is strictly smaller than the Dedekind reals.
>
this will give me negative credits one way or another, but here it goes:

let a = (a_i) be a cauchy sequence of rationals between 0 and 1. (cauchy
means |a_m - a_n| < 1/m + 1/n, as in andrej's message.)

let b = (b_i) be the subsequence b_i = a_{2^i+3}. b and a are equivalent
in the sense from the message, because

     |a_m - b_n| < 1/m + 1/(2^n+3) < 2/m + 2/n

note that

     |b_i - b_{i+k}| < 1/(2^i+3) + 1/(2^(i+k)+3) < 1/(2^i+2)

now define x_i to be the simplest dyadic that falls in the interval
between b_i - 1/2^(i+2) and b_i + 1/2^(i+2). in other words, to get x_i,
begin adding 1/2 + 1/4 + 1/8... until you overshoot b_i - 1/2^(1+2). if
you also overshoot b_i + 1/2^(1+2), and the last summand was 1/2^k, skip
it, and try adding 1/2^(k+1), etc. one of them must fall in between. a
less childish way to say this is that x_i is the shortest irredundant
binary (no infinite sequences of 1) such that

     |b_i - x_i| < 1/2^(i+2)

so x =  (x_i) is a cauchy sequence equivalent to b, with

     |x_i - x_{i+k}| <= |x_i-b_i| + | b_i - b_{i+k}| + |b_{i+k} - x_{i+k}| <
                     <  1/2^(i+2) + 1/2^(i+2)        + 1/2^(i+k+2) <
                     <  1/2^i

this means that the first i digits of x_i and x_{i+k} coincide.

now let X be the binary number such that its first i digits are the same
as in x_i, for every i. (if it ends on an infinte sequence of 1s,
replace it by the corresponding irredundant representative.) this is
clearly a constant cauchy sequence equivalent to x, so it is its limit.
since x is equivalent to b

    |b_m - x_n| <= |b_m - b_n| + |b_n - x_n| < 1/2^(m+3) + 1/2^(n+3) +
1/2^(n+2) < 2/m + 2/n

and b is equivalent to a, X is also the limit of a.

is there an error in the above reasoning? i can't find it. on the other
hand, i printed out the paper by alex and martin, and the conjecture is
stated rather strongly, so i guess i must be missing something.

-- dusko

Re: Cauchy completeness of Cauchy reals

[Dusko Pavlovic]

heh, i typed this late, and managed to confuse the basic assumption.
instead of

> let a = (a_i) be a cauchy sequence of rationals between 0 and 1.

let a = (a_i) be a cauchy sequence of *cauchy reals*, i.e. each a_i is a
cauchy sequence of rationals between 0 and 1.

i think the rest goes unchanged: you take a fast converging subsequence
b of a, and then approximate b by irredundant rational prefixes. the
irredundant representation is thus used instead of choice. the
completeness of such representation is the finality of its coalgebraic
structure.

-- dusko