Commuting Closure Common Fixed Point

Abstract

Two commuting closure operators compose to a closure whose fixed points are exactly their common fixed points.

Theorem 1.1 (Commuting Composition Apply).

$$\begin{gathered} \forall alpha:Type,first:ClosureOperatoralpha,second:ClosureOperatoralpha,x:alpha,[\mathrm{PartialOrder}\left(alpha\right)], \\ (Function.Commutefirstsecond)\Rightarrow \\ (commutingCompositionfirstsecondcommutex=first(secondx)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commutingComposition_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

This theorem establishes commuting composition apply in the module’s typed setting.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.2 (Commuting Closure Composition Fixed iff).

$$\begin{gathered} \forall alpha:Type,first:ClosureOperatoralpha,second:ClosureOperatoralpha,x:alpha,[\mathrm{PartialOrder}\left(alpha\right)], \\ (Function.Commutefirstsecond)\Rightarrow \\ (commutingCompositionfirstsecondcommutex=x\iff firstx=x\wedge secondx=x). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commuting_closure_composition_fixed_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

A point is fixed by the commuting composition exactly when it is fixed by both constituent closures.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.3 (Commuting Composition Order Independent).

$$\begin{gathered} \forall alpha:Type,first:ClosureOperatoralpha,second:ClosureOperatoralpha,x:alpha,[\mathrm{PartialOrder}\left(alpha\right)], \\ (Function.Commutefirstsecond)\Rightarrow \\ (commutingCompositionfirstsecondcommutex=commutingCompositionsecondfirstcommute.symmx). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commuting_composition_order_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

Commutativity makes the one-pass common closure independent of order.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

References

• Truth anchor: D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commutingComposition_apply
• Truth anchor: D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commuting_closure_composition_fixed_iff
• Truth anchor: D5/S3/ObserverMemory/RefinementClosure/CommutingClosureCommonFixedPoint.commuting_composition_order_independent