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

Detailed Description

template<typename Seq>
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.

tail__From_The_Undecidable_General_Case_To_A_Decidable_Bool

Tail-equivalence is undecidable in general — deciding s ~ t means consuming the infinite tail, i.e. general recursion over a codata stream whose state space is unbounded; the honest verdict is Ternary::Unknown. It collapses to a decidable bool exactly when both streams have a finite-state presentation — a lasso: a finite prefix followed by a cycle, \(s(n) = s(n + C)\ \forall n \ge P\). On a lasso the decision is structural recursion over the finite (prefix, cycle) witness: past max(Pₛ,Pₜ) both streams factor through a common cycle of length lcm(Cₛ,Cₜ), so agreement on one full period is agreement forever — a provably sufficient, terminating check, not a sampled heuristic.

This is the type-directed bridge from the general (Ternary) case to the decidable (Boolean) case: the finite-presentation witness IsEventuallyPeriodic is exactly what licenses structural recursion. It unifies the :convergence shape concepts as lasso shapes — IsAbsorptiveSequence is a prefix + 1-cycle (eventually constant), IsPeriodicSequence<N> is a 0-prefix + N-cycle — and coheres with the #719 Slice 5 collapse: a finite presentation is a countable / Boole object (decidable), its absence is Kleene.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/sequences/tail_equivalence.cppm