The genuine Arnold cat-map derivative cocycle has a positive top exponent

The companion module Oseledets/Examples/Elementary.lean realizes the cat-map matrix M = !![2,1;1,1] as a constant cocycle over the doubling map and reads off its Lyapunov spectrum log((3 ± √5)/2) (Oseledets.catMapMatrix_exponents). That theorem carries an explicit honesty caveat: the base is the doubling map, not the genuine cat-map dynamics, and the cocycle is the bare constant matrix, not the derivative cocycle of the Arnold cat map.

This module removes that caveat on two fronts, banking each independently.

Grade 1 — the genuine ergodic torus base

Oseledets/Examples/CatMapToral.lean proves the genuine Arnold cat map catTorus : 𝕋² → 𝕋² is ergodic for Haar (Oseledets.CatMapToral.ergodic_catTorus). We realize the cat-map matrix catℝ as a constant cocycle over this ergodic base and read off the spectrum log((3 ± √5)/2), with top exponent log((3 + √5)/2) > 0 (catTorus_constCocycle_topExponent_pos). This strictly improves the doubling-map version: the base is now the genuine hyperbolic toral automorphism.

Grade 2a — the genuine derivative of the cat map's linear lift

The Arnold cat map lifts to the universal cover ℝ² as the genuine ℝ-linear map catLift with matrix catℝ (acting through Matrix.toEuclideanCLM). The Fréchet derivative of a continuous linear map is the map itself (ContinuousLinearMap.fderiv), so the repo's derivative cocycle of catLift is the constant matrix catℝ at every point (derivativeCocycle_catLift). Hence derivativeCocycle catLift is — in the repo's exact DerivativeCocycle framework — the genuine tangent cocycle of the cat map's linear lift, and it equals the constant catℝ. Combining with Grade 1, the top Lyapunov exponent of this genuine derivative cocycle, realized over the genuine ergodic base catTorus, is log((3 + √5)/2) > 0 (catLift_derivativeCocycle_topExponent_pos). This is fully honest: catLift is the genuine ℝ²-linear lift of the cat map to the universal cover, and derivativeCocycle is the repo's genuine Fréchet-derivative cocycle.

Grade 2b — the manifold mfderiv reading (documented gap)

A third, strictly stronger route would read the derivative directly on the torus manifold: prove mfderiv of catTorus, in the standard AddCircle charts, equals catℝ. Mathlib provides the charted/smooth-manifold structure on AddCircle but has no mfderiv API for AddCircle endomorphisms (no lemma computing the manifold derivative of n • · or of an AddMonoidHom of a product of circles in terms of its matrix). Supplying that API is a genuine Mathlib-scale task orthogonal to the Oseledets development, so we do not pursue 2b here; the universal-cover lift (Grade 2a) is the honest derivative-cocycle deliverable, since the cat map and its lift have the same derivative everywhere (the covering projection ℝ² → 𝕋² is a local diffeomorphism with identity derivative).

Main results

• Oseledets.CatMapToral.catTorus_constCocycle_exponents — the two Lyapunov exponents of the constant cocycle catℝ over the genuine ergodic base catTorus are log((3 ± √5)/2).
• Oseledets.CatMapToral.catTorus_constCocycle_topExponent_pos — its top exponent is log((3 + √5)/2) > 0.
• Oseledets.CatMapToral.catLift — the genuine ℝ²-linear lift of the cat map to the universal cover, with matrix catℝ.
• Oseledets.CatMapToral.derivativeCocycle_catLift — the repo's derivative cocycle of catLift is the constant matrix catℝ at every point.
• Oseledets.CatMapToral.catLift_derivativeCocycle_topExponent_pos — the top Lyapunov exponent of the genuine derivative cocycle of catLift, over the genuine ergodic base catTorus, is log((3 + √5)/2) > 0.

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

@[implicit_reducible]

noncomputable def instMeasureSpaceUnitAddCircle_oseledets_1 : MeasureTheory.MeasureSpace UnitAddCircle

Normalise the circle measure to total mass 1 (AddCircle.haarAddCircle), matching the MeasureSpace UnitAddCircle convention of Oseledets/Examples/CatMapToral.lean so that the ambient volume : Measure T2 here is the same product Haar probability measure for which ergodic_catTorus is stated.

Equations

• instMeasureSpaceUnitAddCircle_oseledets_1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem instIsAddHaarMeasureUnitAddCircleVolume_oseledets_1 : MeasureTheory.volume.IsAddHaarMeasure

theorem instIsProbabilityMeasureUnitAddCircleVolume_oseledets_1 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The real cat-map matrix coincides with Elementary's catMapGen

theorem Oseledets.CatMapToral.catℝ_eq_catMapGen : catℝ = catMapGen

The real cat-map matrix catℝ = !![2,1;1,1] is literally Elementary's catMapGen.

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

catℝ is symmetric (inherited from catMapGen).

theorem Oseledets.CatMapToral.catℝ_posSemidef : catℝ.PosSemidef

catℝ is positive semidefinite (inherited from catMapGen).

theorem Oseledets.CatMapToral.catℝ_det_ne_zero : catℝ.det ≠ 0

det catℝ = 1 ≠ 0 (inherited from catMapGen).

theorem Oseledets.CatMapToral.catℝ_isHermitian : catℝ.IsHermitian

The Hermitian witness for catℝ, reused from catMapGen.

Grade 1 — the constant cat-map cocycle over the genuine ergodic torus base

theorem Oseledets.CatMapToral.catTorus_constCocycle_exponents : exponents ergodic_catTorus ⋯ ⋯ ⋯ ⋯ ⟨0, ⋯⟩ = Real.log ((3 + √5) / 2) ∧ exponents ergodic_catTorus ⋯ ⋯ ⋯ ⋯ ⟨1, ⋯⟩ = Real.log ((3 - √5) / 2)

Grade 1. The cat-map Lyapunov spectrum over the genuine ergodic base. Realized as a constant cocycle with generator catℝ = !![2,1;1,1] over the genuine ergodic Arnold cat map catTorus : 𝕋² → 𝕋² (ergodic_catTorus), the two Lyapunov exponents are log((3 + √5)/2) and log((3 - √5)/2) — the logs of the eigenvalues of the cat-map matrix.

Unlike Oseledets.catMapMatrix_exponents, the base here is the genuine hyperbolic toral automorphism, not the doubling map.

theorem Oseledets.CatMapToral.catTorus_constCocycle_topExponent_pos : 0 < topExponent ergodic_catTorus ⋯ ⋯ ⋯ ⋯

Grade 1 (headline). The top Lyapunov exponent over the genuine ergodic base is positive. The top Lyapunov exponent of the constant cat-map cocycle catℝ over the genuine ergodic Arnold cat map catTorus is log((3 + √5)/2) > 0. Positivity is the hyperbolicity of the cat map: (3 + √5)/2 > 1.

Grade 2a — the genuine derivative cocycle of the cat map's linear lift

noncomputable def Oseledets.CatMapToral.catLift : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

The universal-cover lift of the Arnold cat map. The cat map catTorus : 𝕋² → 𝕋² lifts to the universal cover ℝ² = EuclideanSpace ℝ (Fin 2) as the genuine ℝ-linear map with matrix catℝ, acting through the star-algebra equivalence Matrix.toEuclideanCLM. The covering projection ℝ² → 𝕋² intertwines catLift with catTorus, and is a local diffeomorphism with identity derivative, so catLift and catTorus have the same derivative everywhere.

Equations

• Oseledets.CatMapToral.catLift = ⇑(Matrix.toEuclideanCLM Oseledets.CatMapToral.catℝ)

theorem Oseledets.CatMapToral.fderiv_catLift (x : EuclideanSpace ℝ (Fin 2)) : fderiv ℝ catLift x = Matrix.toEuclideanCLM catℝ

catLift is the coercion of the continuous linear map toEuclideanCLM catℝ, hence its Fréchet derivative at every point is that very map: fderiv ℝ catLift x = toEuclideanCLM catℝ.

theorem Oseledets.CatMapToral.differentiable_catLift : Differentiable ℝ catLift

catLift is differentiable (it is a continuous linear map).

@[simp]

theorem Oseledets.CatMapToral.derivativeCocycle_catLift (x : EuclideanSpace ℝ (Fin 2)) : derivativeCocycle catLift x = catℝ

Grade 2a. The repo's derivative cocycle of catLift is the constant matrix catℝ. Since catLift is a continuous linear map, its Fréchet derivative at every point is itself (fderiv_catLift); transporting back along toEuclideanCLM.symm recovers the matrix catℝ. So the genuine tangent cocycle of the cat map's linear lift, in the repo's exact DerivativeCocycle framework, is the constant generator catℝ.

theorem Oseledets.CatMapToral.derivativeCocycle_catLift_eq_const : derivativeCocycle catLift = fun (x : EuclideanSpace ℝ (Fin 2)) => catℝ

The derivative cocycle of catLift is the constant generator fun _ => catℝ.

theorem Oseledets.CatMapToral.derivativeCocycle_catLift_det_ne_zero : (derivativeCocycle catLift 0).det ≠ 0

The determinant of the constant derivative-cocycle generator derivativeCocycle catLift 0 is nonzero (it equals catℝ, whose determinant is 1).

theorem Oseledets.CatMapToral.catLift_derivativeCocycle_topExponent_pos : 0 < topExponent ergodic_catTorus ⋯ ⋯ ⋯ ⋯

Grade 2a (headline). The genuine derivative cocycle of the cat map's lift has positive top exponent over the genuine ergodic base. The derivative cocycle of catLift is the constant matrix catℝ (derivativeCocycle_catLift). Realized as a constant cocycle over the genuine ergodic Arnold cat map catTorus, the top Lyapunov exponent of this genuine derivative cocycle is the same constant-cocycle top exponent as in Grade 1, namely log((3 + √5)/2) > 0.

This closes the EuclideanSpace ↔ torus adapter gap: the generator is no longer a bare constant matrix — it is the genuine Fréchet derivative derivativeCocycle catLift of the cat map's ℝ²-linear lift to the universal cover (the repo's DerivativeCocycle.derivativeCocycle), evaluated as a constant cocycle over the genuine hyperbolic toral automorphism, and its top Lyapunov exponent is positive.