Golden Projective Derivative

Abstract

The golden Mobius derivative equals its projective multiplier.

Theorem 1.1 (Golden Mobius Has Deriv At).

$(H a sDer i v A t g o l d e n M o bi u s g o l d e n P ro j ec t i v e M u lt i pl i er R e a l . g o l d e n R a t i o) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.golden_mobius_hasDerivAt (✓ std3). ∎

Source. Repository-derived.

Commentary.

Ordinary differentiation gives the same multiplier as exact projective linearization.

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

Theorem 1.2 (Deriv Golden Mobius At Golden).

$(d er i vg o l d e n M o bi u s R e a l . g o l d e n R a t i o = g o l d e n P ro j ec t i v e M u lt i pl i er) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.deriv_golden_mobius_at_golden (✓ std3). ∎

Source. Repository-derived.

Commentary.

Evaluation of deriv at the golden fixed point.

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

Theorem 1.3 (Abs Golden Projective Multiplier).

$(∣ g o l d e n P ro j ec t i v e M u lt i pl i er ∣ = (R e a l . g o l d e n R a t i o^{- 1})^{2}) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.abs_golden_projective_multiplier (✓ std3). ∎

Source. Repository-derived.

Commentary.

The projective multiplier has the expected positive magnitude.

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

Theorem 1.4 (Abs Golden Projective Multiplier lt One).

$(∣ g o l d e n P ro j ec t i v e M u lt i pl i er ∣ < 1) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.abs_golden_projective_multiplier_lt_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

The completion derivative is a strict contraction in projective coordinates.

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

Theorem 1.5 (Linearized Golden Has Deriv At Zero).

$(H a sDer i v A t (λ y : R \mapsto g o l d e n P ro j ec t i v e M u lt i pl i er \times y) g o l d e n P ro j ec t i v e M u lt i pl i er 0) .$

Proof. Machine-checked in Lean as D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.linearized_golden_hasDerivAt_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplication by the golden multiplier has that derivative at zero.

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/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.abs_golden_projective_multiplier
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.abs_golden_projective_multiplier_lt_one
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.deriv_golden_mobius_at_golden
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.golden_mobius_hasDerivAt
Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative.linearized_golden_hasDerivAt_zero
Dependency: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization

Keyboard shortcuts

trureturing Blueprint

Golden Projective Derivative

Abstract

References