dedekind::sequences::IsCauchySequence Concept Reference

A Seq is a Cauchy sequence: its tail is eventually arbitrarily small under the metric on the carrier. More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsCauchySequence =  IsSequence<Seq> && requires(Seq s) {
  { s.at(0) } -> std::same_as<typename Seq::Codomain>;
  { s.at(0) - s.at(0) };
}

Detailed Description

A Seq is a Cauchy sequence: its tail is eventually arbitrarily small under the metric on the carrier.

Structurally, the concept pins: (i) Seq satisfies IsSequence, (ii) s.at(0) returns Seq::Codomain, (iii) Codomain supports subtraction (a - a is well-formed), the minimal arithmetic needed to write down |s(m)-s(n)|.

The earlier formulation required std::abs(diff) to be callable, which excluded user-defined carriers that don't overload std::abs. The current body keeps the subtraction shape (permissive: user-defined carriers with operator- participate) and lifts the absolute-value metric reasoning into the engineer's honesty obligation, alongside the full Cauchy criterion (∀ε>0 ∃N ∀m,n≥N. |s(m)−s(n)|<ε).

Anchor: Bishop, Foundations of Constructive Analysis §2.10. Form-chain row 5 of #719.