Golden Cross Ratio Linearization

Abstract

Golden cross-ratio coordinates exactly linearize the Mobius map.

Theorem 1.1 (Golden Cross Ratio At Golden).

$$(goldenCrossRatioReal.goldenRatio=0).$$

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

Source. Repository-derived.

Commentary.

This theorem establishes golden cross ratio at golden 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 (Golden Mobius Sub Golden).

$$\begin{gathered} \forall x:\mathbb{R}, \\ (x\ne 0)\Rightarrow \\ (goldenMobiusx-Real.goldenRatio=-(x-Real.goldenRatio)/(Real.goldenRatio\times x)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Numerator identity in a denominator-separated form.

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

Theorem 1.3 (Golden Mobius Sub Conjugate).

$$\begin{gathered} \forall x:\mathbb{R}, \\ (x\ne 0)\Rightarrow \\ (goldenMobiusx-Real.goldenConj=Real.goldenRatio\times (x-Real.goldenConj)/x). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Denominator identity in a denominator-separated form.

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

Theorem 1.4 (Golden Cross Ratio Linearization).

$$\begin{gathered} \forall x:\mathbb{R}, \\ (x\ne 0)\wedge (x\ne Real.goldenConj)\Rightarrow \\ (goldenCrossRatio(goldenMobiusx)=goldenProjectiveMultiplier\times goldenCrossRatiox). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Exact golden projective linearization.

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

Theorem 1.5 (Positive Avoids Golden Singularities).

$$\begin{gathered} \forall x:\mathbb{R}, \\ (0<x)\Rightarrow \\ (x\ne 0\wedge x\ne Real.goldenConj). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Positive points avoid both affine-chart singularities.

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

Theorem 1.6 (Golden Mobius Iterate pos).

$$\begin{gathered} \forall n:\mathbb{N},x:\mathbb{R}, \\ (0<x)\Rightarrow \\ (0<(goldenMobiu{s}^{[n]})x). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Positivity is invariant under every finite Mobius iterate.

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

Theorem 1.7 (Golden Cross Ratio Iterate).

$$\begin{gathered} \forall n:\mathbb{N},x:\mathbb{R}, \\ (0<x)\Rightarrow \\ (goldenCrossRatio((goldenMobiu{s}^{[n]})x)=goldenProjectiveMultiplie{r}^n\times goldenCrossRatiox). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Exact geometric contraction law on the positive affine chart.

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/GoldenCrossRatioLinearization.golden_cross_ratio_at_golden
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.golden_cross_ratio_iterate
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.golden_cross_ratio_linearization
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.golden_mobius_iterate_pos
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.golden_mobius_sub_conjugate
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.golden_mobius_sub_golden
• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization.positive_avoids_golden_singularities
• Dependency: D5/S3/CompletionDynamics/GoldenMobius/GoldenMobiusMap