natural.cppm File Reference

The Dictionary of Species (The Registry). More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <optional>
#include <stdexcept>
#include <utility>
import dedekind.numbers:scalars;
import dedekind.sets;
import dedekind.sequences;
import dedekind.relational;
import dedekind.order;
import dedekind.morphologies;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for natural.cppm:

Classes
struct	dedekind::sets::ResidueClass< L >
	The class \(\{x \in \mathbb{N} \mid x \equiv r \pmod n\}\), read analytically: the materialisation of ℕ | (π % n == r). More...

Namespaces
namespace	dedekind::numbers
namespace	dedekind::numbers::detail_lambek_witness
namespace	dedekind::category
namespace	dedekind::sets

Concepts
concept	dedekind::numbers::IsNatural
	Structural concept for a commutative semiring with total order (the intensional ℕ).

Functions
template<typename S> requires requires(S&& s) { dedekind::sets::image(embed_𝔹_ℕ_, std::forward<S>(s)); }
constexpr auto	dedekind::numbers::embed_𝔹_ℕ (S &&s)
	Set-level lift of embed_𝔹_ℕ_: image of a Boolean set S under the canonical mono 𝔹 ↪ ℕ.
template<IsNatural N, std::unsigned_integral U>
constexpr N	dedekind::numbers::embed_unsigned_integral (U v)
	Canonical injection from std::unsigned_integral into any IsNatural domain N via its single-argument constructor.
template<typename L, typename C, std::integral K1, std::integral K2>
constexpr ResidueClass< L >	dedekind::sets::operator& (const 𝔸< Cardinality, L, C > &, const Cmp< Rel::Eq, BinOp< std::modulus<>, Projection< 0 >, Const< K1 > >, Const< K2 > > &c)
	ℕ & (π % n == r): the residue class, decided analytically. A residue outside \([0, n)\) is never met, so π % 3 == 3 is empty. ADL finds it through the 𝔸<Cardinality> operand.
constexpr auto	dedekind::numbers::dagger (const auto &r)
template<typename F> requires dedekind::category::IsArrow<F> && std::equality_comparable<typename std::remove_cvref_t<F>::Codomain>
constexpr Graph< std::remove_cvref_t< F > >	dedekind::numbers::graph (F f)
	graph(f) — the graph of a function f : A → B as the Set of pairs \(\{\,(a,b) \mid b = f(a)\,\} \subseteq A\times B\).

Variables
constexpr auto	dedekind::numbers::embed_𝔹_ℕ_
	Canonical embedding 𝔹 ↪ ℕ: bool → Cardinality.
constexpr Cardinality	dedekind::numbers::detail_lambek_witness::largest_finite
constexpr Cardinality	dedekind::numbers::aleph_0 = Cardinality{ℵ_0{}}
	The countably-infinite cardinal \(\aleph_0\) as a Cardinality value: the saturation point, and the unique fixpoint of Successor<Cardinality> (succ(ℵ₀) = ℵ₀). A readable spelling of Cardinality{ℵ_0{}}, sibling to finite_cardinality(n).
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< std::decay_t< decltype(dedekind::numbers::embed_𝔹_ℕ_)> >
template<>
constexpr bool	dedekind::category::is_embedding_functor_v< std::decay_t< decltype(dedekind::numbers::embed_𝔹_ℕ_)> > = true
template<>
constexpr bool	dedekind::category::is_monotone_v< std::decay_t< decltype(dedekind::numbers::embed_𝔹_ℕ_)>, std::less_equal<> >
constexpr auto	dedekind::numbers::ℕ
constexpr Projection< 0 >	dedekind::numbers::π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

The Dictionary of Species (The Registry).

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

@partition :numbers @build_order 7 @dependency :algebra, :topology, :cardinalities

natural__Numbers

This partition is the final "Registry" of the ontology. It maps concrete C++ types to their formal algebraic and topological identities.

We "Bless" the coordinate species by verifying their rungs on the ladder:

• IsNatural : N (ℕ) - The Discrete Monoid.
• IsInteger : Z (ℤ) - The Euclidean Group.
• Rational : Q (ℚ) - The Countable Dense Field.
• QuadraticReal<D> / 𝕃<F> : R (ℝ) - Exact and finite-float realisations.

natural__Structural_Mapping

This is where we perform the final 'Lifting'. We prove that SignedExtensionalCardinal<> satisfies the strict IsArithmeticAdditiveGroup / IsCommutativeRing witnesses pinned in integer.cppm and that double is a hardware-constrained approximation of an exact field.

@anchors C++ Fundamental Types: bool, char, int, long, float, double.

Wikipedia: Number, Natural number, Integer, Rational number, Real number

Copyright

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

Note

"Ubi ex mirabili magisterio in arte per novem figuras Indorum introductus, scientia artis in tantum mihi pre ceteris placuit, et intellexi ad illam, quod, quicquid studebatur ex ea apud Egyptum, Syriam, Greciam, Siciliam et Provinciam cum suis variis modis, ad que loca negotiationis tam postea peragravi per multum studium et disputationis didici conflictum." [Trans: "There, having been introduced to that art by a marvelous method of teaching by means of the nine figures of the Indians, the knowledge of the art so pleased me above all others, and I came to understand it, that whatever was studied of it in Egypt, Syria, Greece, Sicily, and Provence, and their various methods, to which places of business I afterwards travelled — through much study and the contest of disputation, I learned."] — Leonardo Pisano (Fibonacci), Liber Abaci, Prologus (1202; Boncompagni edition, Rome 1857).