Finite History Stability

Abstract

Finite observation histories stabilize and their class growth is bounded by the finite carrier.

Theorem 1.1 (Finite history stability).

$$\begin{array}{c}\forall X,Q,[\mathrm{Fintype}(X)],\tau :X\to X,q:X\to Q,\\ c_m=|X/R_m|,m_{\ast }=\mathrm{sInf}\{m\in \mathbb{N}\mid R_m=R_{m+1}\},\\ \forall m,(x,y)\in R_{m+1}\Rightarrow (x,y)\in R_m\wedge \\ \forall m,c_m\le c_{m+1}\wedge \\ R_{m_{\ast }}=R_{\infty }\wedge \\ \forall n,m_{\ast }\le n\Rightarrow R_n=R_{\infty }\wedge \\ m_{\ast }\le c_{m_{\ast }}-c_0\wedge \\ c_{m_{\ast }}-c_0\le |X|-c_0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/FiniteHistoryStability.finite_history_stability (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite state carrier X, update tau, and readout q, let R_m relate states whose observations agree from time zero through time m, and let R_infinity require agreement at every finite future time. The quotient class count at depth m is c_m.

The finite relations decrease with depth, while their quotient class counts increase. A finite stability depth m_star reaches the infinite-future relation, and every later depth has that same relation.

Each strict refinement before m_star consumes a new quotient class. Consequently m_star is bounded by c_m_star minus c_0, and that increase is at most the carrier cardinality minus c_0. The proof handles the empty finite carrier directly and uses a private range corestriction only to apply the existing surjective-readout bound.

The source’s qualitative remark that the depth may depend on the whole system has no in-scope quantitative predicate and is therefore not asserted as a universal formal clause.

References

• Truth anchor: D5/S3/Observer/Separation/FiniteHistoryStability.finite_history_stability
• Dependency: D5/S3/Observer/Separation/FiniteFutureCongruence
• Dependency: D5/S3/Observer/Separation/FiniteObservationRefinementBound