Coincidence Length and the Separating Horizon¶
For a given observation on a finite state space, which delay windows separate orbits, and what is the shortest one? The coincidence length answers both questions exactly.
Coincidence length¶
Proved (coincidenceLength)
The coincidence length \(c(x, y) \in \mathbb{N}_\infty\) is the first index \(i\) with \(\alpha(f^i x) \ne \alpha(f^i y)\), or \(\infty\) if the observations always agree.
Two windows of length \(k\) agree exactly when \(k \le c(x, y)\)
(delayEmbedding_eq_iff_le_coincidenceLength). The coincidence length is symmetric, is
\(\infty\) on the diagonal, is \(0\) iff the first observations differ, and satisfies the
one-step recursion \(c(x, y) = c(fx, fy) + 1\) when \(\alpha(x) = \alpha(y)\)
(coincidenceLength_of_eq). Hence \(\alpha\) separates orbits at window \(k\) iff
\(c(x, y) < k\) for every pair of distinct states
(separatesOrbits_iff_forall_coincidenceLength_lt).
The separating horizon¶
Proved (separatesOrbits_iff_separatingHorizon_le)
Let \(H = \sup_{x \ne y} (c(x, y) + 1) \in \mathbb{N}_\infty\) (separatingHorizon). Then a
window of length \(k\) separates orbits iff \(k \ge H\). When \(H\) is finite it is the
least separating window (isLeast_separatingHorizon).
\(H = 0\) iff there are no two distinct states, and a pair that is never distinguished
forces \(H = \infty\). On a finite state space with at least two states the supremum is
attained by a distinct pair
(exists_separatingHorizon_eq), so \(H = \infty\) iff some distinct pair is never
distinguished (separatingHorizon_eq_top_iff). In particular some window separates orbits
iff every distinct pair is eventually distinguished (exists_separatingWindow_iff).
A sharp bound¶
Proved (separatingHorizon_le_card_sub_one)
When a finite separating window exists, the least one uses at most \(N - 1\) observations on
\(N \ge 1\) states; the empty state space has horizon zero. Equivalently, equal windows of length
\(N - 1\) force equal observations at every time (forall_iterate_eq_of_delayEmbedding_eq).
No injectivity of \(f\) or \(\alpha\) is assumed.
The proof tracks the partition of states by their windows of length \(j\). Each longer window refines it, and once a refinement step changes nothing, no later step does. A partition of \(N\) states can be strictly refined at most \(N - 1\) times, so the windows of length \(N - 1\) already determine all observations.
The bound is attained. For \(N \ge 2\), on the countdown chain \(i \mapsto i - 1\) on
\(\{0, \dots, N-1\}\), with \(0\) fixed and observed by the indicator of \(0\), the states
\(N-1\) and \(N-2\) first differ at time \(N - 2\), so exactly \(N - 1\) coordinates are needed
(separatingHorizon_countdown); for \(N \le 1\) the horizon is zero.
Deciding separability¶
For states \(\mathrm{Fin}\,n\) and observations in a type with decidable equality,
horizonSearch scans the windows of length \(k < n\) and returns
either the first separating length or a distinct pair with equal windows of length
\(n - 1\), which by the sharp bound is never distinguished. Both answers are proved sound
and complete: the search returns separating k iff the horizon is \(k\)
(horizonSearch_eq_separating_iff), and a pair iff the horizon is infinite
(exists_horizonSearch_eq_indistinguishable_iff). Real-valued data needs a representation
with decidable equality, such as rationals; equality of reals is not decided.
Scope¶
These are statements about exact observations of a finite model. A finite sample of a continuous system is not a finite state space, and nothing here bounds the number of measurements needed for noisy data.