dedekind::numbers Namespace Reference

Namespaces
namespace	detail_lambek_witness

Classes
struct	ReachPath
	The reach indicator's type: a Path<Ternary> monotone in {Unknown, True} (True absorbs), constructible only through collatz_reach_path, which guarantees that shape; registered absorptive in sequences below, as :mandelbrot's DivergencePath is. More...
class	Complex
struct	PartialAddComplex
	Partial addition transform for Complex<R>. More...
struct	PartialMulComplex
	Partial multiplication transform for Complex<R>. More...
struct	UnitRoot
	A SYMBOLIC N-th root of unity \(\zeta_N^{\,p}\), carried by its exponent p ∈ ℤ/N (Modular<N>). The unit harmonics \(\mu_N=\{z:z^N=1\}\): the torsion subgroup of the unit circle U(1), cut out of ℂ, cyclic of order N and \(\cong\mathbb{Z}/N\) via de Moivre. More...
struct	Character
	The de Moivre CHARACTER \(\chi_m : \mathbb{Z}/N \to \mu_N\), \(k \mapsto \zeta_N^{\,mk}\) — the plane wave "as such", carried SYMBOLICALLY in UnitRoot<N> (consumes the μ_N layer; resolve() collapses to exact ℂ at N=8). More...
struct	DiscreteCos
	The exact discrete COSINE \(\cos_N(k) = \cos(2\pi k/N) = \Re\,\zeta_N^k\) over the Modular<N> angle — the EVEN part of the de Moivre character (= the \(\tfrac12(I+U)\) projection's real value). More...
struct	DiscreteSin
	The exact discrete SINE \(\sin_N(k) = \sin(2\pi k/N) = \Im\,\zeta_N^k\) — the ODD part of the character (Im of character<N>(1) resolved). An IsArrow Modular<N> → ℝ, exact at N=8. More...
class	Cut
	A decidable Dedekind real: a principal rational cut or a rational radical \(\pm\sqrt{c}\). More...
struct	LowerCut
	The datum of a real's lower set: the real itself, χ(q) = real.contains(q). More...
struct	LatticeFactory
	Primary template for lattice factory values. More...
struct	LatticeFactory< ℝ_d, 1 >
	Lattice factory specialization for ℝ. More...
struct	LatticeFactory< ℝ_d, N >
	Lattice factory specialization for ℝ^N, N > 1. More...
class	DivergencePath
	The escape signal of a Mandelbrot orbit, tagged as a sequence-shape witness: a monotone {Unknown,True}-valued Path<Ternary> that is structurally absorptive for every parameter c. More...
class	QuadraticReal
	A real of \(\mathbb{Q}(\sqrt D)\): \(a+b\sqrt D\). More...
class	Quaternion
	Hamilton's hypercomplex numbers q = a + bi + cj + dk. More...
class	Rational
	The Field of Fractions over an Integral Domain Z. More...
struct	PartialAddRational
	Partial addition transform for Rational. More...
struct	PartialMulRational
	Partial multiplication transform for Rational. More...
struct	HonestDivRational
	Division transform for Rational. More...
struct	PartialEmbedIntegerToRational
	Identity and Associativity traits for Rational arithmetic. More...
class	EmbedRationalToReal
	The field embedding \(\mathbb{Q}\hookrightarrow\mathbb{R} =\mathbb{Q}(\sqrt2)\), \(q\mapsto q+0\sqrt2\). More...
struct	Interval
	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	Comprehension
struct	𝔸
	The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...

Concepts
concept	IsIEEEPropagationOp
concept	IsComplexScalar
concept	IsEscapeCriterion
	Escape predicate: ComplexType → bool.
concept	IsNatural
	Structural concept for a commutative semiring with total order (the intensional ℕ).
concept	IsQuaternionScalar
	Scalar type suitable as quaternion components.
concept	RejectsNonFinite
	The rejection contract a saturating backing must offer ℚ's tripwire: is_finite(i), found by ADL, says whether i is a point of ℤ or a sentinel (±ℵ_0 / NaZ). Rational rejects a non-finite value wherever one can arise (construction, comparison); a saturating carrier without this hook would clamp silently and is not admitted as a backing (see FractionBacking).
concept	IsRational
	Q is the rational field Rational<Z> — the canonical exact, dense, strongly-ordered coefficient carrier. Used to gate the real carriers (Cut, QuadraticReal): over \(\mathbb{Q}\) a nonsquare integer D has \(\sqrt D\notin\mathbb{Q}\) (a theorem), so those carriers are genuine (canonical representation, sound conjugate/norm) — which fails for a coefficient field that already contains \(\sqrt D\) (e.g. the degenerate QuadraticReal<2, QuadraticReal<2>>).
concept	IsIntegralScalar
	Numbers-layer alias for the algebra scalar bridge concept.
concept	IsUnsignedIntegralScalar
	Numbers-layer alias for the algebra scalar bridge concept.
concept	IsFloatingScalar
	Numbers-layer alias for the algebra scalar bridge concept.
concept	IsScalar
concept	IsNumbers
	The Root Category for all Numerical Structures.

Typedefs
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::Approx = dedekind::ieee::Approx<F>
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::ReportErrorPolicy = dedekind::ieee::ReportErrorPolicy<F>
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::IgnoreErrorPolicy = dedekind::ieee::IgnoreErrorPolicy<F>
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::AdaptiveErrorPolicy = dedekind::ieee::AdaptiveErrorPolicy<F>
using	dedekind::numbers::C1 = dedekind::sets::ExtensionalCardinal<>
using	dedekind::numbers::Z1 = dedekind::sets::SignedExtensionalCardinal<>
using	dedekind::numbers::SC = dedekind::sets::SignedCardinality
using	dedekind::numbers::Card = dedekind::sets::Cardinality
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.
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::IEEE = dedekind::ieee::IEEE<F>
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::IEEEAdd = dedekind::ieee::IEEEAdd<F>
template<std::floating_point F = machine_real_scalar>
using	dedekind::numbers::IEEEMul = dedekind::ieee::IEEEMul<F>
using	dedekind::numbers::default_integer = dedekind::sets::SignedCardinality
	Default signed-integer carrier used by downstream numeric layers (Rational, embeddings). Post-#670-sibling (ℚ retarget): anchored on sets::SignedCardinality (saturating ℤ proxy with ±ℵ_0 / NaZ escalation), mirroring how ℤ = 𝔸<SignedCardinality> in :integer. This is the discipline-consistent canonical ℤ carrier — ℚ = 𝔸<Rational<default_integer>> now uses the saturating variant uniformly.
template<IsComplexScalar R>
using	dedekind::numbers::OrbitPath = Path<Complex<R>>
using	ℍ_ℚ = Quaternion<Rational<>>
using	dedekind::numbers::machine_integer = int
template<IsInteger I = default_integer>
using	dedekind::numbers::RationalPolynomial = dedekind::algebra::Polynomial<Rational<I>>
	The polynomial ring over the rationals in one variable, ℚ[x]: algebra::Polynomial over the quotient field of the integer carrier I.
using	dedekind::numbers::machine_real_scalar = double

Enumerations
enum class	dedekind::numbers::KleenePolicy { Inclusive , Exclusive }
enum class	NumericRegion
	Region tags for simple runtime numeric diagnostics.
enum class	Strictness
	Whether the boundary is strict (>, <) or inclusive (>=, <=).

Functions
template<std::floating_point F = machine_real_scalar>
constexpr NumericRegion	dedekind::numbers::classify_region (F x, F near_zero_scale=F{64}, F huge_scale=F{0.5}) noexcept
template<std::floating_point F = machine_real_scalar>
constexpr F	dedekind::numbers::roundoff_proxy (F x) noexcept
constexpr std::size_t	dedekind::numbers::collatz_rule (std::size_t n)
	The recurrence, spelled out explicitly as a named function (not a lambda): n even ↦ n/2, n odd ↦ 3n+1. Computed on the native size_t shadow, which saturates where 3n+1 would leave the word, the posture of ℕ's proxy (the point-free relation on Cardinality saturates to ℵ₀ the same way). The word's top is odd, so it is a fixpoint of the rule: an orbit that reaches it never reaches 1, and the verdict below stays Unknown rather than wrapping into a false True.
constexpr auto	dedekind::numbers::collatz_orbit (std::size_t n)
	The orbit \(\{n\} ; T^{\le N}\) presented as the arrow's iterate — a lazy Path<std::size_t>.
constexpr ReachPath	dedekind::numbers::collatz_reach_path (std::size_t n)
	True once 1 is present, Unknown before — a monotone {Unknown,True} absorptive path (the ℕ analogue of Mandelbrot's escape indicator).
constexpr std::optional< std::size_t >	dedekind::numbers::collatz_reach_time (std::size_t n, std::size_t budget)
	The first index \(k \le\) budget at which the orbit hits 1, else nullopt — the efficient materialization (one forward pass).
constexpr Ternary	dedekind::numbers::reaches_1_within (std::size_t n, std::size_t budget)
	The Rosolini-dominance verdict: reaches 1 within budget ⟹ True (IN); not yet ⟹ Unknown (U). Never False.
template<std::size_t W, std::size_t B>
constexpr bool	dedekind::numbers::all_reach_1_within ()
	The collapse: the open \(\forall\)-conjecture, restricted to a finite window \([1, W)\) and a budget B, is a decidable compile-time fact.
template<IsComplexScalar R>
constexpr Complex< R >	dedekind::numbers::conj (const Complex< R > &z)
	Complex conjugate: conj(a + bi) = a − bi.
template<IsComplexScalar R>
constexpr R	dedekind::numbers::dot (const Complex< R > &z, const Complex< R > &w)
	The real inner product on ℂ ≅ ℝ²: dot(z, w) = Re(z · conj w) = re_z·re_w + im_z·im_w.
template<IsComplexScalar R>
constexpr R	dedekind::numbers::abs2 (const Complex< R > &z)
	Squared norm abs2(z) = <z, z> = |z|² = re² + im²: exact, √-free.
template<IsComplexScalar R>
constexpr R	dedekind::numbers::euclidean_norm_squared (const Complex< R > &z)
	Squared Euclidean norm on Complex<R>: a synonym for abs2, kept so it stays reachable by ADL in dedekind::numbers for callers that do not import dedekind.geometry (e.g. the Mandelbrot escape test and the set-algebra predicates). Kept squared to avoid a square root in hot paths.
template<unsigned N>
constexpr UnitRoot< N >	dedekind::numbers::unit_root ()
	The primitive N-th root \(\zeta_N=\zeta_N^{1}\) (the μ_N generator).
template<unsigned N>
constexpr Character< N >	dedekind::numbers::character (dedekind::morphologies::Modular< N > m)
	The character \(\chi_m\) at frequency m.
template<unsigned N> requires (N == 8u)
constexpr DiscreteCos< N >	dedekind::numbers::cos_n ()
	\(\cos_N = \Re\,\zeta_N^{(\cdot)}\) as an arrow.
template<unsigned N> requires (N == 8u)
constexpr DiscreteSin< N >	dedekind::numbers::sin_n ()
	\(\sin_N = \Im\,\zeta_N^{(\cdot)}\) as an arrow.
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}).
template<std::floating_point F = machine_real_scalar>
constexpr IEEE< F >	dedekind::numbers::ieee_unit (F value) noexcept
template<std::floating_point F = machine_real_scalar>
constexpr IEEE< F >	dedekind::numbers::assume_ieee (const dedekind::morphologies::𝕃< F > &r) noexcept
	Explicit entry from the honest lane (the finite floats 𝕃<F>) into the IEEE fast lane.
template<std::floating_point F = machine_real_scalar>
constexpr std::optional< dedekind::morphologies::𝕃< F > >	dedekind::numbers::discharge_ieee (const IEEE< F > &x) noexcept
	Explicit exit from the IEEE fast lane into the honest lane: nullopt when the fast lane produced NaN or +/-inf.
template<IsComplexScalar R>
constexpr auto	dedekind::numbers::euclidean_escape_radius_squared (R escape_radius_squared=R{4})
template<IsComplexScalar R>
constexpr auto	dedekind::numbers::mandelbrot_step (const Complex< R > &c)
template<IsComplexScalar R>
constexpr auto	dedekind::numbers::mandelbrot_orbit (const Complex< R > &c)
template<IsComplexScalar R, typename EscapeCriterion> requires IsEscapeCriterion<EscapeCriterion, Complex<R>>
constexpr auto	dedekind::numbers::orbit_divergence_path (const OrbitPath< R > &orbit, EscapeCriterion criterion) -> DivergencePath< R >
template<IsComplexScalar R, typename EscapeCriterion> requires IsEscapeCriterion<EscapeCriterion, Complex<R>>
constexpr std::optional< std::size_t >	dedekind::numbers::orbit_escape_time (const OrbitPath< R > &orbit, std::size_t max_iter, const EscapeCriterion &criterion)
template<IsComplexScalar R>
constexpr std::optional< std::size_t >	dedekind::numbers::orbit_escape_time (const OrbitPath< R > &orbit, std::size_t max_iter, R escape_radius_squared=R{4})
constexpr bool	collapse_ternary (Ternary t, KleenePolicy policy) noexcept
template<IsComplexScalar R, typename EscapeCriterion> requires IsEscapeCriterion<EscapeCriterion, Complex<R>>
constexpr auto	dedekind::numbers::M_kleene_N (std::size_t max_iter, EscapeCriterion criterion)
template<IsComplexScalar R, typename EscapeCriterion> requires IsEscapeCriterion<EscapeCriterion, Complex<R>>
constexpr auto	dedekind::numbers::M_N (std::size_t max_iter, EscapeCriterion criterion, KleenePolicy policy=KleenePolicy::Inclusive)
template<IsComplexScalar R, typename EscapeCriterion> requires IsEscapeCriterion<EscapeCriterion, Complex<R>>
constexpr auto	dedekind::numbers::M_tower (EscapeCriterion criterion, KleenePolicy policy=KleenePolicy::Inclusive)
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 Q>
constexpr auto	dedekind::numbers::Sqrt2_Symbolic ()
template<typename R> requires std::regular<R>
constexpr auto	dedekind::numbers::TranscendentalSet ()
	The Transcendental Set (𝕋).
template<std::floating_point F, typename Op> requires IsIEEEPropagationOp<Op, F>
constexpr Approx< F >	propagate (const Approx< F > &a, const Approx< F > &b, const Op &op={}) noexcept
	Propagate approximation error through a binary IEEE operation.
template<std::floating_point F = double>
constexpr Approx< F >	demo_propagate_add (const Approx< F > &a, const Approx< F > &b) noexcept
	Demo: propagate error through IEEE addition.
template<std::floating_point F = double>
constexpr Approx< F >	demo_propagate_mul (const Approx< F > &a, const Approx< F > &b) noexcept
	Demo: propagate error through IEEE multiplication.
template<std::floating_point F = double>
constexpr IEEE< F >	demo_add_ignore (const IEEE< F > &a, const IEEE< F > &b) noexcept
template<std::floating_point F = double>
constexpr Approx< F >	demo_add_report (const IEEE< F > &a, const IEEE< F > &b) noexcept
	Demo operation: IEEE add under report policy.
template<std::floating_point F = double>
constexpr TernaryResult< Approx< F > >	demo_add_adaptive (const IEEE< F > &a, const IEEE< F > &b) noexcept
	Demo operation: IEEE add under adaptive policy.
template<std::floating_point F, typename Func>
constexpr IEEE< F >	ieee_bind (const IEEE< F > &x, Func &&f)
	Monadic bind in the IEEE effect context.
template<std::floating_point F, typename Func>
constexpr IEEE< F >	ieee_map (const IEEE< F > &x, Func &&f)
	Functor map in the IEEE effect context.
constexpr auto	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 > >	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	n_even = ℕ * ℕ & π_1 % 2 == 0
	The parity discriminant \(\{(n,m) : n \text{ even}\}\) — the axis restriction spelled once, so \(T\) never repeats the \(\pi_1 \bmod 2\) test. Its complement \(\sim\)n_even is \(\{n \text{ odd}\}\) (on ℕ the two parities exhaust and are disjoint), which makes the case split structural rather than two independent guards.
constexpr auto	halve = ℕ * ℕ & π_2 * 2 == π_1
	The even step \(m = n/2\), spelled without division as \(2\pi_2 = \pi_1\) (the doubling graph read backwards).
constexpr auto	triple_plus_1 = ℕ * ℕ & π_1 * 3 + 1 == π_2
	The odd step \(m = 3n+1\) — the affine graph (:order).
constexpr auto	dedekind::numbers::collatz
	The Trsk relation \(T \subseteq \mathbb{N}\times\mathbb{N}\), spelled point-free as the McCarthy conditional \(T = (\text{even} \cap \text{halve}) \cup (\text{odd} \cap \text{triple})\) — no lambda, no graph, the recurrence is the relation, spelled in uniform set-grammar: & (meet), ~ (complement), | (join, the structural OrPredicate union of #365). Mirrors the divides relation of §4; the parity test appears exactly once.
constexpr auto	dedekind::numbers::converges_in_1
	converges_in_1 \(= \mathrm{collatz}^{\circ}(1) = \{n \mid \mathrm{collatz}(n) = 1\}\) — the pre-image of the fixed-point target \(\{1\}\): the naturals that reach 1 in exactly one step. Point-free, via the converse fibre.
constexpr auto	collatzM = collatz & (π_1 < 64)
	collatz restricted to the finite ℕ-prefix \([0,64)\) by a half-space domain cut — the bound 64 rides in the pivot VALUE, so >> recovers it.
constexpr auto	dedekind::numbers::collatz2 = collatzM >> collatzM
	collatz2 \(= \mathrm{collatz};\mathrm{collatz}\) over the finite \([0,64)\) middle — two steps, the bare relative product, middle inferred from the bound (no argument, no shadow, no graph, no array).
constexpr auto	back2 = converse(collatz2)
	converged_2 \(= \mathrm{collatz2}^{\circ}(\{1,2,4\})\) — the naturals captured by the attractor within two steps: the pre-image of the cycle, spelled as the finite relational image (fibre of the converse over the three cycle points), which distributes to the union of the point-fibres.
constexpr auto	dedekind::numbers::converged_2
constexpr auto	dedekind::numbers::pending_2 = ~converged_2
	pending_2 \(= \sim\)converged_2 — the naturals not yet captured within two steps: the honest "Unknown", complemented on the domain (unary), not on the pair universe.
constexpr auto	dedekind::numbers::embed_ℝ_ℂ
	The Birkhoff S leg \(\mathbb{R}\hookrightarrow\mathbb{C}\) over the coat-hanger: QuadraticReal<2> → Complex<QuadraticReal<2>>, \(r\mapsto (r,0)\).
constexpr auto	dedekind::numbers::root8
	The exact de Moivre exponential \(\zeta_8 : \mathbb{Z}/8 \to \mathbb{C}^\times\) over the coat-hanger ℝ = ℚ(√2): \(k \mapsto \zeta_8^{\,k} = (\cos\tfrac{2\pi k}{8},\ \sin\tfrac{2\pi k}{8})\).
constexpr Complex< QuadraticReal< 2 > >	dedekind::numbers::ζ8
	The primitive 8th root of unity ζ8 = e^{2πi/8} = ½√2 + ½√2·i, exact in ℂ(ℚ(√2)) — the generator of the de Moivre map root8.
constexpr QuadraticReal< 2 >	half_root2
constexpr auto	dedekind::numbers::ℂ
	The canonical complex-number universe ℂ = 𝔸<Complex<QuadraticReal<2>>, Boole, ℶ_1> — the coat-hanger ℂ = Cplx(ℝ) over the genuine ℝ = ℚ(√2) (mirroring ℝ and 𝔻). Equality on ℚ(√2)[i] is decidable, so ℂ answers in Boole; ℶ_1 is the cardinality of the ℂ it models, not a logic.
constexpr auto	dedekind::numbers::ℤ
template<auto AmbientSet, std::size_t N = 1>
constexpr LatticeFactory< AmbientSet, N >	dedekind::numbers::lattice {}
	First-class lattice value: lattice<ℝ_d>.
constexpr auto	dedekind::numbers::embed_𝔹_ℕ_
	Canonical embedding 𝔹 ↪ ℕ: bool → Cardinality.
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).
constexpr ℍ_ℚ	q_i
constexpr ℍ_ℚ	q_j
constexpr ℍ_ℚ	q_k
constexpr ℍ_ℚ	q_neg1
constexpr 𝔸< Rational< default_integer >, Boole, ℵ_0 >	dedekind::numbers::ℚ
	The canonical rational-number universe ℚ = 𝔸<Rational<default_integer>> (post-#559).
constexpr auto	dedekind::numbers::embed_ℤ_ℚ_
	Restored variant-layer subalgebra embedding ℤ ↪ ℚ: SignedCardinality → Rational<default_integer>, \(n\mapsto n/1\).
template<IsInteger I = default_integer>
constexpr auto	dedekind::numbers::embed_𝕃_ℚ
	Exact dyadic embedding of the finite doubles into ℚ: 𝕃<double> → Rational.
constexpr auto	dedekind::numbers::ℝ
	The canonical real-number universe ℝ = 𝔸<QuadraticReal<2>, Boole, ℶ_1> — the coat-hanger.
constexpr auto	dedekind::numbers::ℝ_d
	The machine-real ambient: the finite doubles 𝕃<double>.
constexpr EmbedRationalToReal	dedekind::numbers::embed_ℚ_ℝ {}
	The canonical S-leg instance \(\mathbb{Q}\hookrightarrow\mathbb{R}\).
template<typename T>
constexpr bool	dedekind::numbers::is_transcendental_v = false
	Trait to mark a species as Transcendental (π, e).
constexpr Projection< 0 >	π
	The unary projection, the identity: the variable of a comprehension over one carrier.
constexpr auto	ℕ
constexpr Projection< 0 >	π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

complex__ℝ_ℂ_S_Leg_Witnesses

The S-leg ℝ ↪ ℂ (r ↦ (r,0)) is a genuine ring homomorphism, computed.

Typedef Documentation

ℍ_ℚ

using dedekind::numbers::ℍ_ℚ = Quaternion<Rational<>>

quaternion__Formal_Verification

The Hamilton relations i²=j²=k²=ijk=-1 and non-commutativity ij≠ji are not just documentation — they are compile-time proofs that the Quaternion multiplication table is correct.

default_integer

using dedekind::numbers::default_integer = dedekind::sets::SignedCardinality

export

Default signed-integer carrier used by downstream numeric layers (Rational, embeddings). Post-#670-sibling (ℚ retarget): anchored on sets::SignedCardinality (saturating ℤ proxy with ±ℵ_0 / NaZ escalation), mirroring how ℤ = 𝔸<SignedCardinality> in :integer. This is the discipline-consistent canonical ℤ carrier — ℚ = 𝔸<Rational<default_integer>> now uses the saturating variant uniformly.

Pre-retarget value: SignedExtensionalCardinal<> (cyclic finite fragment). The retarget is what the user asked for: "re-target rationals / ℚ in the same way as ℤ, ℕ, 𝔹".

LowerSet

template<IsRational Q = Rational<default_integer>>

using dedekind::numbers::LowerSet = Comprehension<𝔸<Q, Boole>, LowerCut<Q>>

export

The lower set of a real, \(\{q\in\mathbb{Q}\mid q<r\}\), as a set over \(\mathbb{Q}\).

Template Parameters

Q	the rational scalar carrier.

PrincipalRay

template<IsRational Q = Rational<default_integer>>

using dedekind::numbers::PrincipalRay = Interval<Q>

export

The ray \(\{q<p\}\) over \(\mathbb{Q}\): the lower set of a principal cut, \(\mathbb{Q}\hookrightarrow\mathbb{R}\) as the order datum.

Template Parameters

Q	the rational scalar carrier.

RationalPolynomial

template<IsInteger I = default_integer>

using dedekind::numbers::RationalPolynomial = dedekind::algebra::Polynomial<Rational<I>>

export

The polynomial ring over the rationals in one variable, ℚ[x]: algebra::Polynomial over the quotient field of the integer carrier I.

(ℚ)

The canonical rational-number universe is ℚ = 𝔸<Rational<default_integer>>{} above. The spine witnesses below pin ℚ's syntax / semantics / arrow-fabric witnesses against drift; the layout mirrors the numbers:integer spine for ℤ so that downstream code can scan one block per textbook carrier and find the same five witness slots.

Enumeration Type Documentation

KleenePolicy

enum class dedekind::numbers::KleenePolicy

exportstrong

How Unknown (undecided within budget) maps to Boolean set membership.

Inclusive: Unknown → in M (outer approximation, M_N ⊇ M_true) Exclusive: Unknown → not in M (inner approximation, M_N ⊆ M_true; with finite computation this is effectively ∅, since no finite prefix can witness orbit boundedness)

Function Documentation

abs2()

template<IsComplexScalar R>

R dedekind::numbers::abs2 ( const Complex< R > & z )

constexprexport

Squared norm abs2(z) = <z, z> = |z|² = re² + im²: exact, √-free.

The squared-norm primitive for ℂ, available for every IsComplexScalar R — including the exact, non-√-closed ℝ = ℚ(√2), where norm does not exist but abs2 does. Equals Re(z · conj z) (pinned below).

character()

template<unsigned N>

Character< N > dedekind::numbers::character ( dedekind::morphologies::Modular< N > m )

constexprexport

The character \(\chi_m\) at frequency m.

See also

Character

collapse_ternary()

bool dedekind::numbers::collapse_ternary ( Ternary t, KleenePolicy policy )

constexprnoexcept

Collapse a Ternary escape signal to Boolean set membership under policy. True = escaped → false (not in M) False = proven bounded → true (in M; unreachable by finite computation) Unknown → policy-dependent

collatz_reach_path()

ReachPath dedekind::numbers::collatz_reach_path ( std::size_t n )

constexprexport

True once 1 is present, Unknown before — a monotone {Unknown,True} absorptive path (the ℕ analogue of Mandelbrot's escape indicator).

Parameters

n

the seed.

conj()

template<IsComplexScalar R>

Complex< R > dedekind::numbers::conj ( const Complex< R > & z )

constexprexport

Complex conjugate: conj(a + bi) = a − bi.

The canonical ring involution of ℂ = ℝ[i]/(i²+1) fixing the real subfield {im = 0}. Previously lived only inline inside operator/ (z / w = z · conj(w) / |w|²); exported here as a first-class library primitive because two downstream uses ride it: the norm identity |z|² = Re(z · conj z) (witnessed below) and the even-spectrum symmetry c_k = conj(c_{−k}) that the Figure-5 analytic symmetry check rests on.

FIXME(#808): register as an arrow<Complex<R>, Complex<R>> carrying is_involution_v (category:involution) once the Spectrum<(ℤ/N)², ·> even-check (Tier 2) needs the arrow form; kept a plain function for now.

cos_n()

template<unsigned N>
requires (N == 8u)

DiscreteCos< N > dedekind::numbers::cos_n ( )

constexprexport

\(\cos_N = \Re\,\zeta_N^{(\cdot)}\) as an arrow.

See also

DiscreteCos

dot()

template<IsComplexScalar R>

R dedekind::numbers::dot ( const Complex< R > & z, const Complex< R > & w )

constexprexport

The real inner product on ℂ ≅ ℝ²: dot(z, w) = Re(z · conj w) = re_z·re_w + im_z·im_w.

The Hermitian form read through the ℝ²-realification of ℂ (scalar field R): the inner-product form of ℂ. With abs2 it holds for every IsComplexScalar R; the exact ℂ(ℚ(√2)) has no norm, because its field is not closed under √. abs2 and the Euclidean escape-test norm both derive from it, replacing the former bespoke |z|² = re²+im² formula with the inner-product-induced one. The codomain is R, not Complex<R>: the sesquilinear ℂ-valued form z·conj w is a richer layer that would break the R-typed norm consumers (cf. the Mandelbrot escape radius), so the realification is the default that slots into the existing metric.

embed_𝔹_ℕ()

template<typename S>
requires requires(S&& s) { dedekind::sets::image(embed_𝔹_ℕ_, std::forward<S>(s)); }

auto dedekind::numbers::embed_𝔹_ℕ ( S && s )

constexprexport

Set-level lift of embed_𝔹_ℕ_: image of a Boolean set S under the canonical mono 𝔹 ↪ ℕ.

Layer-1 entry per #602: names the construction at the call site rather than re-spelling image(embed_𝔹_ℕ_, S). The accepted input S is anything dedekind::sets::image already dispatches on — Singleton (:sets:singleton), std::set<bool> / std::unordered_set<bool> (:sets:extensional); lazy predicate sets join the dispatch table when #602's layer 2 lands. This is structurally the union of the IsSet universe-value carriers and the std-container carriers that image accepts today; the requires-clause checks well-formedness directly rather than gating through a single concept (which would exclude one or the other tier).

Mathematically: the image of S under the canonical mono 𝔹 ↪ ℕ is a subset of {0, 1} ⊂ ℕ containing whichever bool elements are in S.

embed_unsigned_integral()

template<IsNatural N, std::unsigned_integral U>

N dedekind::numbers::embed_unsigned_integral ( U v )

constexprexport

Canonical injection from std::unsigned_integral into any IsNatural domain N via its single-argument constructor.

std::unsigned_integral types are the machine/extensional approximation of ℕ. This arrow is the Liskov injection into a certified IsNatural domain (e.g. ExtensionalCardinal<K>). The reverse direction — projecting a certified natural back to a machine width — is realize_to_size_t(sentinel).

Template Parameters

N	The target IsNatural type.
U	A std::unsigned_integral source type (deduced).

euclidean_escape_radius_squared()

template<IsComplexScalar R>

auto dedekind::numbers::euclidean_escape_radius_squared ( R escape_radius_squared = R{4} )

constexprexport

Classical escape criterion: |z|² > r².

graph()

template<typename F>
requires dedekind::category::IsArrow<F> && std::equality_comparable<typename std::remove_cvref_t<F>::Codomain>

Graph< std::remove_cvref_t< F > > dedekind::relational::graph ( F f )

constexpr

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\).

Template Parameters

F	An IsArrow whose Codomain has decidable equality.

Parameters

f	The analytic arrow.

Returns

A Graph<F> (a :expressions Relation) whose GraphPredicate<F> membership carries f for composition.

Note

Not part of the Trsk grammar (Listing~6), on purpose: lifting an arrow to a relation forces image / preimage to be inferred from f rather than spelled point-free, which is the source of the lambda-opacity these reifications (GraphPredicate, FibrePredicate, PreimagePredicate) exist to contain. Prefer building relations point-free (the restricted product S*T|relpred and the Tarski operators); graph stays available for the arrow-composition path but is kept out of the grammar surface. Sibling of the doc-deprecated element scout.

Related surfaces (#824). The point-free arrow lift now exists as ap(f, π_I) → ProjApplyEq (the 𝑦 == f(𝑥) relpred) in :order, and image-membership decidability is read off the arrow's certificate in :category:image (ImageChi specialised for IsRetractableArrow → Boole / decidable, else the default Ternary::Unknown). Redefining graph itself as sugar over ap (graph(f) := 𝔸<X>*𝔸 <Y> | (𝑦==ap(f,𝑥))) is parked: the lift plus the decidability seam capture the value without the DSL relocation. The group-derived mileage — IsGroup ⟹ translations retractable ⟹ free decidable image — is #875. Corrections retained from the #870 CP review: forward membership \(b=f(a)\) gates on equality_comparable (not monicity); the pre-image capability gates on IsRetractableArrow / iso (monicity gives a single-valued pre-image, the retract a computable one).

lower_set()

template<IsRational Q>

LowerSet< Q > dedekind::numbers::lower_set ( const Cut< Q > & r )

constexprexport

\(r \mapsto \{q<r\}\): the real read as its lower set.

Template Parameters

Q	the rational scalar carrier.

M_kleene_N()

template<IsComplexScalar R, typename EscapeCriterion>
requires IsEscapeCriterion<EscapeCriterion, Complex<R>>

auto dedekind::numbers::M_kleene_N ( std::size_t max_iter, EscapeCriterion criterion )

constexprexport

Point-level N-step Kleene membership: M_kleene_N(n, p)(c) = True if orbit(c) escapes within n steps under p = Unknown if no escape witnessed within n steps

The epistemic Layer 2 object: captures what we know at depth n, before any Boolean collapse.

M_N()

template<IsComplexScalar R, typename EscapeCriterion>
requires IsEscapeCriterion<EscapeCriterion, Complex<R>>

auto dedekind::numbers::M_N ( std::size_t max_iter, EscapeCriterion criterion, KleenePolicy policy = KleenePolicy::Inclusive )

constexprexport

M_N: { c in C | M_kleene_N(n, p)(c) is not True, under policy }.

KleenePolicy::Inclusive (default, outer approximation): M_N ⊇ M_true — includes all undecided points; the standard rendering. KleenePolicy::Exclusive (inner approximation): M_N ⊆ M_true — only confirmed members; ≡ ∅ under finite computation.

M_tower()

template<IsComplexScalar R, typename EscapeCriterion>
requires IsEscapeCriterion<EscapeCriterion, Complex<R>>

auto dedekind::numbers::M_tower ( EscapeCriterion criterion, KleenePolicy policy = KleenePolicy::Inclusive )

constexprexport

Tower constructor: n |-> M_N(n, criterion, policy)

orbit_divergence_path()

template<IsComplexScalar R, typename EscapeCriterion>
requires IsEscapeCriterion<EscapeCriterion, Complex<R>>

auto dedekind::numbers::orbit_divergence_path ( const OrbitPath< R > & orbit, EscapeCriterion criterion )->DivergencePath< R >

constexprexport

The divergence spectrum of an orbit: a monotone DivergencePath<R>.

orbit_divergence_path(orbit, p)(n) = True if ∃ k ≤ n : p(z_k) (escape witnessed) = Unknown if ∀ k ≤ n : ¬p(z_k) (no escape yet)

Monotonicity: True is the absorbing element of Kleene OR, so once the path reaches True it stays there. A monotone {Unknown,True}-valued path is isomorphic to ℕ∞ — its information content is exactly the escape time. The result type DivergencePath<R> carries the sequences::IsAbsorptiveSequence shape (eventually constant for every c — see the class doc), making the eventual-constancy a type-level fact.

This is the Layer 1 intensional object; orbit_escape_time() is the efficient materialization.

orbit_escape_time()

template<IsComplexScalar R, typename EscapeCriterion>
requires IsEscapeCriterion<EscapeCriterion, Complex<R>>

std::optional< std::size_t > dedekind::numbers::orbit_escape_time ( const OrbitPath< R > & orbit, std::size_t max_iter, const EscapeCriterion & criterion )

constexprexport

The escape time: the first index k ≤ max_iter at which the orbit escapes, or nullopt if no escape is witnessed within the budget.

orbit_escape_time(orbit, n, p) = min { k ≤ n | p(z_k) } or nullopt

Equivalently: orbit_divergence_path(orbit, p).at(n) = True iff orbit_escape_time(orbit, n, p).has_value()

principal_ray()

template<IsRational Q>

PrincipalRay< Q > dedekind::numbers::principal_ray ( const Q & p )

constexprexport

\(p \mapsto \{q<p\}\): the rational embedded as the principal ray, extensionally lower_set(Cut<Q>{p}).

Template Parameters

Q	the rational scalar carrier.

sin_n()

template<unsigned N>
requires (N == 8u)

DiscreteSin< N > dedekind::numbers::sin_n ( )

constexprexport

\(\sin_N = \Im\,\zeta_N^{(\cdot)}\) as an arrow.

See also

DiscreteSin

TranscendentalSet()

template<typename R>
requires std::regular<R>

auto dedekind::numbers::TranscendentalSet ( )

constexprexport

The Transcendental Set (𝕋).

{ x ∈ ℝ | x is not a root of any rational polynomial }.

Variable Documentation

ζ8

Complex<QuadraticReal<2> > dedekind::numbers::ζ8

inlineconstexprexport

Initial value:

=
    root8(dedekind::morphologies::Modular<8u>{1})

The primitive 8th root of unity ζ8 = e^{2πi/8} = ½√2 + ½√2·i, exact in ℂ(ℚ(√2)) — the generator of the de Moivre map root8.

ℂ

auto dedekind::numbers::ℂ

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<Complex<QuadraticReal<2>>, Boole, ℶ_1>{}

The canonical complex-number universe ℂ = 𝔸<Complex<QuadraticReal<2>>, Boole, ℶ_1> — the coat-hanger ℂ = Cplx(ℝ) over the genuine ℝ = ℚ(√2) (mirroring ℝ and 𝔻). Equality on ℚ(√2)[i] is decidable, so ℂ answers in Boole; ℶ_1 is the cardinality of the ℂ it models, not a logic.

Per #559's chosen direction (option A): the named species symbols denote universe values (constexpr instances of 𝔸 over the carrier), not classifier-alias types. All seven species symbols (𝔹, ℕ, ℤ, ℚ, ℝ, ℂ, 𝔻) carry the canonical element <ℂ> scout spelling.

Post-HSP retarget: the carrier of ℂ is Complex<QuadraticReal<2>> — the 2nd-order quotient ℝ[i]/(i²+1) over the coat-hanger ℝ.

Cardinality is set explicitly to ℶ_1 (continuum) — the textbook cardinality of ℂ, matching ℝ — overriding 𝔸's ℵ_0 default. ℂ is in bijection with ℝ × ℝ and therefore shares ℝ's continuum cardinality.

Textbook construction: ℂ = ℝ[i]/(i²+1) — the H-leg witnessed below via quotient_algebra_base<Complex<R>> = R (the sibling of 𝔻 = ℝ[ε]/(ε²)).

ℕ

auto dedekind::sets::ℕ

inlineconstexpr

natural__Canonical_Species_Spine

The canonical natural-numbers universe ℕ = 𝔸<Cardinality>{} is defined and witnessed upstream in dedekind.sets:boundaries. This partition adds the numbers-/order-/algebra-layer witnesses on top and provides the embedding chain arrows 𝔹 ↪ ℕ ↪ ℤ that the upstream sets layer cannot reach.

ℚ

𝔸<Rational<default_integer>, Boole, ℵ_0> dedekind::numbers::ℚ

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<Rational<default_integer>>{}

The canonical rational-number universe ℚ = 𝔸<Rational<default_integer>> (post-#559).

Per #559's chosen direction (option A): the named species symbols (𝔹 / ℕ / ℤ / ℚ / ℝ / ℂ / 𝔻) denote the universe values (constexpr instances of 𝔸 over the carrier), not carrier types. Carrier types are spelled directly (Rational<default_integer>, or Rational for the parameterised form over an arbitrary IsInteger I) in template-type-parameter positions; ℚ alone is the universe value the set-builder DSL takes as ambient.

This makes element <ℚ> the canonical scout spelling — closer to textbook math notation than the pre-#559 element<𝔸 <ℚ>> form. Pre-#559 the spelling was using ℚ = ℚ_t<> (a carrier- type alias); the type-context sites in concept gates and static_asserts were migrated to Rational<default_integer> directly in step 1 of this slice.

algebra::IsField fires on Rational<default_integer>; see the probe near the bottom of this file.

ℝ

auto dedekind::numbers::ℝ

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<QuadraticReal<2>, Boole, ℶ_1>{}

The canonical real-number universe ℝ = 𝔸<QuadraticReal<2>, Boole, ℶ_1> — the coat-hanger.

Per #559 the named species symbols denote universe values (constexpr 𝔸 instances over the carrier). ℝ's carrier is the decidable FIELD QuadraticReal<2> = ℚ(√2): the universe ℝ is a set-indexed field (algebra::IsField, as ℚ = 𝔸<Rational> is), and its carrier is order-complete in the library's structural surrogate sense (totally ordered + dense + extrema). So the Ddk algebra hangs off ℝ the way analysis bootstraps from the reals.

Honest imperfection: ℚ(√2) is countable and so not genuinely Dedekind-complete (it only passes the surrogate, which ℚ passes too); the ℶ_1 cardinality tags the continuum we model, not the materialised carrier. Machine-double computation lives on ℝ_d (below). Further extensions (numerical subalgebras) and transcendentals (symbolic Expr) grow it. A documented placeholder — not a false postulate on an uninhabited carrier.

ℂ and 𝔻 are the sibling coat-hanger universe values (ℂ = ℝ[i]/(i²+1) = 𝔸<Complex<QuadraticReal<2>>>, 𝔻 = ℝ[ε]/(ε²) = 𝔸<Dual<QuadraticReal<2>>>), the 2nd-order quotient functors over this same ℝ.

ℝ_d

auto dedekind::numbers::ℝ_d

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<dedekind::morphologies::𝕃<machine_real_scalar>, Boole,
                      ℶ_1>{}

The machine-real ambient: the finite doubles 𝕃<double>.

NaN and +/-inf are excluded by the carrier's type, so the order is total and membership is decidable: ℝ_d is Boole, like ℝ. The ℶ_1 tag names the continuum ℝ_d approximates, as it does on ℝ; the carrier itself is the finite set of dyadic rationals a double holds. Only the (min, max) lattice reduct is claimed: IEEE rounding breaks the associativity of + and *. Rule of thumb: compute on ℝ_d; model on ℝ.

ℤ

auto dedekind::numbers::ℤ

inlineconstexprexport

Initial value:

=
    dedekind::sets::𝔸<dedekind::sets::SignedCardinality>{}

(#670)

ℤ is the universe 𝔸<SignedCardinality>, using the saturating variant sets::SignedCardinality as the carrier (rather than the cyclic finite fragment SignedExtensionalCardinal<>). This mirrors the ℕ pattern (ℕ = 𝔸<Cardinality>, where Cardinality is the saturating \(\mathbb{N} \cup \{\aleph_0\}\) variant) — the project's stance is now consistent across ℕ and ℤ: bounded representations escalate (saturate to \(\pm \aleph_0\)) rather than wrap.

The carrier sets::SignedCardinality is the project's documented bona-fide proxy for \(\mathbb{Z}\) modulo physical limits (cf. cardinality.cppm:923-924, "the library's bona-fide proxy for ℤ modulo physical limits") — arithmetic saturates to \(\pm \aleph_0\) on overflow rather than wrapping modulo \(2^{N \cdot 64}\). This is what the in-line scout-algebra surface (#664) requires for translation-invariant halfspace-pivot transport: the IsOrderedAdditiveGroup marker in :algebra:ordered_algebra is specialised to true for SignedCardinality and to false (default) for the cyclic finite fragment, exactly because the saturating discipline preserves order under translation and the cyclic one does not at the wrap boundary.

collatz

auto dedekind::numbers::collatz

inlineconstexprexport

Initial value:

=
    (n_even & halve) | (~n_even & triple_plus_1)

The Trsk relation \(T \subseteq \mathbb{N}\times\mathbb{N}\), spelled point-free as the McCarthy conditional \(T = (\text{even} \cap \text{halve}) \cup (\text{odd} \cap \text{triple})\) — no lambda, no graph, the recurrence is the relation, spelled in uniform set-grammar: & (meet), ~ (complement), | (join, the structural OrPredicate union of #365). Mirrors the divides relation of §4; the parity test appears exactly once.

Note

Whether the DSL infers IsFunction across the (disjoint, total) case split is the next investigation — functionality is inferred from a graph-shaped leaf or through >>, not yet across \(\cap/\cup\).

converged_2

auto dedekind::numbers::converged_2

inlineconstexprexport

Initial value:

= fibre(
    back2, finite_cardinality(1), finite_cardinality(2), finite_cardinality(4))

converges_in_1

auto dedekind::numbers::converges_in_1

inlineconstexprexport

Initial value:

=
    fibre(converse(collatz), finite_cardinality(1))

converges_in_1 \(= \mathrm{collatz}^{\circ}(1) = \{n \mid \mathrm{collatz}(n) = 1\}\) — the pre-image of the fixed-point target \(\{1\}\): the naturals that reach 1 in exactly one step. Point-free, via the converse fibre.

embed_ℝ_ℂ

auto dedekind::numbers::embed_ℝ_ℂ

inlineconstexprexport

Initial value:

=
    arrow<QuadraticReal<2>, Complex<QuadraticReal<2>>>(
        [](const QuadraticReal<2>& r) noexcept {
          return Complex<QuadraticReal<2>>{r, QuadraticReal<2>{}};
        })

The Birkhoff S leg \(\mathbb{R}\hookrightarrow\mathbb{C}\) over the coat-hanger: QuadraticReal<2> → Complex<QuadraticReal<2>>, \(r\mapsto (r,0)\).

A genuine monic ring embedding (an EmbedsAsSubalgebra S-leg, the ℂ sibling of embed_ℚ_ℝ): ℝ is the real subfield \(\{\,\mathrm{im}=0\,\} \subset\mathbb{C}\). The arrow is \(r\mapsto r+0i\), witnessed by computation below. Not registered is_monotone_v — ℂ carries no total order (that is exactly what the quotient by \((i^2+1)\) forfeits vs. ℝ).

embed_ℤ_ℚ_

auto dedekind::numbers::embed_ℤ_ℚ_

inlineconstexprexport

Initial value:

=
    arrow<default_integer, Rational<default_integer>>(
        [](const default_integer& n) {
          
          
          
          return Rational<default_integer>{n};
        })

Restored variant-layer subalgebra embedding ℤ ↪ ℚ: SignedCardinality → Rational<default_integer>, \(n\mapsto n/1\).

Restores the arrow the comment above anticipated ("on the new @b ℤ carrier @c SignedCardinality"), replacing the removed machine-layer arrow<int,…>. \(n\mapsto n/1\) is the genuine ring embedding of ℤ into its field of fractions ℚ: an EmbedsAsSubalgebra S-leg (the canonical tower rung below embed_ℚ_ℝ) that is also order-preserving (is_monotone_v) — the property the halfspace strength-reduction pulls back through. The homomorphism/injectivity laws are witnessed by computation below on the ring ℤ.

See also

PartialEmbedIntegerToRational — the same map \(n\mapsto n/1\) on the Ternary/Kleene surface, generic over I. embed_ℤ_ℚ_ is the categorical arrow over the canonical default_integer, carrying the monic / homomorphism / monotone registrations the tower's S-leg needs; the two are distinct surfaces, not a redundant fork.

embed_𝔹_ℕ_

auto dedekind::numbers::embed_𝔹_ℕ_

inlineconstexprexport

Initial value:

=
    arrow<bool, Cardinality>([](const bool& b) noexcept -> Cardinality {
      return finite_cardinality(b ? 1 : 0);
    })

Canonical embedding 𝔹 ↪ ℕ: bool → Cardinality.

False maps to finite_cardinality(0), True to finite_cardinality(1).

Sister arrow to embed_𝔹_uint_ above; this one lands in the Cardinality carrier (the canonical IsNatural witness of ℕ in the set-builder layer) directly, without routing through the machine-width unsigned proxy. Filed against #602 layer 1 (the set-level lift embed_𝔹_ℕ below uses this arrow to delegate through the existing sets::image dispatch).

embed_𝕃_ℚ

template<IsInteger I = default_integer>

auto dedekind::numbers::embed_𝕃_ℚ

inlineconstexprexport

Exact dyadic embedding of the finite doubles into ℚ: 𝕃<double> → Rational.

Every finite IEEE 754 double is exactly the dyadic rational m·2^e for integers m, e (mantissa, exponent). This arrow extracts the bit-pattern via std::bit_cast and constructs Rational{numerator, denominator} where the denominator is the relevant power of two. NaN and +/-inf cannot reach it: the domain 𝕃<double> excludes them by type, so under ℚ's faithful-field posture the arrow is total on its domain, and it is injective by the exactness of the dyadic decomposition (Knuth, TAOCP, Vol. 2, §4.2), hence registered monic below.

rational__Precision

The integer carrier I must hold the reduced 53-bit mantissa and the power-of-two scaling. For built-in signed I the arrow checks each step against std::numeric_limits and throws std::overflow_error rather than trip signed-overflow UB. The default default_integer (SignedCardinality) stands in for ℤ, and its saturation sentinel is ℚ's out-of-memory tripwire: Rational rejects it with std::domain_error. On the current one-word carrier the tripwire sits at 2^63, so a double whose mantissa or power-of-two scaling exceeds that (e.g. 1e20, 1e-20, every subnormal) trips it.

half_root2

QuadraticReal<2> dedekind::numbers::half_root2

constexpr

Initial value:

= QuadraticReal<2>::of(
    Rational<default_integer>{}, Rational<default_integer>{1, 2})

is_transcendental_v

template<typename T>

bool dedekind::numbers::is_transcendental_v = false

inlineconstexprexport

Trait to mark a species as Transcendental (π, e).

symbolic__Transcendental_Anchors

Defaults to false for base fields (Q).

q_i

ℍ_ℚ dedekind::numbers::q_i

inlineconstexpr

Initial value:

{Rational<>{0}, Rational<>{1}, Rational<>{0},
                         Rational<>{0}}

q_j

ℍ_ℚ dedekind::numbers::q_j

inlineconstexpr

Initial value:

{Rational<>{0}, Rational<>{0}, Rational<>{1},
                         Rational<>{0}}

q_k

ℍ_ℚ dedekind::numbers::q_k

inlineconstexpr

Initial value:

{Rational<>{0}, Rational<>{0}, Rational<>{0},
                         Rational<>{1}}

q_neg1

ℍ_ℚ dedekind::numbers::q_neg1

inlineconstexpr

Initial value:

{Rational<>{-1}, Rational<>{0}, Rational<>{0},
                            Rational<>{0}}

root8

auto dedekind::numbers::root8

inlineconstexprexport

Initial value:

=
    arrow<dedekind::morphologies::Modular<8u>, Complex<QuadraticReal<2>>>(
        [](const dedekind::morphologies::Modular<8u>& k) noexcept {
          using Rz = QuadraticReal<2>;
          const Rz s = Rz::of(Rational<default_integer>{},
                              Rational<default_integer>{1, 2});  
          const Complex<Rz> table[4] = {
              {Rz{1}, Rz{}},  
              {s, s},         
              {Rz{}, Rz{1}},  
              {Rz{} - s, s},  
          };
          const unsigned r = k.value & 3u;               
          const bool neg = ((k.value >> 2) & 1u) != 0u;  
          const Complex<Rz> z = table[r];
          return neg ? -z : z;
        })

The exact de Moivre exponential \(\zeta_8 : \mathbb{Z}/8 \to \mathbb{C}^\times\) over the coat-hanger ℝ = ℚ(√2): \(k \mapsto \zeta_8^{\,k} = (\cos\tfrac{2\pi k}{8},\ \sin\tfrac{2\pi k}{8})\).

complex__Roots_of_Unity_de_Moivre

The arithmetic heart of an 8-point DFT, made exact by the cyclotomic coincidence \(\sqrt 2 = \zeta_8 + \zeta_8^{-1}\): hence ℚ(√2) = ℝ ∩ ℚ(ζ₈) already contains every 8th root of unity, and the sole irrational the table needs is ½√2 = cos(π/4). The map is a group homomorphism \((\mathbb{Z}/8, +) \to (\mathbb{C}^\times, \cdot)\) — angle addition is exponent addition, de Moivre as a ring identity (witnessed below). Implemented via the half-turn fold \(\zeta_8^4 = -1\) (k = 4q+r) so the whole μ₈ table — and its real-zero set — are shallow compile-time facts, not the deep iterated-multiplication chain that would exhaust the constant-evaluation budget.

Library fact (the Figure-5 anchor): the cosine-node set \(\{k : \operatorname{Re}\zeta_8^k = 0\}\) is exactly the residue class \(2 \pmod 4\) — a finite-quotient predicate morphologies::Congruence<4,2>. So the ℂ(ℚ(√2)) node test factors through the finite quotient Modular<4>; the strength reduction that keeps materialisation on a cheap integer surrogate is this residue-class identity, not insight poured into the exhibit.