integer.cppm File Reference

Minimal number taxonomy concepts for reintegration. More...

#include <concepts>
#include <functional>
#include <limits>
#include <numeric>
#include <optional>
#include <type_traits>
import dedekind.numbers:natural;
import dedekind.sets;
import dedekind.relational;
import dedekind.order;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for integer.cppm:

Namespaces
namespace	dedekind::numbers
namespace	dedekind::category

Typedefs
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.
using	dedekind::numbers::detail_step_adjunction::Z = SignedCardinality
using	dedekind::numbers::detail_step_adjunction::S = Successor<Z>
using	dedekind::numbers::detail_step_adjunction::P = Predecessor<Z>
using	dedekind::category::SignedCardinality
	Signed counterpart of Cardinality with ±ℵ_0 escalation; the library's bona-fide proxy for \(\mathbb{Z}\) modulo physical limits.

Functions
consteval bool	dedekind::numbers::detail_step_adjunction::inverts_on_sample ()
consteval bool	dedekind::numbers::detail_step_adjunction::unit_and_counit_at_the_ends ()
consteval bool	dedekind::numbers::detail_step_adjunction::reverse_counit_fails_at_the_top ()
consteval bool	dedekind::numbers::detail_step_adjunction::saturation_breaks_the_bijection ()
consteval bool	dedekind::numbers::detail_step_adjunction::converse_is_predecessor_on_sample ()
consteval bool	dedekind::numbers::detail_step_adjunction::lambek_fails_at_minus_one ()
constexpr auto	dedekind::numbers::detail_step_adjunction::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::detail_step_adjunction::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::ℤ
template<>
constexpr bool	dedekind::category::is_adjoint_v< Successor< SignedCardinality >, Predecessor< SignedCardinality >, std::less_equal<> > = true
	S ⊣ P on the saturating ℤ. Both legs are monotone (order:completeness); the unit \(x \le P(S(x))\) and the counit \(S(P(y)) \le y\) hold everywhere, at the ends by saturation ( \(P(S(\max)) = P(+\aleph_0) = +\aleph_0 \ge \max\)). The reverse P ⊣ S fails at the top, \(P(S(\max)) = +\aleph_0 > \max\), and S is no bijection, \(S(\max) = S(+\aleph_0)\): saturation keeps one of the two adjunctions ℤ proper has, and the witnesses in the numbers block say which.
constexpr Z	dedekind::numbers::detail_step_adjunction::largest_finite
constexpr Z	dedekind::numbers::detail_step_adjunction::smallest_finite

Detailed Description

Minimal number taxonomy concepts for reintegration.

@partition :integer

Copyright

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

Note

"Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk." ("God made the integers; all else is the work of man.") – Leopold Kronecker, Jahresbericht der DMV 2 (1891, reported)

Function Documentation

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

Variable Documentation

largest_finite

Z dedekind::numbers::detail_step_adjunction::largest_finite

inlineconstexpr

Initial value:

= finite_signed_cardinality(
    std::numeric_limits<SignedExtensionalCardinal<>::signed_type>::max())

smallest_finite

Z dedekind::numbers::detail_step_adjunction::smallest_finite

inlineconstexpr

Initial value:

= finite_signed_cardinality(
    std::numeric_limits<SignedExtensionalCardinal<>::signed_type>::min())