Torsion traces forced by finite Markoff orbits

Use returns of coordinate rotations to obtain torsion traces and rule out finite complex orbits away from the origin.

theorem BGS.Markoff.normalizedRotate1Surface_injective {R : Type u} [CommRing R] [Invertible 3] : Function.Injective normalizedRotate1Surface

theorem BGS.Markoff.coe_iterate_normalizedRotate1Surface {R : Type u} [CommRing R] (x : NormalizedMarkoffSurface R) (n : ℕ) : ↑(normalizedRotate1Surface^[n] x) = normalizedRotate1^[n] ↑x

theorem BGS.Markoff.exists_positive_normalizedRotate1Surface_return_of_finite_component {R : Type u} [CommRing R] [Invertible 3] {x y : NormalizedMarkoffSurface R} (hfinite : (normalizedGammaOrbit x).Finite) (hxy : SameNormalizedComponent x y) : ∃ (n : ℕ), 0 < n ∧ normalizedRotate1Surface^[n] y = y

theorem BGS.Markoff.finite_component_coordinate1_has_torsion_trace {K : Type u} [Field K] [IsAlgClosed K] [CharZero K] [Invertible 3] {x y : NormalizedMarkoffSurface K} (hfinite : (normalizedGammaOrbit x).Finite) (hxy : SameNormalizedComponent x y) : ∃ (w : Kˣ), IsOfFinOrder w ∧ (↑y).u1 = splitTorusTrace w

theorem BGS.Markoff.finite_normalizedGammaOrbit_has_torsion_traces {K : Type u} [Field K] [IsAlgClosed K] [CharZero K] [Invertible 3] (x : NormalizedMarkoffSurface K) (hfinite : (normalizedGammaOrbit x).Finite) : ∃ (w₁ : Kˣ) (w₂ : Kˣ) (w₃ : Kˣ), IsOfFinOrder w₁ ∧ IsOfFinOrder w₂ ∧ IsOfFinOrder w₃ ∧ (↑x).u1 = splitTorusTrace w₁ ∧ (↑x).u2 = splitTorusTrace w₂ ∧ (↑x).u3 = splitTorusTrace w₃

theorem BGS.Markoff.complex_normalizedPoint_eq_origin_of_finite_normalizedGammaOrbit (x : NormalizedMarkoffSurface ℂ) (hfinite : (normalizedGammaOrbit x).Finite) : ↑x = normalizedOrigin

theorem BGS.Markoff.complex_normalizedGammaOrbit_infinite_of_ne_origin (x : NormalizedMarkoffSurface ℂ) (hx : ↑x ≠ normalizedOrigin) : (normalizedGammaOrbit x).Infinite