A sequence whose image is order-bounded. Bishop §2. More...

Concept definition

template<typename Seq>

concept dedekind::sequences::IsBoundedSequence = IsSequence<Seq> && is_bounded_sequence_v<Seq>

dedekind::sequences::IsBoundedSequence

A sequence whose image is order-bounded. Bishop §2.

Definition convergence.cppm:326

dedekind::sequences::IsSequence

The fundamental mapping from a Domain Set to a Value Type.

Definition net.cppm:215

dedekind::sequences::is_bounded_sequence_v

constexpr bool is_bounded_sequence_v

Opt-in: Seq is order-bounded (image bounded above and below). The bound witnesses are the engineer's ...

Definition convergence.cppm:312

Detailed Description

A sequence whose image is order-bounded. Bishop §2.

Mandelbrot connection

Orbit-boundedness is the Mandelbrot membership criterion: c ∈ M ⟺ the orbit mandelbrot_orbit(c) = iterate(0, z↦z²+c) (in :numbers::mandelbrot) is bounded ⟺ IsBoundedSequence holds for that orbit. The escape-time machinery (orbit_escape_time) is the negation: an escaping parameter's orbit is unbounded, so IsBoundedSequence honestly rejects it.