Finite Stability Class Bound

Abstract

The least finite-future stability depth obeys the exact quotient-class bound.

Theorem 1.1 (Least finite-future stability depth).

$$\begin{array}{c}\forall X,Q:\mathrm{Type},[\mathrm{Fintype}(X)],\\ F:X\to X,q:X\to Q,\\ m_{\ast }=\mathrm{sInf}\{n\in \mathbb{N}\mid K_n=K_{n+1}\},\\ K_{m_{\ast }}=K_{m_{\ast }+1}=K_{\infty }\wedge \\ (\forall n,K_n=K_{n+1}\Rightarrow m_{\ast }\le n)\wedge \\ m_{\ast }\le |X/K_{\infty }|-|X/K_q|\le |X|-|\mathrm{Im}(q)|.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Prediction/FiniteStabilityClassBound.finite_stability_class_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be a finite state carrier, let F be its deterministic update, and let q be an arbitrary readout. The relation K_n identifies states with equal readouts from time zero through time n, while K_infinity identifies states with equal readouts at every time.

The displayed depth is the canonical least index where two adjacent finite-future relations agree. At that depth both adjacent relations equal the complete-future relation, and the quantified clause states minimality directly.

Each strict refinement creates at least one new quotient class. The resulting depth is therefore bounded by the difference between the complete-future and current-readout quotients; the canonical kernel-quotient equivalence identifies the latter with the realized image of q.

References

• Truth anchor: D5/S3/Observer/Prediction/FiniteStabilityClassBound.finite_stability_class_bound
• Dependency: D5/S3/Observer/Prediction/StableDepthCardinalityBounds