Fixed Point Semiconjugacy

Abstract

Semiconjugate bridges transport fixed points and stable fibers.

Theorem 1.1 (Fixed Point Maps).

$\forall X : T y p e, Y : T y p e, b r i d g e : X \to Y, so u rce St e p : X \to X, t a r g e tSt e p : Y \to Y, x : X, (F u n c t i o n . S e mi co njb r i d g eso u rce St e pt a r g e tSt e p) \land (F u n c t i o n . I s F i x e d Pt so u rce St e p x) \Rightarrow (F u n c t i o n . I s F i x e d Ptt a r g e tSt e p (b r i d g e x)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_maps (✓ std3). ∎

Source. Repository-derived.

Commentary.

A fixed point is transported through every semiconjugate bridge.

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

Theorem 1.2 (Fixed Point Reflects Of Injective).

$\forall X : T y p e, Y : T y p e, b r i d g e : X \to Y, so u rce St e p : X \to X, t a r g e tSt e p : Y \to Y, x : X, (F u n c t i o n . S e mi co njb r i d g eso u rce St e pt a r g e tSt e p) \land (F u n c t i o n . I nj ec t i v e b r i d g e) \land (F u n c t i o n . I s F i x e d Ptt a r g e tSt e p (b r i d g e x)) \Rightarrow (F u n c t i o n . I s F i x e d Pt so u rce St e p x) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_reflects_of_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

An injective semiconjugate bridge also reflects fixed points.

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

Theorem 1.3 (Fixed Point iff Of Injective).

$\forall X : T y p e, Y : T y p e, b r i d g e : X \to Y, so u rce St e p : X \to X, t a r g e tSt e p : Y \to Y, x : X, (F u n c t i o n . S e mi co njb r i d g eso u rce St e pt a r g e tSt e p) \land (F u n c t i o n . I nj ec t i v e b r i d g e) \Rightarrow (F u n c t i o n . I s F i x e d Pt so u rce St e p x \Leftrightarrow F u n c t i o n . I s F i x e d Ptt a r g e tSt e p (b r i d g e x)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_iff_of_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under an injective semiconjugacy, fixedness is exactly preserved.

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

Theorem 1.4 (Observation Fiber Forward Invariant).

$\forall X : T y p e, Y : T y p e, b r i d g e : X \to Y, so u rce St e p : X \to X, t a r g e tSt e p : Y \to Y, x_{1} : X, x_{2} : X, (F u n c t i o n . S e mi co njb r i d g eso u rce St e pt a r g e tSt e p) \land (b r i d g e x_{1} = b r i d g e x_{2}) \Rightarrow (b r i d g e (so u rce St e p x_{1}) = b r i d g e (so u rce St e p x_{2})) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.observation_fiber_forward_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equality under the observer remains equal after one semiconjugate step.

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

Theorem 1.5 (Semiconjugacy Iterate).

$\forall X : T y p e, Y : T y p e, b r i d g e : X \to Y, so u rce St e p : X \to X, t a r g e tSt e p : Y \to Y, n : N, x : X, (F u n c t i o n . S e mi co njb r i d g eso u rce St e pt a r g e tSt e p) \Rightarrow (b r i d g e ((so u rce St e p^{[n]}) x) = (t a r g e tSt e p^{[n]}) (b r i d g e x)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.semiconjugacy_iterate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Semiconjugacy transports every finite iterate, not only one step.

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

Theorem 1.6 (Fixed Point Maps Across Composite).

$\forall X : T y p e, Y : T y p e, Z : T y p e, f i rs tB r i d g e : X \to Y, seco n d B r i d g e : Y \to Z, f i rs tSt e p : X \to X, seco n d St e p : Y \to Y, t hi r d St e p : Z \to Z, x : X, (F u n c t i o n . S e mi co nj f i rs tB r i d g e f i rs tSt e p seco n d St e p) \land (F u n c t i o n . S e mi co nj seco n d B r i d g eseco n d St e pt hi r d St e p) \land (F u n c t i o n . I s F i x e d Pt f i rs tSt e p x) \Rightarrow (F u n c t i o n . I s F i x e d Ptt hi r d St e p ((seco n d B r i d g e \circ f i rs tB r i d g e) x)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_maps_across_composite (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fixed-point transport composes along two observer bridges.

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/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_iff_of_injective
Truth anchor: D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_maps
Truth anchor: D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_maps_across_composite
Truth anchor: D5/S3/Observer/Bridges/FixedPointSemiconjugacy.fixed_point_reflects_of_injective
Truth anchor: D5/S3/Observer/Bridges/FixedPointSemiconjugacy.observation_fiber_forward_invariant
Truth anchor: D5/S3/Observer/Bridges/FixedPointSemiconjugacy.semiconjugacy_iterate

Keyboard shortcuts

trureturing Blueprint

Fixed Point Semiconjugacy

Abstract

References