dedekind::sequences::IsClassicallyConvergent Concept Reference

A Cauchy sequence whose carrier sits in the classical logic regime, so the Cauchy ⇒ convergent collapse (limit extraction) fires honestly. More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsClassicallyConvergent = 
    IsCauchySequence<Seq> &&
    std::same_as<convergence_logic<Seq>, dedekind::category::Boole>

Detailed Description

A Cauchy sequence whose carrier sits in the classical logic regime, so the Cauchy ⇒ convergent collapse (limit extraction) fires honestly.

The LEM-flavoured step "every Cauchy sequence converges" is the completeness axiom; constructively it is blocked — Specker exhibits a computable Cauchy sequence of rationals whose limit is not computable. The carrier-axis cardinality cut (#622/#696) decides the regime via convergence_logic: a countable Codomain lands in Boole and the collapse fires; an uncountable carrier (the continuum, or a non-cardinality'd primitive like double — the float↔ℝ gap) lands in Kleene and the collapse is honestly rejected. The existence of the limit is then the classical theorem / the engineer's honesty obligation; this concept gates only the Cauchy shape and the regime, matching the project's concept-names-the-role discipline.

Form-chain row 7 of #719; the convergence half of the logical-collapse crown that WitnessesBolzanoWeierstrass completes.