Congruence Kernel

Abstract

The all-iterate pullback of an equivalence is its maximal forward congruence.

Definition 1.1 (A tau-congruence is preserved by one forward update).

$$\begin{gathered} \forall Y:\mathrm{Type},\tau :Y\to Y,S:\mathrm{StateRelation}(Y), \\ \mathrm{TauCongruence}(\tau ,S)⟺\forall y,yprime:Y,\mathrm{pair}(y,yprime)\in S\Rightarrow \mathrm{pair}(\tau (y),\tau (yprime))\in S. \end{gathered}$$

Formalization. D5/S3/Observer/Separation/CongruenceKernel.TauCongruence (✓ std3).

Source. Repository-derived.

Commentary.

A state relation S is a congruence for tau exactly when membership of an ordered pair (y,y’) in S implies membership of the updated pair (tau(y),tau(y’)).

Definition 1.2 (The congruence kernel pulls a relation back along every iterate).

$$\begin{gathered} \forall Y:\mathrm{Type},\tau :Y\to Y,R:\mathrm{StateRelation}(Y), \\ \mathrm{congruenceKernel}(\tau ,R)=\{pair:Y\times Y\mid \forall k:\mathbb{N},\mathrm{pair}(\mathrm{iterate}(\tau ,k,\mathrm{fst}(pair)),\mathrm{iterate}(\tau ,k,\mathrm{snd}(pair)))\in R\}. \end{gathered}$$

Formalization. D5/S3/Observer/Separation/CongruenceKernel.congruenceKernel (✓ std3).

Source. Repository-derived.

Commentary.

The congruence kernel of R under tau consists exactly of those state pairs whose two coordinates remain R-related after every natural iterate of tau, including the zeroth iterate.

Theorem 1.3 (Maximal forward congruence inside an equivalence).

$$\begin{array}{c}\forall Y:\mathrm{Type},\tau :Y\to Y,\\ R:\mathrm{StateRelation}(Y),\mathrm{Equivalence}(R)\Rightarrow \\ \mathrm{Equivalence}(C_{\tau }(R))\wedge \mathrm{TauCongruence}(\tau ,C_{\tau }(R))\wedge C_{\tau }(R)\subseteq R\wedge \\ (\forall S:\mathrm{StateRelation}(Y),S\subseteq R\Rightarrow C_{\tau }(S)\subseteq C_{\tau }(R))\wedge C_{\tau }(C_{\tau }(R))=C_{\tau }(R)\wedge \\ (\forall S:\mathrm{StateRelation}(Y),\mathrm{TauCongruence}(\tau ,S)\Rightarrow S\subseteq R\Rightarrow S\subseteq C_{\tau }(R))\wedge \\ (\forall S:\mathrm{StateRelation}(Y),\mathrm{TauCongruence}(\tau ,S)\Rightarrow ((S\subseteq R)⟺(S\subseteq C_{\tau }(R)))).\end{array}$$

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

Source. Repository-derived.

Commentary.

For an update tau and an equivalence R, define C_tau(R) by requiring that every iterate of tau sends a pair into R. The first six conjuncts establish equivalence, forward congruence, contraction, monotonicity, idempotence, and maximality.

The final conjunct gives the equivalent universal characterization: a forward-congruent relation lies inside R exactly when it lies inside the all-iterate kernel.

References

• Truth anchor: D5/S3/Observer/Separation/CongruenceKernel.TauCongruence
• Truth anchor: D5/S3/Observer/Separation/CongruenceKernel.congruenceKernel
• Truth anchor: D5/S3/Observer/Separation/CongruenceKernel.congruence_kernel_laws