dedekind::sequences::IsOrderConvergent Concept Reference

A sequence that converges in the order sense: \(\liminf_n s(n) = \limsup_n s(n)\), with \(\liminf = \bigsqcup_n \bigsqcap_{k\ge n} s(k)\) and \(\limsup = \bigsqcap_n \bigsqcup_{k\ge n} s(k)\). More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsOrderConvergent = 
    IsSequence<Seq> &&
    dedekind::order::IsOrderMeetSemilattice<typename Seq::Codomain> &&
    dedekind::order::IsOrderJoinSemilattice<typename Seq::Codomain> &&
    is_order_convergent_v<Seq>

Detailed Description

A sequence that converges in the order sense: \(\liminf_n s(n) = \limsup_n s(n)\), with \(\liminf = \bigsqcup_n \bigsqcap_{k\ge n} s(k)\) and \(\limsup = \bigsqcap_n \bigsqcup_{k\ge n} s(k)\).

The carrier must be an order lattice — both an order::IsOrderMeetSemilattice (for the ⊓ / inf of tails) and an order::IsOrderJoinSemilattice (for the ⊔ / sup) — so that liminf and limsup are even definable. This is the load-bearing :order::lattice cross-reference: a carrier with no meet/join cannot host order-convergence and is honestly rejected regardless of any trait opt-in. Order-completeness (the inf/sup of the infinite tails actually existing) and the liminf = limsup equality are the engineer's honesty obligation, mirroring how metric-completeness is the obligation for IsCauchySequence.

Order vs metric convergence

Order-convergence is the lattice-theoretic, metric-free notion and is constructive (no LEM): in a Dedekind-complete carrier a bounded monotone sequence order-converges to the sup/inf of its image — the order-theoretic monotone convergence theorem, which needs no choice principle. This contrasts with the metric IsConvergentSequence, whose limit(s) extraction from a Cauchy sequence is the LEM-flavoured collapse gated in #719 Slice 5.

The monotone-convergence propagation itself (is_bounded_sequence_v ∧ is_monotone_sequence_v over a order::IsDedekindComplete carrier ⇒ order-convergent) is a named follow-up rather than a baked-in concept disjunction: the IsDedekindComplete carrier QuadraticReal<D> lives downstream of :sequences, so the propagation is best witnessed in a downstream test alongside that carrier (cf. the orbit bridge, whose propagation is witnessed downstream in :morphologies).

Anchor: Birkhoff, Lattice Theory §X.9 (order convergence). Form-chain row 6b of #719.