Golden Completion Exact Linearization

Abstract

Golden cross-ratio linearization extends exactly through every defined finite iterate.

Theorem 1.1 (Exact Linearization at Every Finite Depth).

$$\begin{gathered} (\forall x:\mathbb{R}, \\ (x\ne 0)\wedge (x\ne Real.goldenConj)\Rightarrow \\ (\mathrm{goldenCrossRatio}\left(\mathrm{goldenMobius}\left(x\right)\right)=goldenProjectiveMultiplier\times \mathrm{goldenCrossRatio}\left(x\right)))\wedge \\ (\forall n:\mathbb{N},x:\mathbb{R}, \\ (\forall k:\mathbb{N},k<n\Rightarrow ((goldenMobiu{s}^{[k]})x\ne 0\wedge (goldenMobiu{s}^{[k]})x\ne Real.goldenConj))\Rightarrow \\ (\mathrm{goldenCrossRatio}\left((goldenMobiu{s}^{[n]})x\right)=goldenProjectiveMultiplie{r}^n\times \mathrm{goldenCrossRatio}\left(x\right))) \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The first clause gives the exact one-step cross-ratio multiplier on the real affine chart. The second gives the exact multiplier power for every finite iterate whose earlier orbit points remain in that chart.

The map, cross-ratio coordinate, and multiplier are the canonical objects from the GoldenMobius family; the domain premises exclude only their displayed affine-chart poles.

References

• Truth anchor: D5/S3/CompletionDynamics/GoldenMobius/GoldenCompletionExactLinearization.golden_completion_exact_linearization
• Dependency: D5/S3/CompletionDynamics/GoldenMobius/GoldenCrossRatioLinearization