Tail-equivalence of paths: the congruence of "agreeing eventually", tying the sequence layer to the #718 quotient machinery. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <numeric>
#include <type_traits>
import dedekind.sequences:path;
import dedekind.category;

Include dependency graph for tail_equivalence.cppm:

Classes
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...

Namespaces
namespace	dedekind::category

Concepts
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`).

Functions
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.

Variables
template<typename T>
constexpr bool	dedekind::category::is_reflexive_v< dedekind::sequences::Path< T >, dedekind::sequences::TailEquivalent< T > >
template<typename T>
constexpr bool	dedekind::category::is_symmetric_v< dedekind::sequences::Path< T >, dedekind::sequences::TailEquivalent< T > >
template<typename T>
constexpr bool	dedekind::category::is_transitive_v< dedekind::sequences::Path< T >, dedekind::sequences::TailEquivalent< T > >
template<typename T>
constexpr bool	dedekind::category::is_congruence_v< dedekind::sequences::TailEquivalent< T >, dedekind::sequences::Path< T >, std::plus< dedekind::sequences::Path< T > > >

Detailed Description

Tail-equivalence of paths: the congruence of "agreeing eventually", tying the sequence layer to the #718 quotient machinery.

@partition :tail

tail__The_Germ_At_Infinity

Two sequences are tail-equivalent when they agree from some index on:

\[ s \sim_{\mathrm{tail}} t \;\;\Longleftrightarrow\;\; \exists N.\ \forall n \ge N.\ s(n) = t(n). \]

The equivalence class of s is its germ at infinity — everything about s except a finite prefix. This is the relation under which the sequence-shape concepts become invariants: an IsAbsorptiveSequence (eventually constant) is exactly a sequence tail-equivalent to a constant path, and an eventually-periodic sequence is tail-equivalent to a periodic one.

tail__A_Congruence_Not_Just_An_Equivalence

Tail-equivalence is compatible with Path's pointwise addition: if s ~ s' (agree past N₁) and t ~ t' (agree past N₂) then s+t ~ s'+t' (agree past max(N₁,N₂)). So it is a genuine dedekind::category::IsCongruence with respect to std::plus<Path<T>>, and the quotient Path<T>/~ inherits the additive structure — a well-defined quotient algebra (the same structural fact #718's IsCongruence machinery certifies for ℤ/Nℤ and Frac). Reifying the quotient carrier (with chosen representatives) is deliberately deferred — the congruence is what makes the quotient well-defined; the carrier struct would be added only when a consumer needs representatives.

tail__Honesty_Obligation

The full relation quantifies over an infinite tail (∀n≥N), so it is not decidable in general. TailEquivalent's operator() therefore gives the operational reading — agreement on a sampled tail window — exactly as IsCauchySequence pins the operational subtraction shape and the convergence hooks sample a tail. The full ∃N ∀n≥N criterion is the engineer's honesty obligation; the type-level is_congruence_v registration carries the structural claim that tail-equivalence is a congruence.

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

Note: "Le silence éternel de ces espaces infinis m'effraie." — Blaise Pascal, Pensées (1670). [Trans: "The eternal silence of these infinite spaces frightens me." — the tail of a sequence is precisely the part that lives in those infinite spaces.]

Function Documentation

◆ decide_tail_equivalence()

template<typename S, typename T>
requires (IsSequence<S> && IsSequence<T> && std::same_as<typename S::Codomain, typename T::Codomain>)

dedekind::category::Ternary dedekind::sequences::decide_tail_equivalence	(	const S &	s,
		const T &	t )

constexprexport

Type-directed tail-equivalence decision: honest bool exactly on the finite-presentation domain, Ternary::Unknown otherwise.

If both S and T are IsEventuallyPeriodic, the verdict is computed by structural recursion over their lasso presentations — a comparison on the provably-sufficient window [max(Pₛ,Pₜ), max(Pₛ,Pₜ) + lcm(Cₛ,Cₜ)) — and returned as Ternary::True / Ternary::False. Otherwise the decision would require general recursion over an unbounded tail, so it is honestly rejected as Ternary::Unknown. Contrast TailEquivalent::operator() — the bool relation the congruence machinery consumes — whose fixed-window read is operational/sampled; this is the decidable, correct verdict where the type permits it.

Classes

Namespaces

Concepts