cut.cppm File Reference

The genuine real: a decidable Dedekind cut on \(\mathbb{Q}\). More...

#include <compare>
#include <concepts>
#include <functional>
#include <stdexcept>
#include <type_traits>
import dedekind.numbers:rational;
import dedekind.order;
import dedekind.sets;
import dedekind.category;

Include dependency graph for cut.cppm:

Classes
class	dedekind::numbers::Cut< Q >
	A decidable Dedekind real: a principal rational cut or a rational radical \(\pm\sqrt{c}\). More...
struct	dedekind::numbers::LowerCut< Q >
	The datum of a real's lower set: the real itself, χ(q) = real.contains(q). More...
struct	dedekind::category::SpeciesTraits< dedekind::numbers::Cut< Q > >
	Atlas registration: Cut<Q> is a first-class species. More...
struct	dedekind::numbers::Interval< V, L >
	A convex subset of a chain as a VALUE — an interval: each side an optional Bound, with a runtime-evaluable membership χ. Closed under ∩; a union or a complement leaves it unless one operand covers the other. No side is the universe; both sides closed at one value is a point; no Span at all is the one empty set, to which crossing bounds normalise. The bounds ride as values, never as NTTPs. Consume it through &, |, ==, <=, membership and the half / point / empty / universe / bounded factories. More...
struct	dedekind::numbers::Comprehension< Base, Predicate >
struct	dedekind::numbers::𝔸< T, L, C >
	The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...

Namespaces
namespace	dedekind::numbers
namespace	dedekind::category

Typedefs
template<IsRational Q = Rational<default_integer>>
using	dedekind::numbers::LowerSet = Comprehension<𝔸<Q, Boole>, LowerCut<Q>>
	The lower set of a real, \(\{q\in\mathbb{Q}\mid q<r\}\), as a set over \(\mathbb{Q}\).
template<IsRational Q = Rational<default_integer>>
using	dedekind::numbers::PrincipalRay = Interval<Q>
	The ray \(\{q<p\}\) over \(\mathbb{Q}\): the lower set of a principal cut, \(\mathbb{Q}\hookrightarrow\mathbb{R}\) as the order datum.

Enumerations
enum class	dedekind::numbers::Strictness
	Whether the boundary is strict (>, <) or inclusive (>=, <=).

Functions
template<IsRational Q>
constexpr LowerSet< Q >	dedekind::numbers::lower_set (const Cut< Q > &r)
	\(r \mapsto \{q<r\}\): the real read as its lower set.
template<IsRational Q>
constexpr PrincipalRay< Q >	dedekind::numbers::principal_ray (const Q &p)
	\(p \mapsto \{q<p\}\): the rational embedded as the principal ray, extensionally lower_set(Cut<Q>{p}).

Variables
template<typename Q>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::numbers::Cut< Q >, std::less_equal<> > = true
template<typename Q>
constexpr bool	dedekind::category::is_transitive_v< dedekind::numbers::Cut< Q >, std::less_equal<> > = true
template<typename Q>
constexpr bool	dedekind::category::is_antisymmetric_v< dedekind::numbers::Cut< Q >, std::less_equal<> > = true
template<typename Q>
constexpr bool	dedekind::category::is_connex_v< dedekind::numbers::Cut< Q >, std::less_equal<> > = true
constexpr Projection< 0 >	dedekind::numbers::π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

The genuine real: a decidable Dedekind cut on \(\mathbb{Q}\).

@partition :cut

Copyright

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

cut__Reals_As_Cuts

A real number is a Dedekind lower cut of \(\mathbb{Q}\) (Dedekind 1872). Rational names only the principal cuts — one rational bound, so it can name \(\mathbb{Q}\) but no irrational. Cut<Q> is the leaf that adds the first non-principal cuts we can still decide:

• principal \(q\): the cut \(\{x\in\mathbb{Q}\mid x<q\}\);
• radical \(\pm\sqrt{c}\) ( \(c\in\mathbb{Q},\,c\ge 0\)): the cut \(\{x\mid x<0 \lor x^2<c\}\) (and its reflection). Membership of a rational point, and the order between two such cuts, are both decidable by exact \(\mathbb{Q}\) arithmetic (compare \(q^2\) to \(c\)) — so Cut<Q> is a genuine IsTotallyOrdered carrier, not a postulate. Arithmetic ( \(+,\times\)) is not yet closed at this leaf: the sum of two cuts is a Minkowski sum whose membership is \(\exists\)-over- \(\mathbb{Q}\) (Ternary), and lands with the Expr layer that grows Cut into the full field. The order fabric decidable here is exactly what a real interval (e.g. \((-\sqrt2,\sqrt2)\)) needs.

cut__The_Cut_Is_Its_Lower_Set

The real is its lower set: lower_set(r) is the comprehension of the cut over 𝔸<Q>, an IsLSet whose χ is contains. A rational \(p\) embeds as the principal cut, whose lower set is the order datum's ray \(\{q<p\}\) (principal_ray); a radical cut's lower set \(\{q<0\lor q^2<c\}\) is not a ray over \(\mathbb{Q}\), which is what makes it a new real.

Note

"Ich sehe es, aber ich glaube es nicht." — Richard Dedekind (letter to Cantor, 1877). [Trans: "I see it, but I don't believe it."]