Finite Equivalence Descent

Abstract

Finite equivalence refinement stabilizes within its quotient-class budget.

Theorem 1.1 (Finite descent and general stability bound).

$$\begin{array}{c}\forall Y,[\mathrm{Fintype}(Y)],R:\mathrm{Setoid}(Y),\tau :Y\to Y,\\ R_0=R\wedge \\ (\forall m,R_{m+1}=\{(x,y)\mid R(x,y)\wedge R_m(\tau (x),\tau (y))\})\wedge \\ (\forall m,R_m=\{(x,y)\mid \forall k,k\le m\Rightarrow R({\tau }^k(x),{\tau }^k(y))\})\wedge \\ C_{\tau }(R)=\{(x,y)\mid \forall k,R({\tau }^k(x),{\tau }^k(y))\}\wedge \\ m_R=\mathrm{sInf}\{m\in \mathbb{N}\mid R_m=R_{m+1}\}\wedge R_{m_R}=R_{m_R+1}\wedge \\ (\forall n,R_n=R_{n+1}\Rightarrow m_R\le n)\wedge \\ (\forall n,m_R\le n\Rightarrow R_n=C_{\tau }(R))\wedge \\ m_R\le |Y/C_{\tau }(R)|-|Y/R|\le |Y|-|Y/R|.\end{array}$$

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

Source. Repository-derived.

Commentary.

Let Y be a finite carrier, R an equivalence relation, and tau its deterministic update. The canonical readout sends each state to its R-class. Equality of finite readout words then constructs the source sequence directly from R and iterates of tau.

The zero and successor clauses identify this sequence with repeated intersection by the one-step pullback. The finite-intersection formula states equivalently that two states remain related at every iterate from zero through the chosen depth.

The displayed depth is the least index where consecutive finite relations agree. At that depth and every later one, the relation is the canonical all-future core.

The terminal quotient can gain at most one unit of stability depth per new class. This gives the sharp difference between terminal and initial quotient counts, followed by the carrier bound. The empty finite carrier is included and handled directly.

References

• Truth anchor: D5/S3/Observer/Prediction/FiniteEquivalenceDescent.finite_equivalence_descent_and_stability_bound
• Dependency: D5/S3/Observer/Prediction/StableDepthCardinalityBounds