dedekind::order::IsDiscrete Concept Reference

A set where every point is isolated by a step: the carrier provides the NNO steps (successor / predecessor, HasNNOStep), as the machine integers and the ℕ / ℤ proxies do. The step is the honest discreteness signal; the IsSuccessor leg of IsArchimedean is withheld on every shipped carrier and cannot carry the guard. More...

Concept definition

template<typename T>
concept dedekind::order::IsDiscrete =  IsPartiallyOrdered<T> && dedekind::category::HasNNOStep<T>

Detailed Description

A set where every point is isolated by a step: the carrier provides the NNO steps (successor / predecessor, HasNNOStep), as the machine integers and the ℕ / ℤ proxies do. The step is the honest discreteness signal; the IsSuccessor leg of IsArchimedean is withheld on every shipped carrier and cannot carry the guard.

Intentionally \emph{not} exported: IsDiscrete is a private helper used only inside IsDense below (the negation !IsDiscrete<T> rules out the step-isolated case). The concept has the same scope now as before the :concepts → :poset/:lattice/:completeness split; if a downstream call site for "is this carrier discrete?" appears, promote this declaration to export at that point rather than pre-emptively widening the API.