dedekind.sequences Module Reference

Concepts
concept	dedekind::sequences::IsIndexedMorphismFamily
	A category arrow equipped with explicit index cardinality metadata.
concept	dedekind::sequences::IsCountablyIndexedFamily
	An indexed family whose index magnitude is finite or countably infinite.
concept	dedekind::sequences::IsNet
concept	dedekind::sequences::IsSequence
	The fundamental mapping from a Domain Set to a Value Type.
concept	dedekind::sequences::IsFiniteSequence
	A sequence bound by a Finite Domain.
concept	dedekind::sequences::IsCountableSet
	A Set capable of producing a Path (Enumerability).
concept	dedekind::sequences::IsTerminalSet
	An Enumerable Set with a known Terminal Index.
concept	dedekind::sequences::IsEventuallyPeriodic
	Seq has a finite-state (lasso) presentation: a lasso_presentation specialisation giving a positive period and a pre_period. This is the finite-presentation witness that licenses a decidable, structural-recursive tail-equivalence test (see decide_tail_equivalence).
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.
concept	dedekind::sequences::HasLimit
	Species that can resolve a Path into a single point.
concept	dedekind::sequences::IsStreamComonad
	\emph{Operational} duck-typed check that W carries the Uustalu–Vene stream-comonad shape on an infinite sequence \(\mathbb{N} \to A\). The concept body checks the two primitive legs — ε (head w.at(0)) and δ (tails(w)) — only; the third leg extend (w <<= f) is the derived \(\mathrm{map}\,f \circ \delta\) and is certified separately by the IsCoKleisliTriple witness (pinned beside the IsStreamComonad<Path<int>> assertion below), not re-checked here.
concept	dedekind::sequences::IsCurve
	A real-parameter indexed morphism family.
concept	dedekind::sequences::IsPstSet
	A decidable set object over a finite chain with the covering step: a leaf or a lattice node whose χ answers in \(\mathbb{B}\) (the Δ grade). An L-valued set enters through its α-cuts.

Classes
struct	dedekind::sequences::ComposePrefixPred< PR, PS >
struct	dedekind::sequences::FiniteNet< X, Cap >
	A finite net: a tabulated morphism size_t → X (an IsNet, since std::size_t is a directed set). Read as a function d(v); the std::array tabulation is private business, not the interface. More...
struct	dedekind::sequences::FiniteSeq< T, Cap >
	A finite sequence: an array-backed range of length n ≤ Cap — the compile-time extensional realization of a sequence. More...
class	dedekind::sequences::TailEquivalent< T >
	The tail-equivalence relation on Path<T>: agreement on a sampled tail window [start, start+span). More...
struct	dedekind::sequences::lasso_presentation< Seq >
	Opt-in finite-state ("lasso") presentation of an eventually-periodic sequence: a prefix of length pre_period followed by a cycle of length period (s(n) = s(n+period) for all n ≥ pre_period). The primary carries no presentation; a witness specialises it with the finite (pre_period, period) data — the engineer's honesty obligation (the presentation cannot be computed in general). Absorptive ⇒ period = 1; periodic ⇒ pre_period = 0. More...
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...
class	dedekind::sequences::Path< T, Cardinality, Index >
	A sequence F: ℕ → T. More...
struct	dedekind::sequences::SequenceGraph< PathT >
	as_relation(path) — adapt a Path<T> into its graph relation, a Set of (index, value) pairs. More...
struct	dedekind::category::path_functor< T >
	The path functor for the Path <·> shape (#508 / PR #521 review). More...
struct	dedekind::category::unit_witness< path_functor< T >, T >
struct	dedekind::category::counit_witness< path_functor< T >, T >
class	dedekind::sequences::Curve< Parameter, T, Cardinality >
	A continuum-indexed family γ: I -> T. More...
struct	dedekind::sequences::BoundedSet< OI, P >
	The value-semantic comprehension \(\{x \in \mathrm{dom} \mid P(x)\}\) over a finite domain: an argmax result (or any refinement of a bounded interval), carrying both the interval (the finite range ext scans via to_iota_view) and the refinement predicate P. More...
struct	dedekind::sequences::DominanceRefinement< T, OI, Cost, Order >
	The dominance-refinement predicate of an argmax: x is optimal iff no member x' of the (finite) domain beats it under order∘cost, i.e. \(\forall x' \in \mathrm{dom}.\ \mathrm{order}(\mathrm{cost}(x'), \mathrm{cost}(x))\). A named functor rather than a capturing lambda, so the refinement is an inspectable type carried in the BoundedSet signature argmax returns — the ∀-filter made visible at compile time. More...
struct	dedekind::sequences::IotaIntersection
	std::ranges::iota_view as a Form-chain object: an order::IsOrderMeetSemilattice under subset-inclusion, with intersection as the meet. More...
struct	dedekind::sequences::ScanSteps< S >
	The normal form of s on the window [lo, hi], by exhaustion: a step source that walks the window (and the element after it) along chain_view and steps where χ changes, ⊥ outside the window. Lazy: one walk per traversal, nothing stored. More...

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).
template<typename T>
using	dedekind::sequences::FinitePath = Path<T, Finite>
template<typename T>
using	dedekind::sequences::Sequence = Path<T>
	Textbook name: a Sequence over T is f : ℕ → T = Path<T>.
template<typename T, typename D = std::size_t>
using	dedekind::sequences::Net = Path<T>
	Textbook name: a Net is a function from a directed set into T.

Functions
template<typename A, typename B, typename C, typename L, IsCardinality K1, IsCardinality K2, IsRelPredicate PR, IsRelPredicate PS> requires HasPrefixBound<PR>
constexpr auto	dedekind::sequences::operator>> (const Comprehension< 𝔸< std::pair< A, B >, L, K1 >, PR > &r, const Comprehension< 𝔸< std::pair< B, C >, L, K2 >, PS > &s)
	R >> S over the finite ℕ-prefix middle inferred from R's bound (no middle argument): \((R;S)(a,c) = \exists b \in [0,M).\, R(a,b) \wedge S(b,c)\), streamed as an OR-fold. The result is itself bounded (ComposePrefixPred carries M), so the squaring chain collatzM >> collatzM >> … composes without re-supplying the middle. Generalizes :relational's Boolean-middle >> to a bounded ℕ carrier (#795). Gated on HasPrefixBound so the unbounded >> is non-viable here (it stays the Boolean case in :relational).
template<typename Range, typename Acc, typename Op>
constexpr Acc	dedekind::sequences::fold (const Range &xs, Acc acc, Op op)
	Strict left fold over an enumerable range xs.
template<typename S, typename T> requires (IsSequence<S> && IsSequence<T> && std::same_as<typename S::Codomain, typename T::Codomain>)
constexpr dedekind::category::Ternary	dedekind::sequences::decide_tail_equivalence (const S &s, const T &t)
	Type-directed tail-equivalence decision: honest bool exactly on the finite-presentation domain, Ternary::Unknown otherwise.
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.
template<typename T> requires std::floating_point<T> && IsArchimedean<T>
constexpr T	dedekind::sequences::limit (const Path< T > &s)
	The Archimedean Limit (lim n->∞ s_n).
constexpr Truth< Boole >	dedekind::sequences::limit (const Path< Truth< Boole > > &s)
	The Discrete Limit Morphism for Boolean Truth.
template<typename T>
constexpr const FinitePath< T > &	dedekind::sequences::as_range (const FinitePath< T > &path)
template<typename R> requires std::ranges::input_range<R>
constexpr auto	dedekind::sequences::from_range (R &&range)
template<typename T, typename Cardinality, typename Index>
constexpr auto	dedekind::sequences::prefix (const Path< T, Cardinality, Index > &path, std::size_t length)
template<typename T, typename Cardinality, typename Index> requires (!dedekind::sets::IsFinite<Cardinality>)
constexpr auto	dedekind::sequences::drop (const Path< T, Cardinality, Index > &path, std::size_t n)
template<typename T, typename Cardinality, typename Index> requires std::equality_comparable<T>
constexpr auto	dedekind::sequences::as_relation (const Path< T, Cardinality, Index > &path)
template<typename T, typename Cardinality, typename Index> requires (!dedekind::sets::IsFinite<Cardinality>)
constexpr auto	dedekind::sequences::tails (const Path< T, Cardinality, Index > &s) -> Path< Path< T, Cardinality, Index >, Cardinality, Index >
	δ (duplicate / comultiplication) of the stream comonad — the stream of all suffixes.
template<typename T, typename Step> requires std::invocable<const std::decay_t<Step>&, const T&> && std::same_as< std::invoke_result_t<const std::decay_t<Step>&, const T&>, T>
constexpr auto	dedekind::sequences::iterate (T seed, Step &&step)
template<typename T, typename Step> requires std::invocable<const std::decay_t<Step>&, const T&> && std::same_as< std::invoke_result_t<const std::decay_t<Step>&, const T&>, T>
constexpr auto	dedekind::sequences::iterate (T seed, Step &&step, std::size_t length)
template<typename Op, typename T, typename... Ts> requires (std::convertible_to<Ts, T> && ...) && std::invocable<const Op&, T, Ts...> && std::same_as< std::remove_cvref_t<std::invoke_result_t<const Op&, T, Ts...>>, T>
constexpr Path< T >	dedekind::sequences::iterate (Op op, T seed_0, Ts... more_seeds)
	iterate(op, seed_0, ... , seed_{n-1}) — n-ary recurrence: a binary (or n-ary) operator applied repeatedly to a sliding window of n previous values.
template<typename T, typename Cardinality, typename Index, typename Pred> requires dedekind::sets::IsFinite<Cardinality> && std::predicate<const std::decay_t<Pred>&, const T&>
constexpr std::size_t	dedekind::sequences::count_if (const Path< T, Cardinality, Index > &path, Pred &&pred)
template<typename T, typename Pred> requires std::copy_constructible<std::decay_t<Pred>> && std::predicate<const std::decay_t<Pred>&, const T&>
constexpr std::optional< std::size_t >	dedekind::sequences::first_where (const Path< T > &path, Pred &&pred, std::size_t budget)
template<typename T, typename Pred> requires std::copy_constructible<std::decay_t<Pred>> && std::predicate<const std::decay_t<Pred>&, const T&>
constexpr std::optional< std::size_t >	dedekind::sequences::first_where (const FinitePath< T > &path, Pred &&pred)
template<typename T, typename Cardinality, typename Index, typename Pred> requires std::predicate<const std::decay_t<Pred>&, const T&>
constexpr auto	dedekind::sequences::exists (const Path< T, Cardinality, Index > &path, Pred &&pred)
template<typename T, typename Index, typename F> requires std::copy_constructible<std::decay_t<F>> && std::invocable<const std::decay_t<F>&, const Path<T, Finite, Index>&>
constexpr auto	dedekind::sequences::scan (F &&f, const Path< T, ℵ_0, Index > &path) -> Path< std::invoke_result_t< const std::decay_t< F > &, const Path< T, Finite, Index > & >, ℵ_0, Index >
	Co-Kleisli scan: apply a prefix aggregate to each initial segment.
template<typename T, typename Cardinality, typename Index, typename Pred> requires std::predicate<const std::decay_t<Pred>&, const T&>
constexpr auto	dedekind::sequences::forall (const Path< T, Cardinality, Index > &path, Pred &&pred)
template<std::integral T, typename L>
constexpr std::ranges::iota_view< T, T >	dedekind::sequences::to_iota_view (const dedekind::order::Interval< T, L > &s)
	The typed→runtime half of the iso: project a finite value set (the reduced meet, e.g. structured_and of two intervals) to its canonical std::ranges::iota_view — the same set of integers viewed as a range rather than a predicate.
template<std::integral T, typename L, typename Chi>
auto	dedekind::sequences::ext (const dedekind::order::Interval< T, L > &oi, Chi chi)
	Realise a finite interval domain into its ExtensionalSet, keeping the members that satisfy chi. The interval is the bounded meet that carries the finiteness certificate (cardinality_type = Finite, so IsExtensional); to_iota_view is the only on-ramp from that bounded meet to a scannable range, and the fold is the existing dedekind::sets::ext. An unbounded set has no to_iota_view and cannot reach here — the Rice wall made structural rather than checked. Two-argument form takes the argmax (or any) predicate; the one-argument form realises the whole interval (chi = ⊤).
template<std::integral T, typename L>
auto	dedekind::sequences::ext (const dedekind::order::Interval< T, L > &oi)
	One-argument overload: realise the whole finite interval (every member kept). The chi = ⊤ case of the two-argument ext — it delegates there with the canonical tautology / top predicate dedekind::category::classifier_true.
template<std::integral T, typename L, typename Cost, typename Order = std::less_equal<>>
constexpr auto	dedekind::sequences::argmax (const dedekind::order::Interval< T, L > &dom, Cost cost, Order order={})
	argmax over a bounded (closed-interval) domain: the §3.3 forall- filter {x ∈ dom | ∀x'∈dom. cost(x') ≤ cost(x)}, with ≤ pulled back through cost. Returns a BoundedSet — intensional (the ∀ is decidable because dom is finite) and carrying its domain, so ext realises it. IsSet-valued: ∅ / singleton (unique optimiser, a function) / larger (ties, a proper relation).
template<typename OI, typename P>
auto	dedekind::sequences::ext (const BoundedSet< OI, P > &bs)
	ext a BoundedSet: scan its domain, keep the members its predicate accepts — an ordered ExtensionalSet (the std::set flavour). This is the single-argument call the endorsed ext(argmax(dom, cost)) surface makes.
template<std::size_t N, typename Seq>
constexpr std::array< typename std::remove_cvref_t< Seq >::Codomain, N >	dedekind::sequences::ext (const Seq &s)
	The sequence flavour of ext: realise the first N terms of a sequence (a bra/ket / Path / any index→value arrow) into a std::array — positional and indexed, dual to the set flavour's std::set. The compile-time N is the Kleene bound (the finite prefix); this is the QM realise — an infinite bra/ket, bounded to [0,N), becomes a concrete finite-dimensional vector. Selected by the explicit N (ext<N>(seq)); the no-N form realises a bounded set instead.
template<dedekind::order::Strictness SL, dedekind::order::Strictness SU, typename L = dedekind::category::Boole, std::integral T>
constexpr dedekind::order::Interval< T, L >	dedekind::sequences::from_iota_view (const std::ranges::iota_view< T, T > &iv)
	The runtime→typed half of the iso, a total inverse: rebuild the interval from the iota_view's [start, bound) by undoing the strictness offsets, read as the strictness pair asked for; every iota_view names an interval (an empty view names the empty interval).
template<IsPstSet S>
constexpr auto	dedekind::sequences::runs (const S &s, const typename S::Domain &lo, const typename S::Domain &hi)
	The runs of s on the window, read off its normal form.
template<IsPstSet S> requires IsPst<typename S::Domain>
constexpr auto	dedekind::sequences::runs (const S &s)
	The runs over a whole truth chain, ⊥ to ⊤.

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.
const auto	dedekind::sequences::is_even
	is_even : ℕ → 𝔹 — the parity sequence as a Path<Truth<Boole>> .
template<dedekind::sets::IsRingIntegral T>
const auto	dedekind::sequences::fibonacci_of = iterate(std::plus<T>{}, T(0u), T(1u))
	fibonacci_of<T> : ℕ → T — the canonical Fibonacci sequence 0, 1, 1, 2, 3, 5, 8, 13, ... in any IsRingIntegral carrier T .
const auto &	dedekind::sequences::fibonacci = fibonacci_of<ℕ_Form>
	fibonacci — named default at T = ℕ_Form (ExtensionalCardinal<> ) for paper citation.

Files
file	src/main/modules/dedekind/sequences/sequences.cppm
	Sequences, paths, and (co-)Kleisli triples over directed sets.
file	src/main/modules/dedekind/sequences/convergence.cppm
	Sequence/series convergence predicates and standard test hooks.
file	src/main/modules/dedekind/sequences/curve.cppm
	The Curve (Continuum-Indexed Morphism Family).
file	src/main/modules/dedekind/sequences/finite.cppm
	Compile-time, array-backed realizations of a sequence and a net — the constexpr siblings of the heap-backed Path.
file	src/main/modules/dedekind/sequences/fold.cppm
	The left fold (catamorphism) over an enumerable sequence.
file	src/main/modules/dedekind/sequences/limits.cppm
	The Convergence Morphism (Resolution of the Path).
file	src/main/modules/dedekind/sequences/net.cppm
	The Path (The Morphism of Enumeration).
file	src/main/modules/dedekind/sequences/path.cppm
	The Path (Morphism of Enumeration): a monad and a comonad.
file	src/main/modules/dedekind/sequences/pst.cppm
	The Pst fragment's normal form: a decidable set over a finite chain, folded into its run list as the chain is walked.
file	src/main/modules/dedekind/sequences/ranges.cppm
	The bridge between order's intervals and std::ranges iota views, and the bounded sets built on it.
file	src/main/modules/dedekind/sequences/relprod.cppm
	The relative product \(R;S\) over a FINITE ℕ-prefix middle: the generalization of :relational's Boolean-middle >> (which enumerates {false,true}) to a bounded ℕ carrier \([0,M)\). The \(\exists\)-over-the-middle is a short-circuiting scan (std::ranges::any_of: it stops at the first witness), and the bound M is carried on the composed type so repeated squaring (R;R, (R;R);(R;R), …) stays bounded — the semantic for-loop of bounded transitive closure (#795).
file	src/main/modules/dedekind/sequences/samples.cppm
	Named §3 page-2 sample sequences: is_even and fibonacci.
file	src/main/modules/dedekind/sequences/tail_equivalence.cppm
	Tail-equivalence of paths: the congruence of "agreeing eventually", tying the sequence layer to the #718 quotient machinery.