Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::sequences::WitnessesBolzanoWeierstrass Concept Referenceexport
module dedekind.sequences

The Bolzano–Weierstrass crown: Sub witnesses that the bounded sequence Sup has a convergent subsequence. More...

Concept definition

template<typename Sub, typename Sup>
concept dedekind::sequences::WitnessesBolzanoWeierstrass =
IsBoundedSequence<Sup> && IsSubsequence<Sub, Sup> &&
IsClassicallyConvergent<Sub>
dedekind::sequences::IsBoundedSequence
A sequence whose image is order-bounded. Bishop §2.
Definition convergence.cppm:326
dedekind::sequences::IsClassicallyConvergent
A Cauchy sequence whose carrier sits in the classical logic regime, so the Cauchy ⇒ convergent collap...
Definition convergence.cppm:160
dedekind::sequences::IsSubsequence
Sub is a subsequence of Sup (same Codomain, strictly increasing index map). Feeds the Bolzano-Weierst...
Definition convergence.cppm:414
dedekind::sequences::WitnessesBolzanoWeierstrass
The Bolzano–Weierstrass crown: Sub witnesses that the bounded sequence Sup has a convergent subsequen...
Definition convergence.cppm:442

Detailed Description

The Bolzano–Weierstrass crown: Sub witnesses that the bounded sequence Sup has a convergent subsequence.

Holds when Sup is order-bounded (IsBoundedSequence), Sub is a subsequence of Sup (IsSubsequence), and Sub is IsClassicallyConvergent. This is Bolzano–Weierstrass read as a logical-collapse theorem: "every bounded sequence has a convergent subsequence" is classically true but constructively false (it needs sequential compactness / a LEM-grade choice). The classical collapse fires exactly when the carrier is in the Boole regime (countable cardinality cut); over a Kleene carrier the witness is honestly rejected — no type-level guarantee of a convergent subsequence (Specker / non-computable limit).

The convergent subsequence itself (the strictly-increasing index map and the limit) is the existential witness the engineer supplies via is_subsequence_v + the carrier's classical regime; this concept certifies that a supplied (Sub, Sup) pair has the Bolzano–Weierstrass shape. Crown of #719 (Form-chain row 7).