completeness.cppm File Reference

Density and completeness profiles of orders. More...

#include <concepts>
#include <functional>
import dedekind.order:total;
import dedekind.sets;
import dedekind.category;

Include dependency graph for completeness.cppm:

Namespaces
namespace	dedekind::category
namespace	dedekind::sets

Concepts
concept	dedekind::order::IsSuccessor
	The algebraic S: T -> T mapping via the Unit element.
concept	dedekind::order::IsArchimedean
	The scale axiom: Every element can be 'reached' by the Successor. FIXME: misnamed. "Every element reached by the successor" is Peano's and Dedekind's generation of the naturals from one element and a step; the Archimedean property is another axiom, that for x, y > 0 some n has n x > y [1]. Rename to the property it states, and reconcile its algebraic IsSuccessor (x + 1) with the NNO step of dedekind.category (successor, HasNNOStep), which every shipped carrier provides and IsSuccessor's carriers withhold.
concept	dedekind::order::IsDiscrete
	A set where every point is isolated by a step: the carrier provides the NNO steps (successor / predecessor, HasNNOStep), as the machine integers and the ℕ / ℤ proxies do. The step is the honest discreteness signal; the IsSuccessor leg of IsArchimedean is withheld on every shipped carrier and cannot carry the guard.
concept	dedekind::order::IsDense
	A property where a midpoint always exists (a < c < b).
concept	dedekind::order::IsDividableChain
	A Totally Ordered species with a partitioning algorithm (/).
concept	dedekind::order::IsDedekindComplete
	The topological "Soul" of the Continuum (LUB property).

Functions
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, EuclideanDivision, bool divisor_is_constant)
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, std::modulus<>, bool divisor_is_constant)

Variables
template<HasNNOStep N>
constexpr bool	dedekind::category::is_monotone_v< Successor< N >, std::less_equal<> > = true
	The step arrows preserve the order of a registered chain, \(x \le y \Rightarrow S(x) \le S(y)\) and likewise for P: the irreducible leaf facts the variance inference starts from. Saturation at a bound is monotone; wrapping is not, and wrapping is the carrier's registered periodicity (is_periodic_v of its +: the unsigned words, ℤ/N), so the fact is read off the algebra, not off the type's name; the chain gate supplies the order.
template<HasNNOStep N>
constexpr bool	dedekind::category::is_monotone_v< Predecessor< N >, std::less_equal<> > = true

Detailed Description

Density and completeness profiles of orders.

@partition :completeness

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

completeness__Scope

These concepts classify \emph{how} an ordered carrier fills the gaps between its elements. Together they distinguish the classical ℤ / ℚ / ℝ tower:

• successor-isolated points ← ℤ (private helper IsDiscrete)
• IsDense ← ℚ (a midpoint always exists)
• IsDedekindComplete ← ℝ (every non-empty bounded set has sup)

The public concepts exported from this partition are IsSuccessor, IsArchimedean, IsDense, IsDividableChain, and IsDedekindComplete. IsDiscrete is a private helper used inside IsDense; see the declaration for the rationale.

Wikipedia: Archimedean property, Dense order, Dedekind completeness.

Note

"Eine geordnete Menge heißt vollständig, wenn jede nicht leere und nach oben beschränkte Teilmenge eine kleinste obere Schranke besitzt." [Trans: "An ordered set is called complete if every non-empty subset bounded above has a least upper bound."] — Felix Hausdorff, Grundzüge der Mengenlehre (Leipzig: Veit & Co., 1914), §6. Hausdorff's foundational text on set-theoretic order and topology codifies the supremum-completeness reading the project's IsDedekindComplete and IsDense concepts pin.