dedekind::algebra::IsOrderedAdditiveGroup Concept Reference

An additive group whose order is translation-invariant. More...

Concept definition

template<typename T>
concept dedekind::algebra::IsOrderedAdditiveGroup = 
    dedekind::category::IsAbelianGroup<T, std::plus<T>> &&
    is_translation_invariant_ordered_v<T>

Detailed Description

An additive group whose order is translation-invariant.

Combines the algebraic gate (IsAdditiveGroup) with the axiom marker (is_translation_invariant_ordered_v). This is the right precondition for halfspace-pivot transport: shifting \(\{x \mid x > k\}\) by +c yields \(\{y \mid y > k+c\}\) exactly when c-translation preserves the order, which is what the marker certifies.

Note

No separate order check here: the marker carries the order claim (translation invariance is an axiom of the ordered group, not a consequence of the carrier being a chain), and the chain itself is certified where the carrier registers its order laws (the ℤ proxy sets::SignedCardinality is a registered IsTotallyOrdered chain).

Modular carriers (unsigned int as \(\mathbb{Z}/2^N\mathbb{Z}\)) satisfy IsAdditiveGroup but NOT this concept — they fail the marker by default. Honest Rejection on halfspace-pipe attempts with modular carriers.