Differentiable Fixed Point Conjugacy

Abstract

Nondegenerate differentiable bridges preserve local multipliers.

Theorem 1.1 (Derivative Intertwining At Fixed Point).

$\forall b r i d g e : R \to R, so u rce St e p : R \to R, t a r g e tSt e p : R \to R, x : R, d B r i d g e : R, d S o u rce : R, d T a r g e t : R, (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) \land (H a sDer i v A t b r i d g e d B r i d g e x) \land (H a sDer i v A t so u rce St e p d S o u rce x) \land (H a sDer i v A tt a r g e tSt e p d T a r g e t (b r i d g e x)) \Rightarrow (d B r i d g e \times d S o u rce = d T a r g e t \times d B r i d g e) .$

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

Source. Repository-derived.

Commentary.

The chain rule intertwines the two local multipliers at a fixed point.

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

Theorem 1.2 (Multiplier eq Of Nondegenerate Bridge).

$\forall b r i d g e : R \to R, so u rce St e p : R \to R, t a r g e tSt e p : R \to R, x : R, d B r i d g e : R, d S o u rce : R, d T a r g e t : R, (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) \land (H a sDer i v A t b r i d g e d B r i d g e x) \land (H a sDer i v A t so u rce St e p d S o u rce x) \land (H a sDer i v A tt a r g e tSt e p d T a r g e t (b r i d g e x)) \land (d B r i d g e \neq = 0) \Rightarrow (d S o u rce = d T a r g e t) .$

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

Source. Repository-derived.

Commentary.

A nonzero bridge derivative forces equality of local multipliers.

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

Theorem 1.3 (Attracting Multiplier iff).

$\forall b r i d g e : R \to R, so u rce St e p : R \to R, t a r g e tSt e p : R \to R, x : R, d B r i d g e : R, d S o u rce : R, d T a r g e t : R, (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) \land (H a sDer i v A t b r i d g e d B r i d g e x) \land (H a sDer i v A t so u rce St e p d S o u rce x) \land (H a sDer i v A tt a r g e tSt e p d T a r g e t (b r i d g e x)) \land (d B r i d g e \neq = 0) \Rightarrow (∣ d S o u rce ∣ < 1 \Leftrightarrow ∣ d T a r g e t ∣ < 1) .$

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

Source. Repository-derived.

Commentary.

Strict attraction is preserved by a nondegenerate bridge.

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

Theorem 1.4 (Neutral Multiplier iff).

$\forall b r i d g e : R \to R, so u rce St e p : R \to R, t a r g e tSt e p : R \to R, x : R, d B r i d g e : R, d S o u rce : R, d T a r g e t : R, (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) \land (H a sDer i v A t b r i d g e d B r i d g e x) \land (H a sDer i v A t so u rce St e p d S o u rce x) \land (H a sDer i v A tt a r g e tSt e p d T a r g e t (b r i d g e x)) \land (d B r i d g e \neq = 0) \Rightarrow (∣ d S o u rce ∣ = 1 \Leftrightarrow ∣ d T a r g e t ∣ = 1) .$

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

Source. Repository-derived.

Commentary.

Neutrality is preserved by a nondegenerate bridge.

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

Theorem 1.5 (Repelling Multiplier iff).

$\forall b r i d g e : R \to R, so u rce St e p : R \to R, t a r g e tSt e p : R \to R, x : R, d B r i d g e : R, d S o u rce : R, d T a r g e t : R, (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) \land (H a sDer i v A t b r i d g e d B r i d g e x) \land (H a sDer i v A t so u rce St e p d S o u rce x) \land (H a sDer i v A tt a r g e tSt e p d T a r g e t (b r i d g e x)) \land (d B r i d g e \neq = 0) \Rightarrow (1 < ∣ d S o u rce ∣ \Leftrightarrow 1 < ∣ d T a r g e t ∣) .$

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

Source. Repository-derived.

Commentary.

Repulsion is preserved by a nondegenerate bridge.

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/DifferentiableFixedPointConjugacy.attracting_multiplier_iff
Truth anchor: D5/S3/Observer/Bridges/DifferentiableFixedPointConjugacy.derivative_intertwining_at_fixed_point
Truth anchor: D5/S3/Observer/Bridges/DifferentiableFixedPointConjugacy.multiplier_eq_of_nondegenerate_bridge
Truth anchor: D5/S3/Observer/Bridges/DifferentiableFixedPointConjugacy.neutral_multiplier_iff
Truth anchor: D5/S3/Observer/Bridges/DifferentiableFixedPointConjugacy.repelling_multiplier_iff
Dependency: D5/S3/Observer/Bridges/FixedPointSemiconjugacy

Keyboard shortcuts

trureturing Blueprint

Differentiable Fixed Point Conjugacy

Abstract

References