Maximal Forward-Invariant Subkernel

Abstract

Every equivalence relation has a greatest forward-invariant subrelation.

Theorem 1.1 (The forward-orbit kernel is the greatest invariant subkernel).

$$\begin{gathered} \forall X:\mathrm{Type},F:X\to X, \\ {K}_q:\mathrm{Set}(X\times X),\mathrm{Equivalence}\left(K_q\right)\Rightarrow \\ {K}_{infinity}=\{(x,y)\mid \forall n\in \mathbb{N},(F^n(x),F^n(y))\in K_q\}\wedge \\ \mathrm{Equivalence}\left(K_{infinity}\right)\wedge K_{infinity}\subseteq K_q\wedge \\ (\forall x,y,(x,y)\in K_{infinity}\Rightarrow (F(x),F(y))\in K_{infinity})\wedge \\ \forall R:\mathrm{Set}(X\times X),(R\subseteq K_q\wedge \forall x,y,(x,y)\in R\Rightarrow (F(x),F(y))\in R)\Rightarrow R\subseteq K_{infinity}. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let Kq be an equivalence relation on X and let F be a self-map of X. The relation K-infinity consists of the pairs whose complete forward orbits remain related by Kq.

K-infinity is itself an equivalence relation contained in Kq and is preserved by applying F to both coordinates. Every relation contained in Kq with the same forward-invariance property is contained in K-infinity, which proves both existence and maximality.

The module also identifies K-infinity with the greatest fixed point of the monotone one-step refinement operator. The repository’s general Knaster-Tarski wrapper supplies the extremal fixed-point facts; pinned Mathlib supplies OrderHom.gfp and the complete lattice of relations.

References

• Truth anchor: D5/S1/FixedPoints/MaximalForwardInvariantSubkernel.maximal_forward_invariant_subkernel
• Dependency: D5/S1/Dynamics/KnasterTarski