# Does a non-constructive proof of bounds of a computable asymptotic complexity, with impossible fix, exist?

Does there exist an algorithm, about which a non-constructive $$\omega$$-consistent theory $$A$$ can prove that it has time complexity $$O(f(n))$$ where $$n$$ is some univariate function of the input, but there is no $$\omega$$-consistent constructive theory which proves this bound, and there is a constructive $$\omega$$-consistent theory $$B$$, which proves that the algorithm terminates? If it is, is there such a case for a polynomial-time algorithm?

No (assuming $$f$$ is computable). By $$ω$$-consistency, the $$O(f(n))$$ bound is correct, so some $$c f(n)$$ bound is correct, and we can add $$c f(n)$$ bound (which is $$Π^0_1$$) as an axiom to a constructive theory.