Finite Monotone Termination

Abstract

Finite monotone refinement terminates, while its limiting fixed point need not be unique.

Theorem 1.1 (Finite monotone termination with nonunique limits).

$$\begin{gathered} (\forall alpha:\mathrm{Type},[\mathrm{Finite}(alpha)],[\mathrm{PartialOrder}(alpha)],update:\mathrm{OrderHom}\left(alpha,alpha\right),initial:alpha,(\forall state:alpha,\mathrm{update}\left(state\right)\le state)\Rightarrow \\ \exists N\in \mathbb{N},\mathrm{IsFixedPt}\left(update,\mathrm{iterate}\left(update,N,initial\right)\right)\wedge \forall n\in \mathbb{N},N\le n\Rightarrow \mathrm{iterate}\left(update,n,initial\right)=\mathrm{iterate}\left(update,N,initial\right))\wedge \\ (\exists x,y:Bool,x\ne y\wedge (\forall n\in \mathbb{N},\mathrm{iterate}\left(id,n,x\right)=x)\wedge (\forall n\in \mathbb{N},\mathrm{iterate}\left(id,n,y\right)=y)\wedge \mathrm{IsFixedPt}\left(id,x\right)\wedge \mathrm{IsFixedPt}\left(id,y\right)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S1/FixedPoints/FiniteMonotoneTermination.finite_monotone_termination_and_nonunique_example (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let alpha be a finite partial order and let update be a monotone endomorphism. The hypothesis update state <= state orients strict refinement downward: whenever an update is not fixed, antisymmetry makes that step strictly smaller.

The iterates from any initial state form an antitone chain. Pinned Mathlib’s WellFoundedLT.antitone_chain_condition, together with the finite-order well-founded instance, gives an index after which the chain is constant. Equality at the next index states that the reached value is a fixed point.

The uniqueness implication is refuted constructively in the same declaration. The identity update on Bool is monotone; the distinct initial states false and true remain at distinct fixed points under every iterate.

Repository search found a finite-set contraction specialization but no generic finite-poset wrapper. The proof therefore directly reuses the exact pinned antitone-chain theorem rather than reproving finite stabilization.

References

• Truth anchor: D5/S1/FixedPoints/FiniteMonotoneTermination.finite_monotone_termination_and_nonunique_example