convergence.cppm File Reference

Sequence/series convergence predicates and standard test hooks. More...

#include <cmath>
#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <vector>
import dedekind.sequences:path;
import dedekind.sets;
import dedekind.order;
import dedekind.category;

Include dependency graph for convergence.cppm:

Classes
struct	dedekind::sequences::carrier_regime< C, typename >
	The regime of a carrier for the limit-collapse: Boole when the carrier declares a countable cardinality_type (ℵ_0 / Finite), Kleene when it is uncountable or declares none (the continuum, or a non-cardinality'd primitive such as double). This is a cardinality question (Specker's theorem is about enumerability), not a species one. More...
struct	dedekind::sequences::carrier_regime< C, std::void_t< typename C::cardinality_type > >
struct	dedekind::sequences::OrbitSequence< T, Op >
	The orbit sequence n ↦ Opⁿ(generator) of a carrier (T, Op), reified as a distinct IsSequence type. More...
struct	dedekind::sequences::SuccessorOrbit< N >
	The orbit of a seed under the NNO step, \(n \mapsto S^{n}(a)\): the unique morphism the universal property gives from ℕ into the carrier ( \(f(0) = a,\; f(n+1) = S(f(n))\)), as a sequence — the unfold iterate(a, Successor<N>{}) named, so the sequence-shape traits can attach to it. Its shape classifies the carrier's posture at the bound: an injective infinite stream on an unbounded chain (the NNO proper), monotone and bounded on a saturating one — eventually constant at ⊤ when the chain is finite (K₃, IsAbsorptiveSequence), converging to ℵ₀ without reaching it on ℕ's proxy — periodic on a wrapping one. More...

Namespaces
namespace	dedekind::sequences::detail
	The interval ↔ iota_view bridge: order's Interval<T,L>, a value, read as the half-open std::ranges::iota_view [start, bound), and back, as a total inverse.

Concepts
concept	dedekind::sequences::IsCauchySequence
	A Seq is a Cauchy sequence: its tail is eventually arbitrarily small under the metric on the carrier.
concept	dedekind::sequences::IsConvergentSequence
	A Cauchy sequence whose limit can be witnessed via limit(s).
concept	dedekind::sequences::IsClassicallyConvergent
	A Cauchy sequence whose carrier sits in the classical logic regime, so the Cauchy ⇒ convergent collapse (limit extraction) fires honestly.
concept	dedekind::sequences::IsOrderConvergent
	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)\).
concept	dedekind::sequences::IsSeries
	A sequence whose Codomain carries the additive structure needed to form partial sums \(S_n = \sum_{k\le n} a_k\).
concept	dedekind::sequences::IsSummable
	A convergent series. Necessary condition (the engineer's obligation to respect): summable ⇒ a_n → 0. The runtime numerical hooks ratio_test_converges, root_test_converges, comparison_test_converges, and converges_series_partial_sums (below) are the operational counterparts that decide summability for concrete float carriers.
concept	dedekind::sequences::IsAbsolutelyConvergent
	An absolutely convergent series. Refines IsSummable: in a complete (Banach) carrier absolute convergence implies convergence, so an IsAbsolutelyConvergent witness is also IsSummable — the same refinement shape as IsConvergentSequence over IsCauchySequence. Carrier completeness is the honesty obligation that makes the implication sound; the witness opts into both traits.
concept	dedekind::sequences::IsBoundedSequence
	A sequence whose image is order-bounded. Bishop §2.
concept	dedekind::sequences::IsMonotoneSequence
	A monotone sequence. Bishop §2; together with IsBoundedSequence drives the monotone-convergence upgrade (LEM-gated, #719 Slice 5).
concept	dedekind::sequences::IsPeriodicSequence
	A period-N sequence. Honest-Rejection foil for the monotone / Cauchy rows (a non-constant periodic sequence is bounded but neither monotone nor Cauchy).
concept	dedekind::sequences::IsAbsorptiveSequence
	An eventually-constant sequence. The simplest convergent case (limit = the absorbing value); period-1-eventually dual to IsPeriodicSequence.
concept	dedekind::sequences::IsSubsequence
	Sub is a subsequence of Sup (same Codomain, strictly increasing index map). Feeds the Bolzano-Weierstrass row (#719 Slice 5: every bounded sequence has a convergent subsequence).
concept	dedekind::sequences::WitnessesBolzanoWeierstrass
	The Bolzano–Weierstrass crown: Sub witnesses that the bounded sequence Sup has a convergent subsequence.

Typedefs
template<typename Seq>
using	dedekind::sequences::convergence_logic
	The logic regime governing Seq's limit-collapse, read off its carrier's declared cardinality (see carrier_regime).
using	dedekind::sequences::Cardinality
	Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.

Enumerations
enum class	dedekind::sequences::Ternary
	A three-valued propositional logic for handling partial information. More...

Functions
constexpr auto	dedekind::sequences::detail::natural_indices (std::size_t count)
template<std::floating_point R>
constexpr R	dedekind::sequences::detail::euclidean_distance (R a, R b)
template<std::floating_point R>
constexpr R	dedekind::sequences::detail::metric_norm (R point, R origin=static_cast< R >(0))
template<std::floating_point R>
constexpr bool	dedekind::sequences::detail::in_closed_euclidean_ball (R center, R point, R radius)
template<typename T> requires requires(T a) { { a + a } -> std::convertible_to<T>; }
constexpr Path< T >	dedekind::sequences::partial_sums (const Path< T > &terms)
	The partial-sum series \(S_n = \sum_{k\le n} a_k\) of a term path, materialised via the co-Kleisli scan.
template<std::floating_point R>
constexpr Path< R >	dedekind::sequences::geometric_series_terms (R ratio)
	Build a geometric-series term path: a_n = r^n.
template<std::floating_point R>
constexpr Path< R >	dedekind::sequences::p_series_terms (R p)
	Build a p-series term path: a_n = 1/(n+1)^p.
template<std::floating_point R>
constexpr bool	dedekind::sequences::converges_sequence_cauchy (const Path< R > &sequence, R epsilon=static_cast< R >(1e-6), std::size_t tail_start=5000, std::size_t tail_span=64)
	Convergence by Cauchy-tail check on sequence values.
template<std::floating_point R>
constexpr bool	dedekind::sequences::converges_series_partial_sums (const Path< R > &terms, R epsilon=static_cast< R >(1e-5), std::size_t warmup=4096, std::size_t tail_span=128)
	Convergence of a series by Cauchy-tail check on partial sums.
template<std::floating_point R>
constexpr bool	dedekind::sequences::ratio_test_converges (const Path< R > &terms, std::size_t tail_start=4000, std::size_t samples=128, R margin=static_cast< R >(1e-3))
	Standard ratio-test hook for non-zero terms.
template<std::floating_point R>
constexpr bool	dedekind::sequences::root_test_converges (const Path< R > &terms, std::size_t tail_start=4000, std::size_t samples=128, R margin=static_cast< R >(1e-3))
	Standard root-test hook on absolute term magnitudes.
template<std::floating_point R>
constexpr bool	dedekind::sequences::comparison_test_converges (const Path< R > &candidate, const Path< R > &upper_bound, std::size_t check_terms=6000, R epsilon=static_cast< R >(1e-5))
	Standard comparison-test hook for non-negative terms.

Variables
template<typename Seq>
constexpr bool	dedekind::sequences::is_order_convergent_v = false
	Opt-in: Seq order-converges — its liminf and limsup coincide. The order-completeness of the carrier (so the inf/sup of the infinite tails exist) and the liminf = limsup equality itself are the engineer's honesty obligation, exactly as metric-completeness is for IsCauchySequence.
template<typename Seq>
constexpr bool	dedekind::sequences::is_summable_v = false
	Opt-in: the series \(\sum a_n\) is summable — its partial-sum sequence converges. The actual convergence (and the carrier completeness it presumes) is the engineer's honesty obligation, as for IsConvergentSequence.
template<typename Seq>
constexpr bool	dedekind::sequences::is_absolutely_convergent_v = false
	Opt-in: the series \(\sum a_n\) is absolutely convergent — the series of norms \(\sum \lVert a_n\rVert\) is summable.
template<typename Seq>
constexpr bool	dedekind::sequences::is_bounded_sequence_v = false
	Opt-in: Seq is order-bounded (image bounded above and below). The bound witnesses are the engineer's obligation.
template<typename Seq>
constexpr bool	dedekind::sequences::is_monotone_sequence_v = false
	Opt-in: Seq is monotone (s(n) ≤ s(n+1) for all n, or the reverse). Direction is the witness's concern.
template<typename Seq, std::size_t N>
constexpr bool	dedekind::sequences::is_periodic_sequence_v = false
	Opt-in: Seq is periodic with period N (s(n) = s(n+N) for all n). Index-side compression: the sequence factors through ℕ/Nℤ. Sequence-axis analog of :total's is_periodic_v<T, Op>.
template<typename Seq>
constexpr bool	dedekind::sequences::is_absorptive_sequence_v = false
	Opt-in: Seq is absorptive (eventually constant — ∃N, z. ∀n≥N. s(n) = z). Codomain-side compression: the tail factors through a singleton {z}. Dual of is_periodic_sequence_v; sequence-axis analog of :species's is_absorptive_v.
template<typename Sub, typename Sup>
constexpr bool	dedekind::sequences::is_subsequence_v = false
	Opt-in: Sub is a subsequence of Sup — there is a strictly increasing index map φ with Sub(n) = Sup(φ(n)). The index map is the engineer's obligation.
template<typename T, typename Op, std::size_t N>
constexpr bool	dedekind::sequences::is_periodic_sequence_v< OrbitSequence< T, Op >, N > = true
	The orbit bridge. If (T, Op) is a periodic carrier with cyclic_order_v<T, Op> = N > 0, then its orbit sequence is a period-N sequence (N is a period; see the section note on minimality). N is deduced from the query and gated against the carrier's cyclic order.
template<HasNNOStep N>
constexpr bool	dedekind::sequences::is_monotone_sequence_v< SuccessorOrbit< N > > = true
	Where the step is a monotone arrow (IsMonotone, registered from the carrier's algebra: it saturates or stops, never wraps), it is inflationary, so the orbit is monotone from any seed; it is bounded where the chain has a top. The K₃ orbit is eventually constant at ⊤ from any seed, within two steps. The ℕ proxy's is not: from a finite seed the index type is exhausted one step before ℵ₀, which is the orbit's supremum and not one of its terms — the sequence converges to the memory boundary without reaching it, so it is monotone and bounded, not absorptive.
template<>
constexpr bool	dedekind::sequences::is_bounded_sequence_v< SuccessorOrbit< Ternary > > = true
template<>
constexpr bool	dedekind::sequences::is_bounded_sequence_v< SuccessorOrbit< Cardinality > > = true
template<>
constexpr bool	dedekind::sequences::is_absorptive_sequence_v< SuccessorOrbit< Ternary > > = true

Detailed Description

Sequence/series convergence predicates and standard test hooks.

@partition :convergence

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"A theorem's elegance is measured by the simplicity of the tests needed to trust it in practice." – Olga Taussky-Todd, paraphrase

See also

#286 undergraduate calculus (work in progress): the ratio, root and comparison tests as criteria proved of a series; here they are finite-sampling hooks.

Typedef Documentation

Cardinality

using dedekind::sets::Cardinality

Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.

The variant (ExtensionalCardinal<>, ℵ_0) is not a cyclic carrier (it does not wrap modulo capacity); on overflow it escalates — saturates — into ℵ_0 via the add / mul helpers below. The explicit overflow story is "you reached countable infinity" rather than the C++ default of silent wrap or UB. The finite fragment is ExtensionalCardinal<>, one std::size_t word (so the variant is not a bignum). The ℵ_0 alternative marks the saturation regime that takes over once the word cannot hold the result.

Strictly mathematically, \(\mathbb{N} \cup \{\aleph_0\}\) is not a monoid in the textbook sense (e.g. left-cancellation fails on the saturating element). The library's pragmatic certificate accepts it as a proxy for \(\mathbb{N}\) because the finite fragment is \(\mathbb{N}\) exactly and the saturation is the explicit overflow contract: "if you compute beyond memory limits, you saturate at @c ℵ_0". Downstream code that requires strict-ℕ behaviour should test the finite-fragment alternative (std::holds_alternative<ExtensionalCardinal<>>). See the sibling SignedCardinality below for the ℤ proxy on the same pattern.

convergence_logic

template<typename Seq>

using dedekind::sequences::convergence_logic

export

Initial value:

 typename carrier_regime<
    std::remove_cvref_t<typename std::remove_cvref_t<Seq>::Codomain>>::type

The logic regime governing Seq's limit-collapse, read off its carrier's declared cardinality (see carrier_regime).

Enumeration Type Documentation

Ternary

enum class dedekind::category::Ternary : std::int8_t

strong

A three-valued propositional logic for handling partial information.

logic__Species_2

Indeterminacy)

Unlike Boole, Kleene's three-valued logic allows for an 'Unknown' state, modeling undecidability or missing knowledge within a predicate. This implementation follows Kleene's strong logic of indeterminacy (K3).

@values

• False (-1): The absolute negative.
• Unknown (0): The indeterminate or undecidable state.
• True (1): The absolute positive.

Function Documentation

converges_series_partial_sums()

template<std::floating_point R>

bool dedekind::sequences::converges_series_partial_sums ( const Path< R > & terms, R epsilon = static_cast<R>(1e-5), std::size_t warmup = 4096, std::size_t tail_span = 128 )

constexprexport

Convergence of a series by Cauchy-tail check on partial sums.

Optimized to cache partial sums once (avoiding O(n^2) recomputation). Computes running sum up to warmup + tail_span - 1, stores tail partial sums in a vector, then validates Cauchy criterion on the tail.

partial_sums()

template<typename T>
requires requires(T a) { { a + a } -> std::convertible_to<T>; }

Path< T > dedekind::sequences::partial_sums ( const Path< T > & terms )

constexprexport

The partial-sum series \(S_n = \sum_{k\le n} a_k\) of a term path, materialised via the co-Kleisli scan.

partial_sums(terms)(n) folds + over the first n+1 terms, seeded from the first term (index 0) and accumulating from index 1 — so no additive identity / default constructor is needed, only the IsSeries additive shape (+). The scan prefix is always non-empty (element i sees the first i+1 terms), so the seed prefix_terms.at(0) is always valid. This is the carrier on which IsSummable / IsAbsolutelyConvergent are judged: the series \(\sum a_n\) converges iff partial_sums does.

Note

Complexity: this is a lazy / intensional series (like scan itself) — each at(n) recomputes the fold, so it is \(O(n)\) per access and \(O(N^2)\) to sample the first N partial sums. For hot-path numerical convergence checks prefer the eager single-pass converges_series_partial_sums below, which caches the running sum.

ratio_test_converges()

template<std::floating_point R>

bool dedekind::sequences::ratio_test_converges ( const Path< R > & terms, std::size_t tail_start = 4000, std::size_t samples = 128, R margin = static_cast<R>(1e-3) )

constexprexport

Standard ratio-test hook for non-zero terms.

Returns true when the sampled tail ratio is strictly below 1.

root_test_converges()

template<std::floating_point R>

bool dedekind::sequences::root_test_converges ( const Path< R > & terms, std::size_t tail_start = 4000, std::size_t samples = 128, R margin = static_cast<R>(1e-3) )

constexprexport

Standard root-test hook on absolute term magnitudes.

Returns true when sampled n-th roots are strictly below 1.