dedekind.algebra Module Reference

Concepts
concept	dedekind::category::IsQuotientAlgebra
	Q is declared as a quotient of some base algebra.
concept	dedekind::category::IsCongruenceQuotient
	Q is a quotient of a carrier V by a declared congruence R for Op and reduces from V — the relational reading of the H leg.
concept	dedekind::category::IsProductAlgebra
	Q is declared as a finite direct product of some base algebra.
concept	dedekind::category::IsSubalgebra
	Subobject S of A is a subalgebra under operation Op when it is closed under Op.
concept	dedekind::category::IsSubalgebraOf
	S is declared as a subalgebra of some base algebra.
concept	dedekind::algebra::IsInitialRing
	R is the initial object in Ring — for every ring S there exists a unique ring homomorphism R → S.
concept	dedekind::algebra::IsGrothendieckGroup
	G is the Grothendieck group of the commutative monoid M — the free abelian group on M, equivalently the left adjoint of the forgetful functor Ab → CMon applied at M.
concept	dedekind::algebra::HasGroupOperatorsAdd
	Pure syntactic shape: T closes strictly under the additive-group operator surface +, binary -, unary -.
concept	dedekind::algebra::HasGroupOperatorsMul
	Pure syntactic shape: T closes strictly under the multiplicative-group operator surface *, /, and exposes the multiplicative unit T{1}.
concept	dedekind::algebra::HasSuccessorOperators
	Pure syntactic shape: T supports the successor / predecessor operator surface (pre- and post-increment / -decrement, all four).
concept	dedekind::algebra::HasCompoundGroupOperatorsAdd
	Pure syntactic shape: T supports the in-place additive-group operator surface +=, -=.
concept	dedekind::algebra::HasCompoundGroupOperatorsMul
	Pure syntactic shape: T supports the in-place multiplicative-group operator surface *=, /=.
concept	dedekind::algebra::IsGroup
	Proposition: a set object X whose carrier X::Domain forms a group — the set-indexed lift of category::IsGroup.
concept	dedekind::algebra::IsAdditiveGroup
	Proposition: a set object X whose carrier is a group under +.
concept	dedekind::algebra::IsMultiplicativeGroup
	Proposition: a set object X whose carrier is a group under *.
concept	dedekind::algebra::IsArithmeticAdditiveGroup
	The ℤ-deal: a carrier that is an additive group AND whose group structure agrees with the standard C++ +, -, unary - operators.
concept	dedekind::algebra::IsVectorSpace
	The Gold Standard: A Module where the Scalar is a Field.
concept	dedekind::algebra::IsFieldElement
	A bona fide element of a field is a 1D vector space over itself.
concept	dedekind::algebra::HasVectorSpaceOperators
	Pragmatic vector-space check used by first reified vector carriers.
concept	dedekind::algebra::SatisfiesVectorSpaceAxioms
	Operational witness of the core vector-space axiom signatures.
concept	dedekind::algebra::IsGaloisField
	A finite field, as an algebraic set: an ETCS set X whose carrier X::Domain is an axiomatic field with the carrier-author finite-cardinality opt-in.
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.
concept	dedekind::algebra::IsTropical
	A dioid: an IsSemiring whose additive monoid Add is idempotent (a semilattice). This is the algebraic gate for the tropical carriers, refining IsSemiring exactly by ⊕-idempotence.
concept	dedekind::algebra::IsMonoid
	Proposition: a set object X whose carrier X::Domain forms a monoid — the set-indexed lift of category::IsMonoid.
concept	dedekind::algebra::IsAdditiveMonoid
	Proposition: a set object X whose carrier is a monoid under +.
concept	dedekind::algebra::IsMultiplicativeMonoid
	Proposition: a set object X whose carrier is a monoid under *.
concept	dedekind::algebra::HasRingOperators
	Pure syntactic shape: T closes strictly under +, -, * (binary and unary -). Textbook closure — results are exactly T, not just convertible to T.
concept	dedekind::algebra::IsSemiring
	The set-indexed lift of category::IsSemiring (an exact alias of category::IsRig): the "rig" rung of the tower.
concept	dedekind::algebra::IsRig
concept	dedekind::algebra::IsRng
concept	dedekind::algebra::IsRing
	The set-indexed lift: a set object X whose carrier X::Domain is both a Semiring AND an Abelian Group under addition.
concept	dedekind::algebra::IsArithmeticRing
	The seal: a carrier that is a ring AND whose ring structure agrees with the standard C++ arithmetic operators.
concept	dedekind::algebra::IsCommutativeRing
	A Ring where multiplication is also commutative.
concept	dedekind::algebra::HasSemiringOperators
	Pure syntactic shape: T closes strictly under + and *, with structural identities T{} and T{1}.
concept	dedekind::algebra::IsRingHomomorphism
	A callable φ from Source to Target that carries the ring structure: \(\varphi(a + b) = \varphi(a) + \varphi(b)\), \(\varphi(a b) = \varphi(a) \varphi(b)\), \(\varphi(0) = 0\) and \(\varphi(1) = 1\) (Lang, Algebra, §II.1).
concept	dedekind::algebra::IsClosedAlgebra
	The closure-only tier of an (A, F) algebra: each Op closes on T, without the value-semantics requirement.
concept	dedekind::algebra::IsAlgebra
	The universal-algebra (A, F) pattern at the closure tier.
concept	dedekind::algebra::IsAlgebraOnSet
	An algebraic set: a Tarski set whose carrier is closed under a family of operations. This is the Ddk = Trsk ∩ Alg layer, spelt out as its two conjuncts.
concept	dedekind::algebra::IsTotalAlgebra
	The universal-algebra (A, F) pattern at the totality tier — every operation closes on the carrier and is total under the carrier's chosen totality path (Periodic / Idempotent / Saturating).
concept	dedekind::algebra::HasCarrier
	The HAS-A posture in code: an Algebra HAS-A Carrier (under operations Ops) iff the carrier closes the operations (IsAlgebra), the carrier is mereologically a part of the algebra, and the algebra exposes the part via the arrow_drill_down projector.
concept	dedekind::algebra::AlgebraAsProduct
	Set-level sibling of HasCarrier: an algebra is a product of (set object, operations on the underlying type).
concept	dedekind::algebra::IsHomomorphism
	An arrow \(f : A \to B\) between two algebras that carries each operation of the signature S on \(A\) to the one in the same place of T on \(B\): \(f(x \odot y) = f(x) \circledast f(y)\) and \(f(e) = e'\) for each (Burris and Sankappanavar, A Course in Universal Algebra, §II.6).
concept	dedekind::algebra::IsQuotientMorphism
	An arrow that is both a homomorphism of the signatures and surjective (via category::is_epic_arrow_v).
concept	dedekind::algebra::EmbedsAsSubalgebra
	The Birkhoff S leg as an arrow: a monic homomorphism, i.e. a structure-preserving embedding whose image is a subalgebra.
concept	dedekind::algebra::IsIntegralScalar
	Internal bridge for std::integral scalar carriers.
concept	dedekind::algebra::IsUnsignedIntegralScalar
	Internal bridge for std::unsigned_integral scalar carriers.
concept	dedekind::algebra::IsFloatingScalar
	Internal bridge for std::floating_point scalar carriers.
concept	dedekind::algebra::IsModule
	An Abelian Group participating in a Linear Action by a Ring.
concept	dedekind::algebra::IsScalar
	A bona fide scalar is a 1D semi-module over itself.
concept	dedekind::algebra::HasFieldOperators
	Pure syntactic shape: T closes strictly under the full field operator surface +, binary -, unary -, *, /, and exposes the multiplicative unit T{1}.
concept	dedekind::algebra::IsField
	The set-indexed lift of the axiomatic category::IsField: a set object X whose carrier X::Domain is a field.
concept	dedekind::algebra::IsAlgebraicallyClosed
	The "Soul" of the Field: Every polynomial has a root in the species.
concept	dedekind::category::IsFreeAlgebra
	F is declared as the free algebra over some base R.
concept	dedekind::algebra::IsDivisionRing
	A Ring establishing the existence of Multiplicative Inverses.
concept	dedekind::algebra::IsEuclidean
	A Commutative Ring endowed with a division algorithm.
concept	dedekind::algebra::IsMagma
	Proposition: a set object X whose carrier X::Domain forms a magma — the set-indexed lift of category::IsMagma.

Classes
struct	dedekind::category::quotient_algebra_base< Q >
	quotient_algebra_base<Q>: carrier-side declaration that Q is a quotient of some base algebra. Specialise the ::type member at the carrier-defining partition (e.g.\ Complex<R> in numbers:complex records quotient_algebra_base<Complex<R>>::type = R). More...
struct	dedekind::category::quotient_congruence< Q >
	quotient_congruence<Q>: carrier-side declaration of the congruence witnessing Q = V/R. ::type is the relation R, ::carrier is the carrier V that R lives on (R is a homogeneous relation on V). Mirrors the S-leg's subalgebra_base. More...
struct	dedekind::category::product_algebra_base< Q >
	product_algebra_base<Q>: carrier-side declaration that Q is a finite direct product of some base algebra (the P operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition (e.g.\ Vec2V<T> in linear_algebra:vec2 records product_algebra_base<Vec2V<T>>::type = T). More...
struct	dedekind::category::subalgebra_base< S >
	subalgebra_base: carrier-side declaration that S is a subalgebra of some base algebra (the S operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition; the propagation specs below then lift the species-trait pins from base to S. More...
struct	dedekind::algebra::Inverse< G, Op >
	The group inverse under Op, reified as an arrow (an endomorphism G → G). More...
struct	dedekind::algebra::Bit2U64Action
	Scalar action \(\mathbb{F}_2 \times \mathbb{F}_2^{64} \to \mathbb{F}_2^{64}\) on (bool, uint64_t). More...
struct	dedekind::algebra::𝔽64
	The Galois field of order 64, \(\mathrm{GF}(2^6) = \mathbb{F}_2[x] / (x^6 + x + 1)\). More...
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...
struct	dedekind::algebra::Tropical< T, Max >
	Tropical carrier T ∪ {∞}. finite==false is the ⊕-identity sentinel (−∞ for Max, +∞ for Min), absorbing under ⊗. operator+ is ⊗ (honest addition); ⊕ is TropicalPlus. More...
struct	dedekind::algebra::TropicalPlus
	⊕: the tropical addition, the order-extremum (a semilattice join for Max, meet for Min). Named, not an operator, so a+b never silently means max. More...
struct	dedekind::algebra::Monomial< N >
	A monomial in N variables: its exponents, one per slot (π is the slot 0; π_1, π_2, π_3 the slots 1, 2, 3). The free commutative monoid on N generators, written multiplicatively (the exponents add, as natural numbers: leaving the word raises), and a chain under the graded lexicographic order: by total degree, then by exponents. More...
class	dedekind::algebra::Polynomial< R, M >
	The monoid algebra R[M]: a finitely supported function from the monomials to the coefficients, stored as its support sorted along the monomials' chain, no coefficient zero. A net (Domain the monomials, Codomain the coefficients, p(m) the coefficient of m), a commutative rig over a commutative rig, a ring over a ring (- where R has additive inverses). More...
struct	dedekind::algebra::Poly< C, N >
	The polynomial reading of a term on the carrier C, an algebra for cata: a projection is its variable, a constant a coefficient, + - * the polynomial's where the carrier admits them, a division by a nonzero constant on a field the multiplication by its inverse. Any other node (//, %, a division by a term, an applied arrow, a conditional) has no free algebra catalogued here and is refused. Expanding into polynomials uses commutativity of * and its distributivity over +, so the carrier must be a certified commutative rig. More...
struct	dedekind::algebra::semiring_ops< S >
	Canonical semiring operations of a carrier, so combinators can default their Add / Mult without a call site spelling them. The default (this primary) is the ordinary ring (+, ×), which is correct for any carrier whose native operators are its semiring ops; carriers whose ops differ specialize (the burden of proof sits at the implementation site): Tropical → (⊕ = TropicalPlus, ⊗ = +), bool → (∨, ∧) — bool must NOT take the default (bool bool promotes to int). This single defaulted seam replaces the old detection(empty-primary)/resolution(semiring_ops_of) split. More...
struct	dedekind::algebra::Signature< Ops >
	A signature, the \(F\) of an \((A, F)\) algebra named as one type: the Ops... of IsAlgebra, IsAlgebraOnSet and HasCarrier, which a concept can then take as a parameter and default. More...
struct	dedekind::algebra::OneDimensionalVector< S, Tag >
	Reified carrier for a 1D module/vector-space coordinate. More...
struct	dedekind::algebra::BoolLineJoin
	Additive join on 1D Boolean vectors (OR). More...
struct	dedekind::algebra::BoolLineMeetAction
	Scalar action on 1D Boolean vectors via meet (AND). More...
struct	dedekind::category::free_algebra_base< F >
	free_algebra_base<F>: carrier-side declaration that F is the free algebra over some base R (the textbook companion to HSP; cf. Burris–Sankappanavar §II.11). Specialise the ::type member at the carrier-defining partition (e.g. Polynomial<R, M> in algebra:polynomial records free_algebra_base<Polynomial<R, M>>::type = R). More...

Typedefs
template<typename Q>
using	dedekind::category::quotient_algebra_base_t = typename quotient_algebra_base<Q>::type
	Convenience alias for quotient_algebra_base<Q>::type.
template<typename Q>
using	dedekind::category::quotient_congruence_t = typename quotient_congruence<Q>::type
	Convenience alias for quotient_congruence<Q>::type (the congruence relation R).
template<typename Q>
using	dedekind::category::quotient_congruence_carrier_t = typename quotient_congruence<Q>::carrier
	Convenience alias for quotient_congruence<Q>::carrier (the carrier V that the congruence lives on).
template<typename Q>
using	dedekind::category::product_algebra_base_t = typename product_algebra_base<Q>::type
	Convenience alias for product_algebra_base<Q>::type.
template<typename S>
using	dedekind::category::subalgebra_base_t = typename subalgebra_base<S>::type
	Convenience alias for subalgebra_base<S>::type.
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).
template<typename T>
using	dedekind::algebra::MaxPlus = Tropical<T, true>
template<typename T>
using	dedekind::algebra::MinPlus = Tropical<T, false>
template<typename S>
using	dedekind::algebra::semiring_signature
	The semiring signature a carrier registers, (⊕, ⊗) off semiring_ops: the default family of a homomorphism.
using	dedekind::algebra::RealLine = OneDimensionalVector<dedekind::ieee::IEEE<double>>
	Alias: reals seen as a canonical 1D vector carrier.
using	dedekind::algebra::UnsignedLine = OneDimensionalVector<unsigned int>
using	dedekind::algebra::BoolLine = OneDimensionalVector<bool>
using	dedekind::algebra::RealLineScalar = decltype(RealLine{}.coordinate())
template<typename F>
using	dedekind::category::free_algebra_base_t = typename free_algebra_base<F>::type
	Convenience alias for free_algebra_base<F>::type.

Functions
constexpr 𝔽64	dedekind::algebra::operator* (bool s, 𝔽64 v) noexcept
	Scalar action of \(\mathbb{F}_2\) (witnessed on bool) on 𝔽64, via the natural embedding \(\mathbb{F}_2 \hookrightarrow \mathbb{F}_{64}\) ( \(0 \mapsto 0\), \(1 \mapsto 1\)).
constexpr 𝔽64	dedekind::algebra::inverse (𝔽64 a, std::plus< 𝔽64 >) noexcept
	The additive (group) inverse of 𝔽64, spelled as the computable inverse(a, std::plus) free function that category::inverse_v routes through by ADL.
auto	dedekind::algebra::f64_primitive_powers ()
	Enumerate \(\mathbb{F}_{64}^{\times}\) as the cyclic walk \(\alpha^0, \alpha^1, \ldots, \alpha^{62}\).
template<typename C, typename T>
constexpr auto	dedekind::algebra::canonical (const T &t)
	The normal form of the term t in the polynomials over C: the fold of Poly<C>. Two terms are equal in the free algebra iff their normal forms are.
template<typename K, typename C, std::size_t N, typename Lift>
dedekind::sets::Term< K >	dedekind::algebra::as_term (const Polynomial< C, Monomial< N > > &p, const Lift &lift)
	A polynomial written back as a term of the grammar: its terms from the leading monomial down, each the coefficient times the product of its variables (a coefficient 1 omitted), summed; the zero polynomial is the constant 0.
template<typename C>
constexpr C	dedekind::algebra::unit_normaliser (const C &)
	A unit u of the carrier with u·c the chosen representative of c's associates (the elements c times a unit): the hook the normal form of an equation divides by. 1 by default, nothing divided out; a carrier with more units states its own overload, found by ADL.
template<std::unsigned_integral W> requires (!std::same_as<W, bool>) && (sizeof(W) >= sizeof(unsigned))
constexpr W	dedekind::algebra::unit_normaliser (const W &c)
	On a word, ℤ/2ⁿ: c = 2ᵏ·o with o odd, and the odd elements are the units, so o⁻¹ (Newton's iteration, 2-adic: each step doubles the correct low bits) makes u·c = 2ᵏ. 0 has no unit part.
template<typename P, typename K, typename Lift>
dedekind::sets::Pred< K >	dedekind::algebra::canonical (const dedekind::sets::Pred< K > &p, const Lift &lift, const P &rep=P{})
	The normal form of a predicate at points of P: its conditionals lifted out of the atoms (lift_conditionals, so an applied set ap(S, t) reads as S's predicate at t), then atom by atom, each atom in its operands' sort (a point of one carrier has one; a pair of two carriers two, each axis its own), a decided atom ⊤ or ⊥ and folded into its connective. Equal normal forms cut out equal sets; different ones need not (πᵖ = π everywhere on 𝔽ₚ). An atom outside the catalogue is refused (not_admitted).
template<typename S> requires requires(S&& s) { dedekind::sets::image(embed_𝔹_𝕂3_, std::forward<S>(s)); }
constexpr auto	dedekind::algebra::embed_𝔹_𝕂3 (S &&s)
	Set-level lift of embed_𝔹_𝕂3_: image of a Boolean set S under the canonical mono 𝔹 ↪ 𝕂3.
template<IsUnsignedIntegralScalar S, typename Tag>
constexpr OneDimensionalVector< S, Tag >	dedekind::algebra::scale_strength_reduced (const OneDimensionalVector< S, Tag > &v, S factor)
	Strength-reduced scaling for unsigned 1D vectors.
template<typename C> requires dedekind::category::IsField<C, std::plus<C>, std::multiplies<C>> && dedekind::category::IsClosedUnder<C, std::divides<>>
constexpr bool	dedekind::sets::admits (On< C >, FieldDivision, bool divisor_is_constant)
	Division by a nonzero constant is in a field's signature: multiplication by the inverse (category::IsField, the axiomatic claim; the carrier closes under /). Its free algebra is the field's polynomials, with the constant's inverse a coefficient (:polynomial).
template<typename T, typename K, typename L, typename C> requires dedekind::category::IsGroup<T, std::plus<T>>
constexpr auto	dedekind::order::inverse (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K > > &g)
	inverse of a translation graph = its CONVERSE, the translation by the group inverse of the shift, again a graph. The inverse is the group's unary inverse (category::inverse_v), not the carrier's operator-: IsGroup guarantees a group inverse, not a negation operator, and on a characteristic-two field the two differ. Gated on IsGroup under the very std::plus the graph evaluates. On a wrapping group such as unsigned the inverse folds modulo capacity, the correct converse of a bijection; so the inverse is taken in the carrier, after the shift is cast into it.
template<typename T, typename K, typename L, typename C> requires dedekind::category::IsAbelianGroup<T, std::plus<T>>
constexpr auto	dedekind::order::image (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K > > &)
	image of a translation graph = the whole carrier: a translation is a bijection on any additive group (a cyclic one included), hence onto. On ℕ (not a group) x+k misses {0,…,k−1}, so the gate is the group.
template<IsTotallyOrdered T, typename K, Rel R, typename V, IsOckhamAlgebra L, IsCardinality C> requires (is_order_rel(R) && (dedekind::algebra::IsOrderedAdditiveGroup<T> || std::same_as<T, dedekind::sets::Cardinality>))
constexpr auto	dedekind::order::image (const Comprehension< 𝔸< std::pair< T, T >, L, C >, ProductRestrict< Translation< K >, Cylinder< R, 1, V > > > &s)
	image of a translation graph restricted to {x⋈p}: the affine pushforward {y⋈p+k}, a halfspace of the same shape. Order comparisons only (equality restricts to a point, not a halfspace), and only where the translation preserves the order: an ordered additive group, or ℕ (a constant cannot be negative there); a wrapping carrier is excluded.
template<IsTotallyOrdered T, typename K, Rel R, typename V, IsOckhamAlgebra L, IsCardinality CU> requires (is_order_rel(R))
constexpr Interval< T, L >	dedekind::order::image (const Comprehension< 𝔸< std::pair< T, T >, L, CU >, ProductRestrict< Scaling< K >, Cylinder< R, 1, V > > > &s)
	image of a restricted scaling x↦c·x, c=±1, on {x⋈p}: the ray scaled by c, its sense flipped when c<0. The sense depends on the constant's value, so the result is the value leaf Interval. c=−1 needs a genuine order-reversing additive inverse (IsOrderedAdditiveGroup); any other scale has no ray for an image here and is refused.
template<typename R> requires dedekind::category::is_right_unique_v<R> && dedekind::category::is_left_total_v<R>
consteval bool	dedekind::order::is_function (const R &)
	is_function(R) for a relation the certificates decide: functional and entire. No overload where they are silent.
template<typename R> requires dedekind::category::is_left_total_v<R>
consteval bool	dedekind::order::is_entire (const R &)
	is_entire(R): true for a relation certified entire; a codomain bound (alone or with a residue) on the unbounded ℤ-like carrier pulls the domain back to a proper subset. ℕ is not matched for the codomain cases: a lower bound there can be vacuous, so no false non-entire claim is made.
template<typename T, typename K, Rel R, typename V, typename L, typename C> requires dedekind::algebra::IsOrderedAdditiveGroup<T>
consteval bool	dedekind::order::is_entire (const Comprehension< 𝔸< std::pair< T, T >, L, C >, ProductRestrict< Translation< K >, Cylinder< R, 2, V > > > &)
template<typename T, typename K, Rel R, typename V, typename M, typename W, typename L, typename C> requires dedekind::algebra::IsOrderedAdditiveGroup<T>
consteval bool	dedekind::order::is_entire (const Comprehension< 𝔸< std::pair< T, T >, L, C >, ProductRestrict< Translation< K >, RelAnd< Cylinder< R, 2, V >, Residue< 2, M, W > > > > &)
template<typename T, typename K, typename V, typename M, typename W, IsOckhamAlgebra L, IsCardinality C> requires (dedekind::algebra::IsOrderedAdditiveGroup<T> && dedekind::sets::IsRingIntegral<T>)
constexpr auto	dedekind::order::argmax (const Comprehension< 𝔸< std::pair< T, T >, L, C >, ProductRestrict< Translation< K >, RelAnd< Cylinder< Rel::Le, 2, V >, Residue< 2, M, W > > > > &s)
	argmax over a partial function: the translation x↦x+k into a codomain bounded above (π_2≤P) and restricted to a residue class (π_2≡W mod M), read off structurally. Gated on an ordered additive group of integers: the domain is unbounded below, so the feasible set is never empty and the read-off is the optimum.
template<typename T, typename K, IsOckhamAlgebra LG, IsCardinality C, IsOckhamAlgebra L> requires dedekind::algebra::IsOrderedAdditiveGroup<T>
constexpr Interval< T, L >	dedekind::order::preimage (const Comprehension< 𝔸< std::pair< T, T >, LG, C >, Translation< K > > &g, const Interval< T, L > &h)
	preimage of an interval under \(x\mapsto x+k\): both sides moved by −k, strictness kept. Gated on a translation-invariant order.
template<typename T, typename K, IsOckhamAlgebra LG, IsCardinality CU, IsOckhamAlgebra L>
constexpr Interval< T, L >	dedekind::order::preimage (const Comprehension< 𝔸< std::pair< T, T >, LG, CU >, Scaling< K > > &g, const Interval< T, L > &h)
	preimage of an interval under \(x\mapsto c\cdot x\), c=±1: the interval itself, or reflected (each side to the other, negated, strictness kept). c=−1 needs an order-reversing additive inverse.

Variables
template<typename S, typename A, typename Op>
constexpr bool	dedekind::category::is_closed_under_v = false
	User-declared closure witness: subobject S of A is closed under operation Op.
template<typename R>
constexpr bool	dedekind::algebra::is_initial_ring_v = false
	Opt-in trait: R is the initial object in the category of (commutative, unital) rings.
template<typename G, typename M>
constexpr bool	dedekind::algebra::is_grothendieck_group_v = false
	Opt-in trait: G is the Grothendieck group of the commutative monoid M.
template<typename V, typename F>
constexpr bool	dedekind::algebra::is_vector_space_v = IsVectorSpace<V, F>
	is_vector_space_v<V, F>: V is an F-vector-space. Concept-based dispatch — fires automatically when IsVectorSpace<V, F> holds (which composes IsModule<V, F> + IsField<F>). Companion to is_module_v in :modules. (#498/#499 trait registry.)
template<typename T, typename Add = std::plus<T>, typename Mult = std::multiplies<T>>
constexpr bool	dedekind::algebra::is_galois_field_v = is_galois_field<T, Add, Mult>::value
template<typename T, typename Add = std::plus<T>, typename Mult = std::multiplies<T>>
constexpr std::size_t	dedekind::algebra::galois_order_v = galois_order<T, Add, Mult>::value
constexpr 𝔽64	dedekind::algebra::f64_primitive_α = 𝔽64{static_cast<std::uint8_t>(2)}
template<typename T>
constexpr bool	dedekind::algebra::is_translation_invariant_ordered_v
template<typename T>
constexpr bool	dedekind::algebra::is_scaling_invariant_ordered_v
constexpr auto	dedekind::algebra::embed_𝔹_𝕂3_
	Canonical embedding 𝔹 ↪ 𝕂3: bool → Ternary.
template<typename M, typename R>
constexpr bool	dedekind::algebra::is_module_v = IsModule<M, R>
	is_module_v<M, R>: M is an R-module. Concept-based dispatch — fires automatically when IsModule<M, R> holds.
constexpr auto	dedekind::algebra::𝕂3 = 𝔸<Ternary, Boole, Finite>{}
	The canonical Kleene universe 𝕂3 = 𝔸<Ternary, Boole, Finite> (the three-valued sibling of 𝔹 = 𝔸<bool>).

Files
file	src/main/modules/dedekind/algebra/algebra.cppm
	Groups ⊂ Rings ⊂ Modules ⊂ Polynomials.
file	src/main/modules/dedekind/algebra/boolean.cppm
	Boolean Starter Package: the algebra on the carrier bool and the canonical embedding 𝔹 ↪ 𝕂3.
file	src/main/modules/dedekind/algebra/division.cppm
	The Euclidean Engine (Division Rings and Domains).
file	src/main/modules/dedekind/algebra/field.cppm
	The Rules of Harmony (Groups, Rings, and Fields).
file	src/main/modules/dedekind/algebra/free.cppm
	Free-algebra constructions — the textbook companion to HSP.
file	src/main/modules/dedekind/algebra/galois.cppm
	Galois fields (finite fields).
file	src/main/modules/dedekind/algebra/group.cppm
	The Symmetry of Numbers (ℤ, ℚ*).
file	src/main/modules/dedekind/algebra/halfspace_transport.cppm
	Transport of halfspaces along the additive group: the ordered-group slice of the point-free relational DSL (image / inverse / argmax and the entireness inference).
file	src/main/modules/dedekind/algebra/initial_ring.cppm
	ℤ as a Form — Initial Ring and Grothendieck group of ℕ.
file	src/main/modules/dedekind/algebra/kleene.cppm
	Kleene starter: the three-valued truth surface 𝕂3 as an algebra on a set (the downstream sibling of the Boolean 𝔹).
file	src/main/modules/dedekind/algebra/magma.cppm
	The Magma: base rung of the algebra tower (an algebraic set).
file	src/main/modules/dedekind/algebra/modules.cppm
	The Linear Synthesis (Modules and Vector Spaces).
file	src/main/modules/dedekind/algebra/monoid.cppm
	The Additive and Multiplicative Monoids (ℕ).
file	src/main/modules/dedekind/algebra/ordered_algebra.cppm
	Ordered-algebra markers and concepts: carriers whose order is compatible with their group / ring / field structure (#664, #895).
file	src/main/modules/dedekind/algebra/polynomial.cppm
	The monoid algebra R[M]: polynomials as finitely supported nets over the monomials, and the normal form of a rig's, ring's or field's terms.
file	src/main/modules/dedekind/algebra/quotient.cppm
	HSP structure-preserving operations on algebras — H (quotient, with a relational congruence reading) + P (direct product) + S (subalgebra) carrier-side concepts; their laws and totality are read off the construction in category:total.
file	src/main/modules/dedekind/algebra/ring.cppm
	The Rules of Harmony (The Semiring Synthesis).
file	src/main/modules/dedekind/algebra/tropical.cppm
	The tropical semiring Tropical<T> = T ∪ {∞}, a dioid.
file	src/main/modules/dedekind/algebra/universal.cppm
	The universal-algebra (A, F) meta-pattern: carrier + finitary operations.
file	src/main/modules/dedekind/algebra/vectorspace.cppm
	vector-space concepts + concrete witnesses.