The cat-map index orbit is infinite

For the Arnold cat-map matrix M = !![2,1;1,1] : Matrix (Fin 2) (Fin 2) ℤ, this file proves that the forward orbit p ↦ Mᵖ ·ᵥ v of any nonzero integer vector v is injective in p, hence the orbit is an infinite set. This is the number-theoretic heart of the ergodicity proof for the hyperbolic toral automorphism: a Fourier coefficient that is constant along such an orbit and ℓ²-summable must vanish.

The argument is the eigen-covector / growth one (Walkden, Ergodic Theory, Lecture 17): the matrix M is symmetric with two real eigenvalues λ = (3+√5)/2 > 1 and λ⁻¹ = (3-√5)/2 ∈ (0,1), neither a root of unity. Pairing a vector with the two eigen-covectors w (for λ) and u (for λ⁻¹) gives two real functionals φ, ψ with φ(Mᵏ v) = λᵏ φ(v) and ψ(Mᵏ v) = λ⁻ᵏ ψ(v). If Mᵏ v = v for some k ≥ 1 then φ(v) = λᵏ φ(v) and ψ(v) = λ⁻ᵏ ψ(v) with λᵏ ≠ 1, forcing φ(v) = ψ(v) = 0; since w, u span, v = 0.

Main results

• Oseledets.CatMapToral.catℤ — the integer cat-map matrix !![2,1;1,1].
• Oseledets.CatMapToral.eq_zero_of_pow_mulVec_eq — Mᵏ ·ᵥ v = v, k ≥ 1 ⇒ v = 0 over ℝ.
• Oseledets.CatMapToral.orbit_injective — p ↦ Mᵖ ·ᵥ v is injective for nonzero integer v.
• Oseledets.CatMapToral.orbit_infinite — the orbit {Mᵖ ·ᵥ v | p} is infinite for nonzero v.

The cat-map matrix and its real eigen-data

def Oseledets.CatMapToral.catℤ : Matrix (Fin 2) (Fin 2) ℤ

The Arnold cat-map matrix !![2,1;1,1] over ℤ.

Equations

• Oseledets.CatMapToral.catℤ = !![2, 1; 1, 1]

noncomputable def Oseledets.CatMapToral.catℝ : Matrix (Fin 2) (Fin 2) ℝ

The cat-map matrix over ℝ (entrywise integer cast).

Equations

• Oseledets.CatMapToral.catℝ = !![2, 1; 1, 1]

noncomputable def Oseledets.CatMapToral.lam : ℝ

The dominant eigenvalue λ = (3 + √5)/2 > 1.

Equations

• Oseledets.CatMapToral.lam = (3 + √5) / 2

theorem Oseledets.CatMapToral.sqrt5_lt_three : √5 < 3

√5 < 3 (since 5 < 9).

theorem Oseledets.CatMapToral.two_lt_sqrt5 : 2 < √5

2 < √5 (since 4 < 5).

theorem Oseledets.CatMapToral.sqrt5_sq : √5 ^ 2 = 5

(√5)² = 5.

theorem Oseledets.CatMapToral.one_lt_lam : 1 < lam

The dominant eigenvalue is hyperbolic: 1 < λ.

theorem Oseledets.CatMapToral.lam_sq : lam ^ 2 = 3 * lam - 1

λ satisfies the characteristic equation λ² = 3λ - 1.

noncomputable def Oseledets.CatMapToral.mu : ℝ

The stable eigenvalue μ = (3 - √5)/2.

Equations

• Oseledets.CatMapToral.mu = (3 - √5) / 2

theorem Oseledets.CatMapToral.mu_sq : mu ^ 2 = 3 * mu - 1

μ satisfies the same characteristic equation μ² = 3μ - 1.

theorem Oseledets.CatMapToral.lam_sub_mu : lam - mu = √5

The two eigenvalues are distinct: λ - μ = √5 ≠ 0.

The growth functionals coming from the two eigen-covectors

Because catℝ is symmetric, an eigenvector is simultaneously an eigen-covector. Pairing with ![1, λ-2] and ![1, μ-2] (the eigenvectors for λ and μ) gives two linear functionals that scale by λ and μ respectively under one step of the dynamics.

theorem Oseledets.CatMapToral.catℝ_mulVec_apply (v : Fin 2 → ℝ) : catℝ.mulVec v = ![2 * v 0 + v 1, v 0 + v 1]

Evaluate catℝ *ᵥ v componentwise as a Fin 2 vector.

theorem Oseledets.CatMapToral.catℝ_mulVec_eigen_lam : catℝ.mulVec ![1, lam - 2] = lam • ![1, lam - 2]

One application of the cat-map matrix to the λ-eigenvector scales it by λ.

theorem Oseledets.CatMapToral.catℝ_mulVec_eigen_mu : catℝ.mulVec ![1, mu - 2] = mu • ![1, mu - 2]

One application of the cat-map matrix to the μ-eigenvector scales it by μ.

theorem Oseledets.CatMapToral.catℝ_transpose : catℝ.transpose = catℝ

catℝ is symmetric, hence equal to its transpose.

theorem Oseledets.CatMapToral.catℝ_pow_mulVec_eigen_lam (k : ℕ) : (catℝ ^ k).mulVec ![1, lam - 2] = lam ^ k • ![1, lam - 2]

The k-th power of catℝ scales the λ-eigenvector by λᵏ.

theorem Oseledets.CatMapToral.catℝ_pow_mulVec_eigen_mu (k : ℕ) : (catℝ ^ k).mulVec ![1, mu - 2] = mu ^ k • ![1, mu - 2]

The k-th power of catℝ scales the μ-eigenvector by μᵏ.

theorem Oseledets.CatMapToral.dotProduct_pow_mulVec (k : ℕ) (w v : Fin 2 → ℝ) : w ⬝ᵥ (catℝ ^ k).mulVec v = (catℝ ^ k).mulVec w ⬝ᵥ v

Adjoint identity for the symmetric matrix catℝ and its powers: w ⬝ᵥ (catℝᵏ *ᵥ v) = (catℝᵏ *ᵥ w) ⬝ᵥ v.

A +1-eigenvector of a power forces the zero vector

theorem Oseledets.CatMapToral.eq_zero_of_pow_mulVec_eq {k : ℕ} (hk : 1 ≤ k) {v : Fin 2 → ℝ} (hv : (catℝ ^ k).mulVec v = v) : v = 0

If catℝᵏ ·ᵥ v = v for some k ≥ 1, then v = 0. Pairing with the two eigen-covectors collapses both coordinates: the λ-pairing gives λᵏ ⟨w,v⟩ = ⟨w,v⟩ with λᵏ ≠ 1, hence ⟨w,v⟩ = 0; likewise ⟨u,v⟩ = 0; the two covectors are independent, so v = 0.

From the eigen-collapse to orbit injectivity and infiniteness

theorem Oseledets.CatMapToral.catℝ_eq_map_catℤ : catℝ = catℤ.map Int.cast

The real cat-map matrix is the entrywise integer cast of the integer one.

theorem Oseledets.CatMapToral.det_catℝ : catℝ.det = 1

det catℝ = 1, hence every power has nonzero determinant.

theorem Oseledets.CatMapToral.catℝ_pow_eq_map (p : ℕ) : catℝ ^ p = (catℤ ^ p).map Int.cast

catℝ ^ p is the entrywise integer cast of catℤ ^ p.

theorem Oseledets.CatMapToral.cast_pow_mulVec (p : ℕ) (v : Fin 2 → ℤ) : (fun (i : Fin 2) => ↑((catℤ ^ p).mulVec v i)) = (catℝ ^ p).mulVec fun (i : Fin 2) => ↑(v i)

Casting an integer orbit step to ℝ is the corresponding real orbit step.

theorem Oseledets.CatMapToral.orbit_injective {v : Fin 2 → ℤ} (hv : v ≠ 0) : Function.Injective fun (p : ℕ) => (catℤ ^ p).mulVec v

Orbit injectivity. For nonzero integer v, the forward orbit p ↦ catℤᵖ ·ᵥ v is injective.

theorem Oseledets.CatMapToral.orbit_infinite {v : Fin 2 → ℤ} (hv : v ≠ 0) : (Set.range fun (p : ℕ) => (catℤ ^ p).mulVec v).Infinite

Orbit infiniteness. For nonzero integer v, the orbit {catℤᵖ ·ᵥ v | p} is infinite.