Cardinality types and the one-word extensional cardinal carrier. More...

#include <algorithm>
#include <array>
#include <climits>
#include <cmath>
#include <compare>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <ranges>
#include <stdexcept>
#include <type_traits>
#include <utility>
#include <variant>
import dedekind.category;

Include dependency graph for cardinality.cppm:

Classes
struct	dedekind::sets::Finite
struct	dedekind::sets::is_extensional< T >
	Primary trait: Is a species defined by its members? More...
struct	dedekind::sets::is_extensional< T >
struct	dedekind::sets::ℵ< N >
struct	dedekind::sets::ExtensionalCardinal< W >
	Finite extensional cardinal: one machine word `W`. More...
struct	dedekind::sets::ExtensionalCardinal< W >::CheckedResult
	A wrapped result and whether the exact result overflowed `W`. More...
struct	dedekind::sets::CardinalityEffect
	Draft writer-like cardinality effect carrier. More...
struct	dedekind::sets::SignedExtensionalCardinal< S >
	Signed one-word integer: two's complement in the signed word `S`. More...
struct	dedekind::sets::SignedExtensionalCardinal< S >::CheckedResult
	A wrapped result and whether the exact result overflowed. More...
struct	dedekind::sets::PositiveInfinity
struct	dedekind::sets::NegativeInfinity
struct	dedekind::sets::NaZ
struct	dedekind::category::is_integer_chain< dedekind::sets::Cardinality >
struct	dedekind::category::is_integer_chain< dedekind::sets::SignedCardinality >
struct	dedekind::category::is_integer_chain< dedekind::sets::ExtensionalCardinal< W > >
struct	dedekind::category::is_integer_chain< dedekind::sets::SignedExtensionalCardinal< S > >
struct	dedekind::category::unit_trait< C1, std::plus< C1 > >
struct	dedekind::category::unit_trait< C1, std::multiplies< C1 > >
struct	dedekind::category::is_periodic< C1, std::plus< C1 > >
struct	dedekind::category::is_periodic< C1, std::multiplies< C1 > >
struct	dedekind::category::unit_trait< Z1, std::plus< Z1 > >
struct	dedekind::category::unit_trait< Z1, std::multiplies< Z1 > >
struct	dedekind::category::is_periodic< Z1, std::plus< Z1 > >
struct	dedekind::category::is_periodic< Z1, std::multiplies< Z1 > >
struct	dedekind::category::inverse_trait< Z1, std::plus< Z1 > >
struct	dedekind::category::is_cyclic_group< dedekind::sets::ExtensionalCardinal< W >, std::plus< dedekind::sets::ExtensionalCardinal< W > > >
struct	dedekind::category::is_cyclic_group< dedekind::sets::SignedExtensionalCardinal< S >, std::plus< dedekind::sets::SignedExtensionalCardinal< S > > >
struct	dedekind::category::unit_trait< SC, std::plus< SC > >
struct	dedekind::category::unit_trait< SC, std::multiplies< SC > >
struct	dedekind::category::is_saturating< SC, std::plus< SC > >
struct	dedekind::category::is_saturating< SC, std::multiplies< SC > >
struct	dedekind::category::is_saturating< SC, std::minus< SC > >
struct	dedekind::category::inverse_trait< SC, std::plus< SC > >
struct	dedekind::category::unit_trait< Card, std::plus< Card > >
struct	dedekind::category::unit_trait< Card, std::multiplies< Card > >
struct	dedekind::category::is_saturating< Card, std::plus< Card > >
struct	dedekind::category::is_saturating< Card, std::multiplies< Card > >
struct	dedekind::category::SpeciesTraits< dedekind::sets::Cardinality >
struct	dedekind::category::SpeciesTraits< dedekind::sets::SignedCardinality >
struct	dedekind::category::SpeciesTraits< dedekind::sets::SignedExtensionalCardinal< S > >

Namespaces
namespace	dedekind::sets
namespace	dedekind::category

Concepts
concept	dedekind::sets::IsCardinality
concept	dedekind::sets::IsCountable
concept	dedekind::sets::IsFinite
concept	dedekind::sets::IsExtensional
concept	dedekind::sets::IsWrappingWord
	A machine word that is the wrapping ring ℤ/2^w: an unsigned built-in integer (not `bool`) that the `category` registrations certify as a commutative ring under `+` and `*`, periodic under `+`, and totally ordered.
concept	dedekind::sets::IsRingIntegral
	The old name of `IsIntegerChain`, which never claimed a ring.

Typedefs
using	dedekind::sets::ℵ_0 = ℵ<0>
	Countable Infinity.
using	dedekind::sets::ℶ_1 = ℵ<1>
	The Continuum (assuming GCH).
using	dedekind::sets::Cardinality = std::variant<ExtensionalCardinal<>, ℵ_0>
	Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.
using	dedekind::sets::SignedCardinality
	Signed counterpart of `Cardinality` with ±ℵ_0 escalation; the library's bona-fide proxy for \(\mathbb{Z}\) modulo physical limits.
using	dedekind::category::C1 = dedekind::sets::ExtensionalCardinal<>
using	dedekind::category::Z1 = dedekind::sets::SignedExtensionalCardinal<>
using	dedekind::category::SC = dedekind::sets::SignedCardinality
using	dedekind::category::Card = dedekind::sets::Cardinality

Functions
template<IsWrappingWord W>
constexpr std::variant< ExtensionalCardinal< W >, ℵ_0 >	dedekind::sets::add_or_ℵ_0 (const ExtensionalCardinal< W > &lhs, const ExtensionalCardinal< W > &rhs)
template<IsWrappingWord W>
constexpr std::variant< ExtensionalCardinal< W >, ℵ_0 >	dedekind::sets::mul_or_ℵ_0 (const ExtensionalCardinal< W > &lhs, const ExtensionalCardinal< W > &rhs)
constexpr Cardinality	dedekind::sets::finite_cardinality (std::size_t n)
	Convenience constructor for finite cardinal values.
constexpr Cardinality	dedekind::sets::add (const Cardinality &lhs, const Cardinality &rhs)
	Cardinal addition under the finite/ℵ_0 policy.
constexpr Cardinality	dedekind::sets::mul (const Cardinality &lhs, const Cardinality &rhs)
	Cardinal multiplication under the finite/ℵ_0 policy.
constexpr std::strong_ordering	dedekind::sets::compare (const Cardinality &lhs, const Cardinality &rhs)
	Total comparison over the finite/ℵ_0 fragment.
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Explicit `==` on `Cardinality`. `std::variant` supplies a defaulted `operator==` inside the module's purview, but it is not reachable across the `dedekind.sets` module boundary (the <variant> header lives in the global module fragment, so its operator templates are not exported). Defining the operator explicitly in `dedekind::sets` — where ADL can find it from importers like `dedekind.numbers` — closes that gap so `IsPartiallyOrdered<Cardinality>` / `std::three_way_comparable<Cardinality>` fire downstream.
constexpr Cardinality	dedekind::sets::operator+ (const Cardinality &lhs, const Cardinality &rhs) noexcept
	`+` on `Cardinality` wraps the existing `add()` policy (saturating to `ℵ_0` on overflow).
constexpr Cardinality	dedekind::sets::successor (const Cardinality &n) noexcept
	The NNO steps on the ℕ proxy, as the free customization points the order layer's point collapse calls (`category:nno`, found here by ADL): successor is `+` `finite_cardinality(1)`, saturating at `ℵ_0` (its fixpoint); predecessor is the monus — 0 is its fixpoint (ℕ has no negatives), and `ℵ_0` is fixed again. The :nno arrow `Successor<Cardinality>` delegates here, so the law is spelled once.
constexpr Cardinality	dedekind::sets::predecessor (const Cardinality &n) noexcept
constexpr Cardinality	dedekind::sets::operator++ (Cardinality n) noexcept
	`++n` / `--n:` the successor and the predecessor of the ℕ proxy, by value, saturating at ℵ₀ and stepping down by monus (#1002).
constexpr Cardinality	dedekind::sets::operator-- (Cardinality n) noexcept
constexpr Cardinality	dedekind::sets::operator* (const Cardinality &lhs, const Cardinality &rhs) noexcept
	`*` on `Cardinality` wraps the existing `mul()` policy.
constexpr Cardinality	dedekind::sets::operator/ (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean division on `Cardinality`. Convention follows the `ExtensionalCardinal<>` totalisation: division by zero yields zero; `finite` `/` `ℵ_0` yields zero (the limit); `ℵ_0` `/` `finite-non-zero` yields `ℵ_0`; `ℵ_0` `/` `ℵ_0` yields `ℵ_0` (saturation rather than indeterminate — `Cardinality` has no `NaZ-equivalent` sentinel; the ℕ proxy keeps the policy total).
constexpr Cardinality	dedekind::sets::operator% (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean remainder on `Cardinality`. Mirrors the `operator/` convention: `finite` `%` `finite` delegates to the underlying `ExtensionalCardinal<>'s` `%`; `finite` `%` `ℵ_0` returns the `lhs` (the limit-style "remainder is the original" reading); operations with `ℵ_0` on the `lhs` saturate to `ℵ_0`.
constexpr std::strong_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Spaceship on `Cardinality` wraps `compare()` (finite values compare via the underlying `ExtensionalCardinal<>` spaceship; `ℵ_0` dominates every finite value). Returns `std::strong_ordering` — there is no NaN-equivalent in the ℕ proxy.
constexpr std::size_t	dedekind::sets::realize_to_size_t (const Cardinality &value, std::size_t transfinite_sentinel=std::numeric_limits< std::size_t >::max())
	Realize a cardinality value to std::size_t with explicit boundary.
constexpr CardinalityEffect	dedekind::sets::unit_effect (Cardinality value)
	Unit for cardinality effect composition.
template<typename F> requires std::invocable<F&, const Cardinality&> && std::convertible_to<std::invoke_result_t<F&, const Cardinality&>, CardinalityEffect>
constexpr CardinalityEffect	dedekind::sets::bind_effect (const CardinalityEffect &effect, F f)
	Sequential composition of cardinality effects.
constexpr ExtensionalCardinal	dedekind::sets::inverse (ExtensionalCardinal<> value, std::plus< ExtensionalCardinal<> >)
	Additive inverse of ExtensionalCardinal<> (two's-complement).
template<typename T> requires requires(T x) { { -x } -> std::convertible_to<T>; }
constexpr T	dedekind::sets::inverse (const T &x, std::plus< T >)
	Generic additive inverse for a carrier supporting unary negation: the `+-inverse` is `-x`, inferred from the negation structure rather than registered per carrier.
constexpr bool	dedekind::sets::detail::sc_is_finite (const SignedCardinality &v) noexcept
constexpr bool	dedekind::sets::detail::sc_is_pos_inf (const SignedCardinality &v) noexcept
constexpr bool	dedekind::sets::detail::sc_is_neg_inf (const SignedCardinality &v) noexcept
constexpr bool	dedekind::sets::detail::sc_is_naz (const SignedCardinality &v) noexcept
constexpr bool	dedekind::sets::detail::sc_is_zero (const SignedCardinality &v) noexcept
constexpr int	dedekind::sets::detail::sc_sign (const SignedCardinality &v) noexcept
constexpr bool	dedekind::sets::is_finite (const SignedCardinality &v) noexcept
	Is this signed cardinal a FINITE ℤ value (not `±ℵ_0` / `NaZ`)? The public query behind Honest-Rejection guards at the carrier boundary — e.g. `Rational::simplify` skips `euclidean_gcd` (which would not terminate on a `NaZ`, since `NaZ` `%` `·` `==` `NaZ`) when a numerator/denominator is a non-finite sentinel (#680).
template<std::integral S>
constexpr SignedCardinality	dedekind::sets::finite_signed_cardinality (S value) noexcept
	Convenience constructor for finite signed values.
template<std::integral K>
constexpr Cardinality	dedekind::sets::carrier_cast (std::type_identity< Cardinality >, K k)
	An integer constant meeting ℕ or ℤ, the hook the term grammar's `carrier_cast` reaches by ADL: exactly, or a domain error for a negative constant meeting ℕ.
template<std::integral K>
constexpr SignedCardinality	dedekind::sets::carrier_cast (std::type_identity< SignedCardinality >, K k)
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &v) noexcept
	Unary negation: swaps signs and ±ℵ_0; preserves NaZ.
constexpr SignedCardinality	dedekind::sets::operator+ (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Addition with ±ℵ_0 escalation on overflow.
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Subtraction, computed directly so that only an overflowing difference saturates (`a` + (−b) would saturate `−min` first, so `min` − min would not be 0). Infinities as for `a` + (−b).
constexpr SignedCardinality	dedekind::sets::successor (const SignedCardinality &n) noexcept
	The step up on the ℤ proxy, the free customization point the order layer's point collapse calls (`category:nno`, found here by ADL), as on `Cardinality:` `+1` through the saturating `+`, so `+ℵ_0` is a fixpoint and `NaZ` propagates.
constexpr SignedCardinality	dedekind::sets::predecessor (const SignedCardinality &n) noexcept
	The step down on the ℤ proxy: `−1` through the saturating `-`, so `−ℵ_0` is a fixpoint and `NaZ` propagates. Unlike ℕ there is no monus: ℤ steps down past zero.
constexpr SignedCardinality	dedekind::sets::operator* (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Multiplication with ±ℵ_0 escalation on overflow. `0` * ±ℵ_0 is indeterminate (returns `NaZ`).
constexpr SignedCardinality	dedekind::sets::operator/ (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Truncating division. Division by zero and `±ℵ_0/±ℵ_0` return `NaZ`; `finite/±ℵ_0` returns `0` (the limit); `±ℵ_0` divided by a non-zero finite value saturates to signed infinity according to the operand signs.
constexpr SignedCardinality	dedekind::sets::operator% (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Truncating remainder. Mirrors C++ semantics on the finite alternative; non-finite operands give `NaZ`.
constexpr std::partial_ordering	dedekind::sets::compare_signed (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Partial ordering on the extended integers: −ℵ_0 < finite < +ℵ_0; `NaZ` is unordered with respect to everything (including itself), mirroring IEEE-NaN's unordered semantics. Returning `std::partial_ordering` rather than `std::strong_ordering` is the principled choice: `NaZ` compares `unordered`, which keeps ordering and equality (variant's defaulted `==`, which finds `NaZ` == `NaZ` true) consistent without forcing a fake `equal` answer.
constexpr bool	dedekind::sets::operator< (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	`<` derived from `compare_signed`; required by `IsInteger`. For `NaZ` operands the comparison is `unordered` so this returns `false`, mirroring IEEE-NaN's `<` behaviour.
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Explicit homogeneous `==` on `SignedCardinality` (#669).
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Explicit homogeneous `<=>` on `SignedCardinality` (#669).
constexpr std::weak_ordering	dedekind::sets::constant_order (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	The structural order of signed cardinalities as constants of a term (#884, `canonical's` sort key): total, unlike `<=>`. By alternative first (finite, +∞, −∞, then `NaZ`), a finite value by its order.
template<std::integral T>
constexpr std::strong_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, T rhs) noexcept
	`Cardinality` `<=>` `std::integral`. ℵ_0 is greater than any finite integer; negative signed values are below the entire ℕ proxy (no element of `Cardinality` is negative), which is encoded as `lhs` `>` `rhs`. Otherwise the comparison reduces to the `ExtensionalCardinal<>` spaceship. Delegates the integral lift through `ExtensionalCardinal<>'s` existing `std::integral` ctor, which subsumes `bool` / `size_t` / signed-non-negative paths uniformly — avoiding `std::make_unsigned_t` (undefined for `bool`).
template<std::integral T>
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, T rhs) noexcept
	`Cardinality` `==` `std::integral`. Negative signed values and ℵ_0 never equal a finite integer; the finite alternative delegates to `ExtensionalCardinal<>'s` defaulted `==`.
template<std::integral T>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, T rhs) noexcept
	`SignedCardinality` `<=>` `std::integral`. Lifts `rhs` to a finite `SignedCardinality` and routes through `compare_signed`; `NaZ` on `lhs` propagates as `std::partial_ordering::unordered`, mirroring IEEE-NaN's unordered semantics.
template<std::integral T>
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, T rhs) noexcept
	`SignedCardinality` `==` `std::integral`. `NaZ` and `±ℵ_0` never equal a finite integer; the finite alternative delegates to `SignedExtensionalCardinal<>'s` canonical-zero-aware equality.
template<std::floating_point F>
constexpr bool	dedekind::sets::detail::is_negative (F x) noexcept
	Whether `x` lies strictly below zero (`-0.0` does not); and whether it is zero of either sign. The operators on `F` live here, ahead of the overloads below, which read `F` through these and the standard classification functions only.
template<std::floating_point F>
constexpr bool	dedekind::sets::detail::is_zero (F x) noexcept
template<std::floating_point F, std::unsigned_integral LT>
constexpr std::partial_ordering	dedekind::sets::detail::compare_unsigned_to_floating (LT lhs, F rhs) noexcept
	Compare a non-negative integer `lhs` with a finite floating-point value `rhs` in integer domain — the comparison is precision-correct even when `lhs` exceeds `2^digits` <F> (where the cast `LT` `→` `F` is no longer exact and consecutive integers collapse to the same float).
template<std::floating_point F, std::unsigned_integral LT>
constexpr bool	dedekind::sets::detail::eq_unsigned_to_floating (LT lhs, F rhs) noexcept
	Equality counterpart of `compare_unsigned_to_floating:` requires `rhs` to be finite, non-negative, integer-valued, in [0, 2^digits<LT>) range, and equal to `lhs` in `LT` domain. Anything else is `false`.
template<std::floating_point F>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, F rhs) noexcept
	`Cardinality` `<=>` `std::floating_point`. `ℵ_0` is greater than every finite double (and equivalent to `+inf`); negative finite floats and `-inf` land strictly below the ℕ proxy. A `NaN` `rhs` returns `std::partial_ordering::unordered`. Finite-vs-finite is settled in integer domain via `compare_unsigned_to_floating`, which stays precision-correct even when the underlying word exceeds `2^digits` <F>.
template<std::floating_point F>
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, F rhs) noexcept
	`Cardinality` `==` `std::floating_point`. Equality requires either `ℵ_0` vs `+inf`, or finite `lhs` equal to a finite, non-negative, integer-valued `rhs` in the carrier's representable range. Float rounding cannot fake equality (`eq_unsigned_to_floating` compares in integer domain).
template<std::floating_point F>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, F rhs) noexcept
	`SignedCardinality` `<=>` `std::floating_point`. `NaZ` propagates as `unordered` (mirrors compare_signed's NaZ semantics); `±ℵ_0` maps to `±inf-equivalent`; `NaN` `rhs` returns `unordered`. Finite-vs-finite is settled by sign-aware delegation to the unsigned integer- domain helper, so the comparison stays precision-correct even when the underlying magnitude exceeds `2^digits` <F>.
template<std::floating_point F>
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, F rhs) noexcept
	`SignedCardinality` `==` `std::floating_point`. `NaZ` / `NaN` never equal anything; `±ℵ_0` equals only `±inf`; finite delegates to the integer-domain `eq_unsigned_to_floating` on the magnitude with sign reconciled, so float rounding cannot fake equality on large-magnitude integers.
constexpr SignedCardinality	dedekind::sets::lift_cardinality_to_signed (const Cardinality &c) noexcept
	Lift `Cardinality` into `SignedCardinality` via the canonical ℕ ↪ ℤ embedding direction. Public, exported: this is the canonical variant-level `ℕ` `↪` `ℤ` embedding that the carrier-lattice diagram (Figure 1 in `paper.tex`) labels at the top row. The machine-layer counterpart is `embed_uint_sint_` in `numbers:integer` (an `arrow<unsigned`, `int>` sign reinterpretation, structurally distinct from the variant- layer canonical embedding here). Lives in `sets:cardinality` so the cross-variant operators below reach it without crossing the `sets` `→` `numbers` module boundary; an exported `arrow` form `lift_ℕ_ℤ_` wrapping this function lives in `numbers:integer` for monic-arrow registration in the carrier lattice.
constexpr std::partial_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, const SignedCardinality &rhs) noexcept
	`Cardinality` `<=>` `SignedCardinality`. Routes through the canonical ℕ ↪ ℤ lift and `compare_signed`; `NaZ` on the `rhs` propagates as `unordered`.
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, const SignedCardinality &rhs) noexcept
	`Cardinality` `==` `SignedCardinality`. `NaZ` never equals anything; otherwise the canonical lift settles the comparison.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &v) noexcept
	Closure-forcing unary minus on `Cardinality:` well-defined on every natural, with codomain widened to `SignedCardinality`. Delegates to the canonical lift `lift_cardinality_to_signed` and `SignedCardinality's` existing unary `-`, so canonicalisation rules (canonical `+0` for negation-of-zero; `+ℵ_0` → `-ℵ_0` sentinel flip) flow from a single source of truth. This is the smallest possible elementwise statement of the Grothendieck construction in code.
constexpr Cardinality	dedekind::sets::abs (const SignedCardinality &z) noexcept
	Retraction direction: `abs` : `ℤ` `→` `ℕ`. The math- honest signature for absolute value: every element of `SignedCardinality` has a non-negative magnitude, so the result type is `Cardinality` (not `SignedCardinality`), announcing the non-negativity guarantee at the type level.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &a, const Cardinality &b) noexcept
	Closure-forcing binary minus on `Cardinality:` well-defined as a function `ℕ` × ℕ → ℤ; ℕ isn't closed under it. The operator's existence with the wider return type is the Grothendieck embedding made operational at the binary level. Routes through `lift_cardinality_to_signed` on both operands and dispatches to `SignedCardinality's` `-`.
constexpr SignedCardinality	dedekind::sets::operator+ (const Cardinality &a, const SignedCardinality &b) noexcept
	Closed cross-carrier addition: `Cardinality` `+` `SignedCardinality` lifts the `Cardinality` through the canonical embedding and dispatches to `SignedCardinality's` `+`. Closes in `ℤ`. Carrier-promotion in the math-correct direction (larger carrier wins).
constexpr SignedCardinality	dedekind::sets::operator+ (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: `SignedCardinality` `+` `Cardinality`. Delegates to the canonical direction; addition is commutative on ℤ.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &a, const SignedCardinality &b) noexcept
	Closure-forcing cross-carrier subtraction: `Cardinality` `-` `SignedCardinality`. Result is in `ℤ` — well-defined on the (ℕ, ℤ) pair as a function into ℤ.
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: `SignedCardinality` `-` `Cardinality`. Lifts `b` through the embedding; result is in `ℤ`. Subtraction is not commutative, so this is a separate overload, not a delegation.
constexpr SignedCardinality	dedekind::sets::operator* (const Cardinality &a, const SignedCardinality &b) noexcept
	Closed cross-carrier multiplication: `Cardinality` `*` `SignedCardinality` lifts and dispatches. Closes in `ℤ`.
constexpr SignedCardinality	dedekind::sets::operator* (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: `SignedCardinality` `*` `Cardinality`. Multiplication is commutative; delegates to the canonical direction.
template<IsWrappingWord W>
constexpr ExtensionalCardinal< W >	dedekind::sets::successor (const ExtensionalCardinal< W > &n) noexcept
	The NNO's step on the extensional cardinals, the wrapping ring \(\mathbb{Z}/2^w\): `n` + 1 and `n` - 1 modulo the word, as on the word itself.
template<IsWrappingWord W>
constexpr ExtensionalCardinal< W >	dedekind::sets::predecessor (const ExtensionalCardinal< W > &n) noexcept
template<std::integral S>
constexpr SignedExtensionalCardinal< S >	dedekind::sets::successor (const SignedExtensionalCardinal< S > &n) noexcept
template<std::integral S>
constexpr SignedExtensionalCardinal< S >	dedekind::sets::predecessor (const SignedExtensionalCardinal< S > &n) noexcept
template<>
constexpr SignedCardinality	dedekind::category::lift< Cardinality, SignedCardinality > (Cardinality const &n)

Variables
constexpr Cardinality	dedekind::sets::detail_cardinality_step_witness::two = finite_cardinality(2)
template<std::floating_point F, std::unsigned_integral LT>
constexpr F	dedekind::sets::detail::two_to_the_digits_v
	\(2^{d}\) with `d` the digits of `LT`, as an exact `F:` the doublings are exact in `F` since \(2^k\) is representable until `k` overflows `F's` exponent range (well above any plausible `LT::digits`; for `LT` `=` `uint64_t` and `F` `=` `double` this is \(2^{64}\)). A fold of the doublings (Rule 3); `std::ldexp` would be cleaner but is not `constexpr` until C++26.
constexpr auto	dedekind::sets::lift_ℕ_ℤ_
	Canonical variant-layer embedding `ℕ` `↪` `ℤ:` `Cardinality` `→` `SignedCardinality`, exposed as a first-class `arrow` object for the carrier-lattice diagram.
constexpr auto	dedekind::sets::embed_𝕂3_ℤ_
	Canonical embedding K3 ↪ ℤ: Ternary → SignedCardinality.
constexpr auto	dedekind::sets::abs_
	Arrow form of `abs:` an exported `arrow<SignedCardinality`, Cardinality> object. Registered epic (surjective) below: every `Cardinality` is the image of itself ( `abs`(lift_ℕ_ℤ_(c)) `=` `c`) and of its negation; the map is sign-folding, conflating `+n` and `-n`. Companion to the injective `lift_ℕ_ℤ_` in `numbers:integer` — together they exhibit the split-mono pair from the carrier-lattice diagram (Figure 1).
template<>
constexpr bool	dedekind::category::is_associative_v< C1, std::plus< C1 > > = true
template<>
constexpr bool	dedekind::category::is_associative_v< C1, std::multiplies< C1 > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< C1, std::plus< C1 > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< C1, std::multiplies< C1 > > = true
template<>
constexpr bool	dedekind::category::is_distributive_v< C1, std::multiplies< C1 >, std::plus< C1 > > = true
template<typename W>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::sets::ExtensionalCardinal< W >, std::less_equal<> >
template<typename W>
constexpr bool	dedekind::category::is_transitive_v< dedekind::sets::ExtensionalCardinal< W >, std::less_equal<> >
template<typename W>
constexpr bool	dedekind::category::is_antisymmetric_v< dedekind::sets::ExtensionalCardinal< W >, std::less_equal<> > = true
template<typename W>
constexpr bool	dedekind::category::is_connex_v< dedekind::sets::ExtensionalCardinal< W >, std::less_equal<> >
template<>
constexpr bool	dedekind::category::is_associative_v< Z1, std::plus< Z1 > > = true
template<>
constexpr bool	dedekind::category::is_associative_v< Z1, std::multiplies< Z1 > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< Z1, std::plus< Z1 > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< Z1, std::multiplies< Z1 > > = true
template<>
constexpr bool	dedekind::category::is_distributive_v< Z1, std::multiplies< Z1 >, std::plus< Z1 > > = true
template<>
constexpr bool	dedekind::category::is_invertible_v< Z1, std::plus< Z1 > > = true
template<typename S>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::sets::SignedExtensionalCardinal< S >, std::less_equal<> > = true
template<typename S>
constexpr bool	dedekind::category::is_transitive_v< dedekind::sets::SignedExtensionalCardinal< S >, std::less_equal<> > = true
template<typename S>
constexpr bool	dedekind::category::is_antisymmetric_v< dedekind::sets::SignedExtensionalCardinal< S >, std::less_equal<> > = true
template<typename S>
constexpr bool	dedekind::category::is_connex_v< dedekind::sets::SignedExtensionalCardinal< S >, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_associative_v< SC, std::plus< SC > > = true
template<>
constexpr bool	dedekind::category::is_associative_v< SC, std::multiplies< SC > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< SC, std::plus< SC > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< SC, std::multiplies< SC > > = true
template<>
constexpr bool	dedekind::category::is_distributive_v< SC, std::multiplies< SC >, std::plus< SC > > = true
template<>
constexpr bool	dedekind::category::is_invertible_v< SC, std::plus< SC > > = true
template<>
constexpr bool	dedekind::category::is_reflexive_v< SC, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_transitive_v< SC, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_antisymmetric_v< SC, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_connex_v< SC, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_associative_v< Card, std::plus< Card > > = true
template<>
constexpr bool	dedekind::category::is_associative_v< Card, std::multiplies< Card > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< Card, std::plus< Card > > = true
template<>
constexpr bool	dedekind::category::is_commutative_v< Card, std::multiplies< Card > > = true
template<>
constexpr bool	dedekind::category::is_distributive_v< Card, std::multiplies< Card >, std::plus< Card > > = true
template<>
constexpr bool	dedekind::category::is_reflexive_v< Card, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_transitive_v< Card, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_antisymmetric_v< Card, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_connex_v< Card, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_closure_forcing_v< std::negate<>, dedekind::sets::Cardinality, dedekind::sets::SignedCardinality > = true
template<>
constexpr bool	dedekind::category::is_closure_forcing_v< std::minus<>, dedekind::sets::Cardinality, dedekind::sets::SignedCardinality > = true
template<>
constexpr bool	dedekind::category::is_epic_arrow_v< std::decay_t< decltype(dedekind::sets::abs_)> > = true
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< std::decay_t< decltype(lift_ℕ_ℤ_)> >
template<>
constexpr bool	dedekind::category::is_monotone_v< std::decay_t< decltype(lift_ℕ_ℤ_)>, std::less_equal<> > = true
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< std::decay_t< decltype(embed_𝕂3_ℤ_)> >
template<>
constexpr bool	dedekind::category::is_monotone_v< std::decay_t< decltype(embed_𝕂3_ℤ_)>, std::less_equal<> >

Detailed Description

Cardinality types and the one-word extensional cardinal carrier.

@partition :cardinality

This partition owns all concrete cardinality types:

Finite, ℵ<N>, ℵ_0, ℶ_1 — the cardinality ladder (moved from :mereology, where only the structural concepts now remain).
ExtensionalCardinal<W> — the machine-total finite cardinal carrier with wrapping arithmetic, compatible with dedekind.category:total.
Cardinality — the finite | ℵ_0 sum type and its utility functions.

Cardinality is a property of sets — how many elements a set contains — so it belongs in the sets layer, below numbers and algebra. The numbers:cardinality partition re-exports this and adds the IsNatural and IsTotallyOrdered proofs that require the numbers and order layers.

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

Note: "Das Wesen der Mathematik liegt in ihrer Freiheit." ("The essence of mathematics lies entirely in its freedom.") – Georg Cantor, Grundlagen einer allgemeinen Mannigfaltigkeitslehre (1883)

Function Documentation

◆ compare_unsigned_to_floating()

template<std::floating_point F, std::unsigned_integral LT>

std::partial_ordering dedekind::sets::detail::compare_unsigned_to_floating	(	LT	lhs,
		F	rhs )

constexprnoexcept

Compare a non-negative integer lhs with a finite floating-point value rhs in integer domain — the comparison is precision-correct even when lhs exceeds 2^digits <F> (where the cast LT → F is no longer exact and consecutive integers collapse to the same float).

Pre: rhs is finite, not NaN. Sign of rhs is handled.

Strategy:

rhs negative → lhs (≥ 0) is strictly greater.
rhs out of [0, 2^digits<LT>) range → lhs ≤ LT_max < rhs, so lhs is strictly less.
rhs in range → split rhs into integer part trunc(rhs) and a fractional indicator; compare lhs to the integer part in LT domain (exact); if rhs has no fractional part, equivalent at integer-equality, else lhs sits below rhs at integer-equality (since rhs > floor in that case).

◆ is_negative()

template<std::floating_point F>

bool dedekind::sets::detail::is_negative ( F x )

constexprnoexcept

Whether x lies strictly below zero (-0.0 does not); and whether it is zero of either sign. The operators on F live here, ahead of the overloads below, which read F through these and the standard classification functions only.

Template Parameters

F	the floating type.

Variable Documentation

◆ two_to_the_digits_v

template<std::floating_point F, std::unsigned_integral LT>

F dedekind::sets::detail::two_to_the_digits_v

inlineconstexpr

Initial value:

= std::ranges::fold_left(
    std::views::repeat(F{2}, std::numeric_limits<LT>::digits), F{1},
    std::multiplies<F>{})

\(2^{d}\) with d the digits of LT, as an exact F: the doublings are exact in F since \(2^k\) is representable until k overflows F's exponent range (well above any plausible LT::digits; for LT = uint64_t and F = double this is \(2^{64}\)). A fold of the doublings (Rule 3); std::ldexp would be cleaner but is not constexpr until C++26.

Template Parameters

F	the floating type.
LT	the unsigned word.

Classes

Namespaces

Concepts

Typedefs