Transport of halfspaces along the additive group: the ordered-group slice of the point-free relational DSL (image / inverse / argmax and the entireness inference). More...

#include <concepts>
#include <functional>
#include <limits>
#include <optional>
#include <stdexcept>
#include <type_traits>
#include <utility>
import dedekind.algebra:ordered_algebra;
import dedekind.relational;
import dedekind.order;
import dedekind.sets;
import dedekind.category;

Include dependency graph for halfspace_transport.cppm:

Typedefs
template<Rel R, IsRingIntegral auto I, typename K>
using	dedekind::order::Cylinder = Cmp<R, Projection<I>, Const<K>>
	A cylinder atom `π_I` `⋈` `c`.
template<IsRingIntegral auto I, typename M, typename W>
using	dedekind::order::Residue
	The residue atom `π_I` `%` `m` `==` `w`.

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

Detailed Description

Transport of halfspaces along the additive group: the ordered-group slice of the point-free relational DSL (image / inverse / argmax and the entireness inference).

@partition :halfspace_transport

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

halfspace_transport__Why_Here

The DSL surface (the image / inverse / argmax / is_function / is_entire spellings) lives in namespace dedekind::order so that the point-free calls resolve by ADL on their order/relation argument types. Its implementation, however, lives here in dedekind.algebra, because these operations are ordered-group operations: they slide a \(\le\)-defined halfspace by +K, which is sound exactly when the carrier's order is translation-invariant. That property is the canonical algebra::IsOrderedAdditiveGroup (its marker is_translation_invariant_ordered naming precisely "a non-cyclic ordered additive group"), and algebra sits downstream of order, so this is where the gate is in scope — no order-layer reconstruction. This is the deliberate front-loading: an order-facing DSL whose transport slice is backed by algebra.

halfspace_transport__Functional_vs_Entire

The relation-property split follows the same logic. Functionality (is_right_unique_v, single-valuedness) is structural and stays in order. Entireness (is_left_total_v) is algebraic — a translation \(x\mapsto x+K\) is total iff x+K stays in the carrier, an ordered-group fact — so every is_left_total_v specialisation for the DSL's graph relations lives here. IsFunctional on a graph is therefore an order-level query; IsEntire (and IsFunction) is an algebra-level one.