ordered_algebra.cppm File Reference

Ordered-algebra markers and concepts: carriers whose order is compatible with their group / ring / field structure (#664, #895). More...

#include <functional>
#include <type_traits>
import dedekind.algebra:group;
import dedekind.sets;
import dedekind.category;

Include dependency graph for ordered_algebra.cppm:

Classes
struct	dedekind::algebra::is_translation_invariant_ordered< T >
	Marker trait: T is a non-cyclic ordered additive group whose order is translation-invariant, with the saturating escape contract for values that would exceed representable capacity. More...
struct	dedekind::algebra::is_translation_invariant_ordered< dedekind::sets::SignedCardinality >
	sets::SignedCardinality is the project's bona-fide saturating proxy for \(\mathbb{Z}\): arithmetic escalates to \(\pm \aleph_0\) on overflow and propagates NaZ on indeterminate forms, rather than wrapping modulo capacity (cf. cardinality.cppm:923-967). This is the structural guarantee the marker certifies: translation preserves the partial order \(\le\) on the finite fragment; saturation collapses ordering past the boundary into the \(\pm \aleph_0\) sentinel (the meet still holds: both sides land at the same sentinel). The finite-fragment carrier SignedExtensionalCardinal is intentionally not opted in: it is cyclic (mod \(2^w\)), so its addition would reverse the order at the wrap boundary. The variant SignedCardinality is what callers should use whenever they want translation-invariance at the type level (i.e. the halfspace pipe). More...
struct	dedekind::algebra::is_scaling_invariant_ordered< T >
	The MULTIPLICATIVE order-compatibility axiom marker (O2): the positive cone is closed under *, i.e. 0≤a ∧ 0≤b ⟹ 0≤a·b — equivalently, scaling by a positive preserves the order. The multiplicative sibling of is_translation_invariant_ordered (O1, scaling ↔ translation). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::algebra::IsOrderedAdditiveGroup
	An additive group whose order is translation-invariant.
concept	dedekind::algebra::IsOrderedMultiplicativeGroup
	An ordered field — the textbook home of multiplicative scaling of halfspaces.
concept	dedekind::algebra::IsOrderedCommutativeRing
	A commutative ring whose carrier is ordered under the additive translation marker.

Typedefs
template<typename G>
using	dedekind::algebra::AdditiveInverse = Inverse<G, std::plus<G>>
	The additive inverse x ↦ -x — the additive instance of the reified group-inverse arrow Inverse (:group).

Variables
template<typename T>
constexpr bool	dedekind::algebra::is_translation_invariant_ordered_v
template<typename T>
constexpr bool	dedekind::algebra::is_scaling_invariant_ordered_v
template<typename G, typename Op>
constexpr bool	dedekind::category::is_antimonotone_v< dedekind::algebra::Inverse< G, std::plus< G > >, Op > = true
	The additive group inverse Inverse<G, +> is antitone exactly on an ordered additive group (translation invariance is the hypothesis of the -b≤-a step), so the registration is gated on IsOrderedAdditiveGroup — the algebraic dog-food of the antitone reification (#959).
template<>
constexpr bool	dedekind::category::is_adjoint_v< dedekind::algebra::AdditiveInverse< dedekind::sets::SignedCardinality >, dedekind::algebra::AdditiveInverse< dedekind::sets::SignedCardinality >, std::less_equal<> > = true
	The theorem: an antitone involution is self-adjoint, \(a \le -b \iff b \le -a\). The law leg of the witness below.

Detailed Description

Ordered-algebra markers and concepts: carriers whose order is compatible with their group / ring / field structure (#664, #895).

@partition :ordered_algebra

Copyright

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

ordered_algebra__Motivation

Compatibility of a total order with the algebraic operations is a \(\forall\)-law over VALUES, not a property of types or operation signatures. A concept can only inspect the latter, so the order- compatibility axioms are carried by opt-in markers (is_translation_invariant_ordered / is_scaling_invariant_ordered) that a carrier specialises when its arithmetic genuinely preserves the order. The markers are then composed with the type-indexed algebraic concepts (IsAbelianGroup / IsCommutativeRing / IsField) to give the ordered-algebra concepts (IsOrderedAdditiveGroup / IsOrderedCommutativeRing / IsOrderedMultiplicativeGroup). The additive marker is the translation-invariance axiom for an ordered group, made a per-carrier opt-in; the field concepts add the Artin–Schreier order-compatibility axioms that pin an ordered (formally real) field.

ordered_algebra__Consumers

These concepts are the algebraic preconditions for halfspace transport and the ordered-numeric carriers: they are consumed by :algebra:halfspace_transport, :numbers:complex, :numbers:rational, :numbers:quadratic, :numbers:integer, and :morphologies:integral.

Note

This partition was split out of the retired :scout_algebra partition under #895 (scout sunset). It houses only the live ordered-algebra concept layer; the symbolic scout-algebra scaffolding (GroupScout et al.) that formerly shared the partition had zero live consumers and was deleted separately.

Wikipedia: Ordered field, Linearly ordered group, Artin-Schreier theory

Note

"Die Zahlen sind freie Schöpfungen des menschlichen Geistes." [Trans: "Numbers are free creations of the human mind."] – Richard Dedekind, Was sind und was sollen die Zahlen?, Vorwort (1888)

Typedef Documentation

AdditiveInverse

template<typename G>

using dedekind::algebra::AdditiveInverse = Inverse<G, std::plus<G>>

export

The additive inverse x ↦ -x — the additive instance of the reified group-inverse arrow Inverse (:group).

On an ordered additive group it is antitone (order-reversing): from a≤b, add (-a-b) to both sides and use translation invariance to obtain -b≤-a. This is the algebraic witness that a unary field inverse reverses order (#908 / #959) — the same antitone shape as the logic NegationArrow's ¬ on Ω, one structure down (the additive group's own ¬).

Variable Documentation

is_scaling_invariant_ordered_v

template<typename T>

bool dedekind::algebra::is_scaling_invariant_ordered_v

inlineconstexprexport

Initial value:

=
    is_scaling_invariant_ordered<T>::value

is_translation_invariant_ordered_v

template<typename T>

bool dedekind::algebra::is_translation_invariant_ordered_v

inlineconstexprexport

Initial value:

=
    is_translation_invariant_ordered<T>::value