dedekind.order Module Reference

Concepts
concept	dedekind::order::SubReifiable
	A base that reifies as an ordered-carrier subobject Sub(C): it is SetShaped, its carrier is totally ordered (the enabler — so the gate itself, not a later membership call, rejects an unordered carrier), and it coerces to Sub via one of the converting constructors above. The single gate concept for both power_set and 𝔓 (DRY), and — because it conjoins the very SetShaped atom the :sets default is constrained on — it subsumes that deleted gate, so it wins by partial ordering for the ordered families.
concept	dedekind::order::IsStrictWeakOrder
	The standard C++ 'Compare' requirement (e.g., for std::sort).
concept	dedekind::order::IsTotallyOrdered
	A refinement where every pair is comparable (The Chain).
concept	dedekind::order::IsLinearOrder
	Synonym for Total Order.
concept	dedekind::order::HasTotalOrderOperators
	Pure syntactic shape: T supports the spaceship operator <=> alongside the four partial-order operators (the latter return L::Ω).
concept	dedekind::order::HasTotalOrderOperatorsWith
	Heterogeneous shape: T and U can be compared via <=> in both directions, alongside the four partial-order operators (the latter return L::Ω).
concept	dedekind::order::HasLatticeOperators
	Pure syntactic shape: T supports the bitwise / lattice operators &, |, ^, ~ with results convertible to T.
concept	dedekind::order::IsOrderMeetSemilattice
	Re-export the certified meet-semilattice stage from :posetal.
concept	dedekind::order::IsOrderJoinSemilattice
	Re-export the certified join-semilattice stage from :posetal.
concept	dedekind::order::IsOrderLattice
	Bundled lattice witness: the strict commutative-ring proof under (std::bit_xor<T>, std::bit_and<T>) AND the bitwise/lattice operator surface on T, by definition.
concept	dedekind::order::IsOrderDistributiveLattice
	Re-export the certified distributive lattice stage from :posetal.
concept	dedekind::order::IsPreOrdered
	The most basic relation: Reflexive and Transitive.
concept	dedekind::order::IsDirectedSet
	A Pre-ordered structure where any two elements have a common successor.
concept	dedekind::order::IsPartiallyOrdered
	A refinement of the Pre-Order that satisfies Antisymmetry (Identity).
concept	dedekind::order::IsDirectedPoset
	The "Convergent Identity": A Poset that is also a Directed Set.
concept	dedekind::order::HasPartialOrderOperators
	Pure syntactic shape: T supports the partial-order operators <, <=, >, >= with results in the truth-value carrier L::Ω of a chosen logical species.
concept	dedekind::order::HasPartialOrderOperatorsWith
	Heterogeneous shape: T and U can be compared via the four partial-order operators in both directions, yielding results in the truth-value carrier L::Ω.
concept	dedekind::order::IsSuccessor
	The algebraic S: T -> T mapping via the Unit element.
concept	dedekind::order::IsArchimedean
	The scale axiom: Every element can be 'reached' by the Successor. FIXME: misnamed. "Every element reached by the successor" is Peano's and Dedekind's generation of the naturals from one element and a step; the Archimedean property is another axiom, that for x, y > 0 some n has n x > y [1]. Rename to the property it states, and reconcile its algebraic IsSuccessor (x + 1) with the NNO step of dedekind.category (successor, HasNNOStep), which every shipped carrier provides and IsSuccessor's carriers withhold.
concept	dedekind::order::IsDense
	A property where a midpoint always exists (a < c < b).
concept	dedekind::order::IsDividableChain
	A Totally Ordered species with a partitioning algorithm (/).
concept	dedekind::order::IsDedekindComplete
	The topological "Soul" of the Continuum (LUB property).
concept	dedekind::order::IsStepTerm
	A set term whose normal form the run lists read.
concept	dedekind::order::IsStepSource
	A step source: the carrier and species, the value before every step, and the steps as a forward range, in order along the chain.
concept	dedekind::order::SubobjectLatticePair
	A compatible pair of subobject lattices — same ambient Domain and logic_species: the canonical rung on which subset is defined. Ties the order to category::IsSubobjectLattice rather than a bespoke shape; the same-logic clause is the cross-logic-mereology guard (#833 review).
concept	dedekind::order::DecidableMeetSubset
	\(A \subseteq B\) is decidable via the structural meet: a subobject-lattice pair whose meet-then-equality is a truth value. The gate for the generic identity <=; where the meet does not collapse this is unsatisfied (the honest exists / forall wall) and a per-carrier <= must supply the case.
concept	dedekind::order::HasSubset
	A decidable <= exists for the pair — generic (meet) or a per-carrier specialisation (Singleton membership, Interval endpoints). The gate for the derived relations, so they ride any <=, not only the meet-based one.
concept	dedekind::order::HasProperSubset
	HasSubset plus a bool ==, so \(A \subsetneq B \equiv A \subseteq B \wedge A \neq B\) is expressible.

Classes
struct	dedekind::order::Sub< C, L >
	Sub(C) for an ordered carrier: a subobject reified as a runtime interval value. Bounds are C values with ±∞ (unbounded) flags and an empty flag; the convex families coerce in via the converting constructors below (which also are the 𝔓 gate — no constructor ⇒ no Sub(C)). Folds onto SetExpr (so it is itself a first-class IsSubobject / IsSet) and is std::regular, so Set<Sub,…> is an IsSet and Sub values are usable in generic set APIs. More...
struct	dedekind::order::SubsetOf< C, L >
	The membership predicate of 𝔓(S): \(X \mapsto X \subseteq S\), with S coerced to Sub(C). A named functor (no lambda). More...
struct	dedekind::order::bit_subset_eq< T >
	Integral carriers under the bitwise Boolean algebra (#710). More...
struct	dedekind::order::Interval< V, L >
	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	dedekind::order::ProductRestrict< P, RP >
	The product's own membership conjoined with a relational restriction, so a bind over a restricted product keeps that membership and cannot admit pairs outside it (a full product contributes a trivially-true product). More...
struct	dedekind::order::InSlot< I, S >
	\(\pi_I^{-1}(S)\): the cylinder of a set S on axis I of a pair, a relational predicate. More...
struct	dedekind::order::Bound< V >
	One side of an interval as a value: the bound and whether it is attained (non-strict) or not (strict). More...
struct	dedekind::order::Span< V >
	The sides of an inhabited convex set; an absent side is unbounded. More...
struct	dedekind::order::Position< V >
	A position on the chain: just below at, or just above it. More...
struct	dedekind::order::Step< V, L >
	Where the value changes, and to what. A source holds its steps by value (an interval's two sides, an iterator's current step), so the carrier and the truth values are default-initialisable. More...
struct	dedekind::order::SpanSteps< V, L >
	An interval's sides as a source, valued value on it and ⊥ elsewhere: at most two steps. No sides is the whole carrier, no span the empty set, so the constants are spans too. More...
struct	dedekind::order::RunListSteps< N, K >
	Pst's run list (category:runs) as a step source: each of its steps the position just below it, the value from there on alternating from outside. Where both apply, on a finite chain with Boolean values, the order's run lists read it as any source, so ext, the merges and the cuts take it; the vocabulary they share is to move into category (#1138). More...
struct	dedekind::order::SourceRef< S >
	A source read through a reference: a stored run list inside a term is traversed where it is, not copied. More...
struct	dedekind::order::RelabelSteps< A, F, L2 >
	A source with every value relabelled into the species L2: a complement, a lift into a wider species, an α-cut. More...
struct	dedekind::order::MergeSteps< A, B, F >
	Two sources merged along the chain under a pointwise operation: the steps of both, each read as f of the two values there. More...
struct	dedekind::order::IdentitySteps< C >
	χ(x) = x on a finite chain, valued in the chain's own species: a step at every element above the least (none on a one-element chain). More...
struct	dedekind::order::Piece< V >
	A piece on which a two-valued source holds: a start (nullopt below every element) and an end (nullopt above). More...
struct	dedekind::order::Run< C >
	A maximal run of membership as its closed ends, [lo, hi]. More...
struct	dedekind::order::Runs< V, L >
	A set of the chain V valued in L, materialised: its breakpoints, each the value from that position on, and the value before them. The one stored form, for a value that must outlive the term it was read from (a Python handle); a source like any other, its steps a view of the map. More...

Enumerations
enum class	dedekind::order::Direction { Upward , Downward }
	Orientation of a halfspace along the chain.
enum class	dedekind::order::Strictness { Strict , NonStrict }
	Whether the boundary is strict (>, <) or inclusive (>=, <=).
enum class	dedekind::order::Side : bool { Below , Above }
	Which side of its value a position sits on. More...

Typedefs
template<typename K>
using	dedekind::order::Translation
	The translation graph π_1 + k == π_2 and the scaling graph π_1 * k == π_2, as the atoms the grammar builds for them.
template<typename K>
using	dedekind::order::Scaling

Functions
template<SubReifiable S>
constexpr auto	dedekind::order::power_set (const S &base)
	\(\mathfrak{P}(S) = \mathbb{A}\langle\mathrm{Sub}(C)\rangle \mid (X \mapsto X \subseteq S)\) — a bona-fide Set over Sub(C). Gated on S coercing to Sub(C): an unordered / general base is ill-formed.
template<typename C, typename L, typename Card> requires IsTotallyOrdered<C>
constexpr auto	dedekind::order::power_set (const dedekind::sets::𝔸< C, L, Card > &)
	\(\mathfrak{P}(\mathbb{A}) = \mathbb{A}\langle\mathrm{Sub}(C)\rangle\) — the universe of ALL (decidable convex) subobjects, as the universal boundary type, not a trivially-true filtered Set. A more-specialised overload than the generic power_set above, so it wins by partial ordering; keeping the 𝔸 type (rather than Set<Sub,…,SubsetOf>) preserves the boundary / cardinality metadata and the lattice identities 𝔸|X=𝔸 / 𝔸&X=X on 𝔓(𝔸). (Sibling of the :sets closed form \(\mathfrak{P}(\emptyset)=\{\emptyset\}=\mathbb{A}\langle\varnothing\rangle\).)
template<SubReifiable S>
constexpr auto	dedekind::order::𝔓 (const S &base)
	Textbook fraktur-P alias for power_set (blackboard 𝔓). Forwards to power_set, so the 𝔸 closed form above is selected for a universe base and the filtered form for a proper ordered base.
template<typename T, typename Step> requires std::is_integral_v<T>
constexpr T	dedekind::order::bit_closure (T seed, Step step)
	Reachability / the universal-algebra "generated by", over the power-set lattice: the reflexive-transitive closure of a bitmask seed under a one-step adjacency step — the least bitmask ⊒ seed (in bit_subset_eq) that is closed under step, i.e. ⨆ₙ stepⁿ(seed) with join the lattice's own bit_or. It is the Boolean instance of the generic closure (category:functor) over this lattice; decidable because the finite bit-carrier stabilises. Reusing it: reachability of a graph whose nodes are bit positions and step is the adjacency.
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::less<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::less_equal<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::greater<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::greater_equal<>, bool)
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, EuclideanDivision, bool divisor_is_constant)
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, std::modulus<>, bool divisor_is_constant)
constexpr Direction	dedekind::order::dir_of (Rel r)
	The Direction a comparison Rel lifts a halfspace to.
constexpr Strictness	dedekind::order::strict_of (Rel r)
	The Strictness a comparison Rel lifts a halfspace to.
constexpr bool	dedekind::order::is_order_rel (Rel r)
	Whether a Rel is one of the four order comparisons (not Eq/Ne).
template<dedekind::order::IsTotallyOrdered T, dedekind::category::IsOckhamAlgebra L, IsCardinality C, Rel R, typename K> requires (dedekind::order::is_order_rel(R))
constexpr dedekind::order::Interval< T, L >	dedekind::sets::operator& (const 𝔸< T, L, C > &, const Cmp< R, Projection< 0 >, Const< K > > &c)
	An order atom π ⋈ k on a chain is the ray it names, whatever the constant's type: the constant meets the carrier exactly or the binding raises. Declared beside 𝔸 and the atom, so ADL finds it.
template<typename V, typename L>
constexpr Interval< V, L >	dedekind::order::reduce_meet (const Interval< V, L > &a, const Interval< V, L > &b)
	The ONE meet law: the tighter side on each end, collapsed by bounded (crossing sides to Ø, a single admitted element to its point). constexpr, so evaluable at compile time or runtime.
template<typename T> requires requires { typename T::logic_species; }
constexpr auto	dedekind::order::steps (const T &t)
	The normal form of a set term of a chain, as a lazy step source. A stored run list inside the term is read in place, so the source must not outlive the term.
template<IsStepTerm T>
auto	dedekind::order::ext (const T &t)
	The extension of a set term: its normal form, materialised as a stored run list. The explicit step; every query reads steps(t) lazily without it.
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::operator== (const A &a, const B &b)
	Equality of two set terms of a chain as sets of the carrier, in the species: one traversal of their normal forms, so it is extensional ((0, 3) and [1, 3) are the same set of ℤ).
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && (!std::same_as<typename A::logic_species, typename B::logic_species>) && HaveLogicJoin<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::operator== (const A &a, const B &b)
	Equality across two species of one chain, read in their join: a Boolean set beside a K₃-valued one is compared in K₃.
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const Ø< T, L > &, const S &s)
	A set term against the boundaries, in its species: Ø == S is \(\neg\bigvee\chi\), 𝔸 == S is \(\bigwedge\chi\), read over the carrier's own elements (on K₃, Unknown is a verdict).
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const S &s, const Ø< T, L > &e)
template<IsTotallyOrdered T, IsOckhamAlgebra L, IsCardinality CU, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const 𝔸< T, L, CU > &, const S &s)
template<IsTotallyOrdered T, IsOckhamAlgebra L, IsCardinality CU, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const S &s, const 𝔸< T, L, CU > &u)
template<IsTotallyOrdered V, IsOckhamAlgebra L>
constexpr Interval< V, L >	dedekind::order::structured_and (const Interval< V, L > &a, const Interval< V, L > &b)
	The meet of two intervals, under the reducer's customization-point name: the one reduce_meet. Declared here, before axis_factor, so the recursion over a RelAnd tree is closed over its own outputs (#872).
template<IsStepSource S> requires std::same_as<typename S::logic_species, Boole>
constexpr auto	dedekind::order::intervals (const S &s)
	The runs of a two-valued source as intervals, in order along the chain: a view, nothing stored.
template<typename T1, typename T2, typename L, typename C, IsRelPredicate RP> requires (!dedekind::sets::contains_self_v<RP>)
constexpr auto	dedekind::order::operator& (const 𝔸< std::pair< T1, T2 >, L, C > &, RP rp)
	𝔸 & relPred — the relation as a set object on A×B. The universal product carries no factor restriction, so the relation's membership is the rel-predicate: the pure product universe refined to a subobject.
template<typename S, IsRelPredicate RP> requires dedekind::sets::IsSetObject<S> && requires { typename S::Domain::first_type; typename S::Domain::second_type; } && (!dedekind::sets::contains_self_v<RP>)
constexpr auto	dedekind::order::operator& (const S &prod, RP rp)
	product & relPred — the relation as a set object on A×B, keeping the product's own membership (so a restricted product bounds the relation).
constexpr Rel	dedekind::order::rel_of (Direction d, Strictness s)
	A restricted factor lifts to a cylinder on its axis, so operator* keeps the factor predicates instead of dropping them.
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename T2, IsCardinality C2>
constexpr auto	dedekind::order::operator* (const Interval< T, L > &a, const 𝔸< T2, L, C2 > &)
template<typename T1, IsCardinality C1, IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr auto	dedekind::order::operator* (const 𝔸< T1, L, C1 > &, const Interval< T, L > &b)
template<IsTotallyOrdered Ta, IsTotallyOrdered Tb, IsOckhamAlgebra L>
constexpr auto	dedekind::order::operator* (const Interval< Ta, L > &a, const Interval< Tb, L > &b)
template<IsRingIntegral auto I, typename TI, typename L, typename P>
constexpr auto	dedekind::order::axis_factor (const P &)
	dom / cod as the projections \(\pi_A / \pi_B\), recovering the factor from the relation's structure (the inverse of cylinder).
template<IsRingIntegral auto I, IsTotallyOrdered TI, IsOckhamAlgebra L, IsRingIntegral auto Slot, Rel R, typename K> requires (is_order_rel(R) && Slot == I)
constexpr auto	dedekind::order::axis_factor (const Cmp< R, Projection< Slot >, Const< K > > &c)
	An order atom on axis I, π_I ⋈ c: the ray it names (Eq/Ne fall to the default). The slot is matched to the axis by value, so two integral spellings of one axis agree.
template<IsRingIntegral auto I, IsTotallyOrdered TI, IsOckhamAlgebra L, IsRingIntegral auto Slot, typename S> requires (Slot == I)
constexpr S	dedekind::order::axis_factor (const InSlot< Slot, S > &c)
	A cylinder on axis I: its set.
template<IsRingIntegral auto I, typename TI, typename L, typename A, typename B>
constexpr auto	dedekind::order::axis_factor (const dedekind::relational::RelAnd< A, B > &r)
template<IsRingIntegral auto I, typename TI, typename L, typename Pp, typename RP>
constexpr auto	dedekind::order::axis_factor (const ProductRestrict< Pp, RP > &r)
	A restricted product bounding a graph: the factor lives on the product (cylinder) side; the graph rp couples the axes, so it is transparent to a single-axis projection.
template<typename T1, typename T2, typename L, IsRelPredicate P, typename C>
constexpr auto	dedekind::order::dom (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	\(\pi_A(R)\) — the domain factor, recovered structurally (preserving the relation's logic species L).
template<typename T1, typename T2, typename L, IsRelPredicate P, typename C>
constexpr auto	dedekind::order::cod (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	\(\pi_B(R)\) — the codomain factor, recovered structurally.
template<IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr Interval< T, L >	dedekind::order::upperbounds (const Interval< T, L > &s)
	upperbounds(S) — the \(\forall\)-projection \(R/\ni\): the region dominating all of S, and the pluggable point of the extremum (Bird & de~Moor [2]).
template<IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr Interval< T, L >	dedekind::order::lowerbounds (const Interval< T, L > &s)
	The dual: lower bounds, {x ≤ inf}.
template<IsOckhamAlgebra L, IsCardinality C>
constexpr auto	dedekind::order::upperbounds (const 𝔸< bool, L, C > &)
template<IsOckhamAlgebra L, IsCardinality C>
constexpr auto	dedekind::order::lowerbounds (const 𝔸< bool, L, C > &)
template<typename S> requires IsPartiallyOrdered<typename S::Domain> && requires(const S& s) { s & upperbounds(s); }
constexpr auto	dedekind::order::max (const S &s)
	max(S) — the generic extremum: S met (∩) with its own \(\forall\)-dominators, \(S \cap \mathrm{upperbounds}(S)\). min is the dual (S met with its minorants).
template<typename S> requires IsPartiallyOrdered<typename S::Domain> && requires(const S& s) { s & lowerbounds(s); }
constexpr auto	dedekind::order::min (const S &s)
template<typename T, typename K1, typename K2, typename L, typename C, typename CU> requires dedekind::category::IsSaturating<T>
constexpr bool	dedekind::order::operator== (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K1 > > &a, const Comprehension< 𝔸< std::pair< T, T >, L, CU >, Translation< K2 > > &b)
	Two translation graphs are the same relation iff they carry the same shift, read in the carrier. Gated on IsSaturating: the shift arithmetic is faithful only where the carrier's + is (on bool, +1 and +2 are the same graph, so a comparison of shifts would separate them).
template<typename T, typename K1, typename K2, typename L, typename C, typename CU> requires dedekind::category::IsSaturating<T>
constexpr auto	dedekind::order::operator>> (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K1 > > &a, const Comprehension< 𝔸< std::pair< T, T >, L, CU >, Translation< K2 > > &b)
	Symbolic composition of translation graphs, \(T_a \circ T_b = T_{a+b}\): the shifts added in the carrier, with no \(\exists\) over the intermediate. Gated on IsSaturating, where the symbolic a+b is the actual composite.
constexpr Direction	dedekind::order::flip (Direction d)
	Flip a Direction — the direction half of a halfspace complement (~{x>P} is {x≤P}). Reused by the reflection-image pushforward (dedekind.algebra:halfspace_transport) to flip a halfspace's sense under \(x \mapsto -x\).
constexpr Strictness	dedekind::order::flip (Strictness s)
	Flip a Strictness — the strictness half of the same complement (~{x>P} is {x≤P}: > relaxes to ≤).
template<typename V>
constexpr Position< V >	dedekind::order::canonical (const Position< V > &p)
	A position in its canonical form: closed where the chain has the step.
template<std::ranges::view R, typename Ω>
constexpr auto	dedekind::order::distinct_steps (R r, Ω first)
	Steps with no step repeating the value before it, as a view: runs of one value kept by their first step, and a first step at the start value dropped. A view, taken by value as Rule 1 asks; a container or an array is passed as std::views::all of it.
template<dedekind::category::IsCountWord N, std::size_t K>
constexpr RunListSteps< N, K >	dedekind::order::steps (const dedekind::category::RunList< N, K > &r)
template<IsStepSource S>
constexpr auto	dedekind::order::alpha_cut (const S &s, typename S::logic_species::Ω level)
	The decidable sets of an L-valued source: the α-cut \(\{\chi \ge \ell\}\) and the fibre \(\chi^{-1}(\ell)\).
template<IsStepSource S>
constexpr auto	dedekind::order::fibre (const S &s, typename S::logic_species::Ω level)
template<IsStepSource S> requires std::same_as<typename S::logic_species, Boole>
constexpr auto	dedekind::order::pieces (const S &s)
	The pieces of a two-valued source, as a forward view.
template<IsStepSource S> requires IsFiniteChain<typename S::Domain> && HasNNOStep<typename S::Domain> && (detail_position::least<typename S::Domain>().has_value())
constexpr auto	dedekind::order::runs (const S &s)
	The runs of a two-valued source of a finite chain, as a view of closed pairs: every run that ends does so just below an element with a lower cover (ℕ's proxy, whose ℵ₀ has none, is read through positions).
template<std::unsigned_integral V, typename L> requires IsAbelianGroup<V, std::plus<V>>
Runs< V, L >	dedekind::order::translate (const Runs< V, L > &s, V k)
	The translate of a run list by k on a machine word, the chain read as the cyclic group ℤ/2^w it is: \(x \mapsto x + k\) wraps at the word's end, so a run through the end splits in two. It is the image of the set under the translation, and the preimage under the inverse one. The other reading of the same word, as the chain, is Pst's category::preimage(shift(d), s) on a RunList: the translation as a map of the chain, on its extent, where the word does not wrap; the two agree exactly where nothing lies below d, and differ by the segment at the word's top otherwise (witnessed in runs_test). Two arrows on one word; the chain's is the derivative's (:automaton), the group's is this.
template<typename K> requires requires(const K& a, const K& b) { std::weak_order(a, b); }
std::weak_ordering	dedekind::order::constant_order (const K &a, const K &b)
	The order of two constants of the grammar: their own weak (or strong) three-way comparison where they have one; a constant type with none, or only a partial one, names a total order beside it (found by argument-dependent lookup, as carrier_cast).
template<typename K>
std::weak_ordering	dedekind::order::structural_order (const Pred< K > &a, const Pred< K > &b)
	The structural order of two predicates (#884): by kind first, so the comparisons (decided, Δ) precede the connectives and the quantifiers (∃ Σ, then ∀ Π); a comparison by its left term, its relation, its right term; a connective by its operands; a quantifier by its sort, slot and body. The key canonical sorts a conjunction / disjunction by.
template<typename K>
std::weak_ordering	dedekind::order::structural_order (const Term< K > &a, const Term< K > &b)
	The structural order of two terms (#884): by kind (a projection, a constant, an operation, a conditional), then a projection by its slot, a constant by constant_order, an operation by its operator and operands, a conditional by its guard and branches. Total; two terms are equivalent in it exactly when they are the same tree.
template<typename K>
Pred< K >	dedekind::order::connective (typename Pred< K >::Kind k, std::vector< Pred< K > > ops)
	The connective k (And or Or) of the operands, with the order, grouping and repetition forgotten (#884): the bounds folded (the unit dropped, an absorber absorbing), the operands sorted by structural_order, each kept once, folded left. None left: the unit.
template<typename A, typename B> requires DecidableMeetSubset<A, B>
constexpr A::logic_species::Ω	dedekind::order::operator<= (const A &a, const B &b)
	\(A \subseteq B \iff A \cap B = A\) — the generic identity. More-specialized per-carrier <= (Set / Ø / 𝔸, the Singleton membership and Interval endpoints below) win by partial ordering; this fills the gaps (Halfspace ⊆ Halfspace).
template<typename A, typename B> requires HasSubset<B, A>
constexpr A::logic_species::Ω	dedekind::order::operator>= (const A &a, const B &b)
	Superset, proper subset, proper superset — each once from <= and ==, gated on HasSubset so they ride any decidable <= (generic or specialised). Together they supply HasPartialOrderOperators.
template<typename A, typename B> requires HasProperSubset<A, B>
constexpr A::logic_species::Ω	dedekind::order::operator< (const A &a, const B &b)
template<typename A, typename B> requires HasProperSubset<B, A>
constexpr A::logic_species::Ω	dedekind::order::operator> (const A &a, const B &b)
template<typename T, typename L>
constexpr L::Ω	dedekind::order::operator<= (const Interval< T, L > &a, const Interval< T, L > &b)
	\(A \subseteq B\) on intervals: \(A \cap B = A\), extensional since interval equality closes strict bounds on a discrete carrier.

Queries: one traversal of a source
template<IsStepSource S>
constexpr auto	dedekind::order::value_at (const S &s, const typename S::Domain &x)
template<IsStepSource S>
constexpr auto	dedekind::order::forall (const S &s)
	\(\bigwedge_x \chi(x)\) and \(\bigvee_x \chi(x)\) in the species over the carrier's own elements: on Ø both are ⊥, on 𝔸 both ⊤.
template<IsStepSource S>
constexpr auto	dedekind::order::exists (const S &s)
template<IsStepSource A, IsStepSource B> requires std::same_as<typename A::Domain, typename B::Domain> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::equal (const A &a, const B &b)
	Equality of two sources as sets of the carrier, in the species: \(\bigwedge_x (\chi_a(x) \Leftrightarrow \chi_b(x))\), so over K₃ two sets agree to degree U where either is U.

Files
file	src/main/modules/dedekind/order/order.cppm
	Order relations and compile-time halfspace predicates.
file	src/main/modules/dedekind/order/completeness.cppm
	Density and completeness profiles of orders.
file	src/main/modules/dedekind/order/halfspace.cppm
	Compile-time halfspace predicates on ordered carriers.
file	src/main/modules/dedekind/order/inclusion.cppm
	The inclusion (subset) order on subobject lattices, derived from the structural meet and equality (#831).
file	src/main/modules/dedekind/order/lattice.cppm
	Order-theoretic meet / join / lattice structures.
file	src/main/modules/dedekind/order/poset.cppm
	Preorders, partial orders, directed sets, chains.
file	src/main/modules/dedekind/order/powerset.cppm
	The power set \(\mathfrak{P}(S)\) as a filtered universe over a reified subobject domain Sub(C) (#830).
file	src/main/modules/dedekind/order/runs.cppm
	Run lists: the normal form of the sets of a chain built from intervals, valued in a species.
file	src/main/modules/dedekind/order/total.cppm
	Total-order layer (stronger than :poset).