The cat map is two transverse shears, and neither shear stretches on its own

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #153; consumed by SigmaLayer/FibreTwoShears.lean.

Arnold's cat map (x, y) ↦ (2x + y, x + y) factors as the vertical shear shearY : (x, y) ↦ (x, x + y) followed by the horizontal shear shearX : (x, y) ↦ (x + y, y) (cat_eq_shearX_comp_shearY). Each factor is a continuous automorphism of T², so each preserves Haar measure (measurePreserving_shearX, measurePreserving_shearY), and each lifts to a unipotent linear map of the plane preserving the area form u₁v₂ − u₂v₁ (shearXR_area, shearYR_area): the factors are symplectic.

The point of the factoring is the Lyapunov exponents. A unipotent shear moves a vector by at most a linear amount in the iterate count — (shearXR ^ n) v = (v₁ + n v₂, v₂) (shearXR_pow_apply) — so its exponent is 0 in every direction (hasLyapunovExponent_shearXR, hasLyapunovExponent_shearYR), while the composition catR = shearXR ∘ shearYR (catR_eq_shearXR_comp_shearYR) has exponent 2 log φ off its stable line (hasLyapunovExponent_catR). ★★★ cat_two_shears states the whole package: hyperbolicity is produced by the transversality of the two shears, not by either shear. A shear along one coordinate, however often repeated, stretches nothing exponentially.

The general lemma behind the exponents, hasLyapunovExponent_zero_of_linear_growth, is stated for any continuous linear map of a real normed space: a direction bounded below and growing at most linearly has exponent 0. It is the sub-exponential sibling of hasLyapunovExponent_of_geometric_bounds.

Honest scope

• The shears here are the linear toral automorphisms [[1,1],[0,1]] and [[1,0],[1,1]]. They are not time-one maps of vector fields on T²: the plane flow (x, y) ↦ (x, y + t x) descends to the torus only at integer t. So nothing here is a flow, and the flux obstruction for translation fields on the torus (LF4/ArenaStrokeFlux.lean) is a statement about a different kind of map.
• log ‖0‖ = 0 in Lean, so the zero direction has exponent 0 trivially; the shear theorems hold for every direction, zero included, which is why no nonvanishing hypothesis appears.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8; Mathlib/Dynamics/CatMapWitness.lean (cat, catHom, measurePreserving_cat), Mathlib/Dynamics/LyapunovExponent.lean (HasLyapunovExponent, catR, hasLyapunovExponent_catR); specs/BACKLOG.md #153, #19, #148.

Exponent zero from linear growth

theorem tendsto_log_natCast_add_one_div : Filter.Tendsto (fun (n : ℕ) => Real.log (↑n + 1) / ↑n) Filter.atTop (nhds 0)

log (n + 1) / n → 0.

theorem hasLyapunovExponent_zero_of_linear_growth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : E →L[ℝ] E) (v : E) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hlow : ∀ (n : ℕ), a ≤ ‖(A ^ n) v‖) (hup : ∀ (n : ℕ), ‖(A ^ n) v‖ ≤ b * (↑n + 1)) : HasLyapunovExponent A v 0

Exponent zero from linear growth: a direction bounded away from zero whose iterates grow at most linearly in the iterate count has Lyapunov exponent 0.

The two shears on the torus

noncomputable def MeasureTheory.shearX : Torus2 → Torus2

The horizontal shear (x, y) ↦ (x + y, y) on T²: the first coordinate is translated by the second.

Equations

• MeasureTheory.shearX p = (p.1 + p.2, p.2)

noncomputable def MeasureTheory.shearY : Torus2 → Torus2

The vertical shear (x, y) ↦ (x, x + y) on T²: the second coordinate is translated by the first.

Equations

• MeasureTheory.shearY p = (p.1, p.1 + p.2)

theorem MeasureTheory.cat_eq_shearX_comp_shearY : cat = shearX ∘ shearY

★ The cat map is the vertical shear followed by the horizontal one.

theorem MeasureTheory.shearX_add (a b : Torus2) : shearX (a + b) = shearX a + shearX b

theorem MeasureTheory.shearY_add (a b : Torus2) : shearY (a + b) = shearY a + shearY b

noncomputable def MeasureTheory.shearXHom : Torus2 →+ Torus2

The horizontal shear as an additive monoid hom.

Equations

• MeasureTheory.shearXHom = AddMonoidHom.mk' MeasureTheory.shearX MeasureTheory.shearX_add

noncomputable def MeasureTheory.shearYHom : Torus2 →+ Torus2

The vertical shear as an additive monoid hom.

Equations

• MeasureTheory.shearYHom = AddMonoidHom.mk' MeasureTheory.shearY MeasureTheory.shearY_add

theorem MeasureTheory.continuous_shearX : Continuous shearX

theorem MeasureTheory.continuous_shearY : Continuous shearY

noncomputable def MeasureTheory.shearXInv : Torus2 → Torus2

The inverse horizontal shear (x, y) ↦ (x − y, y).

Equations

• MeasureTheory.shearXInv q = (q.1 - q.2, q.2)

noncomputable def MeasureTheory.shearYInv : Torus2 → Torus2

The inverse vertical shear (x, y) ↦ (x, y − x).

Equations

• MeasureTheory.shearYInv q = (q.1, q.2 - q.1)

theorem MeasureTheory.shearX_shearXInv (q : Torus2) : shearX (shearXInv q) = q

theorem MeasureTheory.shearXInv_shearX (p : Torus2) : shearXInv (shearX p) = p

theorem MeasureTheory.shearY_shearYInv (q : Torus2) : shearY (shearYInv q) = q

theorem MeasureTheory.shearYInv_shearY (p : Torus2) : shearYInv (shearY p) = p

theorem MeasureTheory.surjective_shearX : Function.Surjective shearX

theorem MeasureTheory.surjective_shearY : Function.Surjective shearY

theorem MeasureTheory.bijective_shearX : Function.Bijective shearX

Each shear is a bijection of the torus.

theorem MeasureTheory.bijective_shearY : Function.Bijective shearY

theorem MeasureTheory.measurePreserving_shearX : MeasurePreserving shearX volume volume

★ Each shear preserves Haar measure — a continuous surjective endomorphism of a compact group does.

theorem MeasureTheory.measurePreserving_shearY : MeasurePreserving shearY volume volume

The linear lifts

noncomputable def MeasureTheory.shearXR : ℝ × ℝ →L[ℝ] ℝ × ℝ

The horizontal shear [[1,1],[0,1]] of the plane: the lift of shearX.

Equations

• MeasureTheory.shearXR = (ContinuousLinearMap.fst ℝ ℝ ℝ + ContinuousLinearMap.snd ℝ ℝ ℝ).prod (ContinuousLinearMap.snd ℝ ℝ ℝ)

noncomputable def MeasureTheory.shearYR : ℝ × ℝ →L[ℝ] ℝ × ℝ

The vertical shear [[1,0],[1,1]] of the plane: the lift of shearY.

Equations

• MeasureTheory.shearYR = (ContinuousLinearMap.fst ℝ ℝ ℝ).prod (ContinuousLinearMap.fst ℝ ℝ ℝ + ContinuousLinearMap.snd ℝ ℝ ℝ)

@[simp]

theorem MeasureTheory.shearXR_apply (v : ℝ × ℝ) : shearXR v = (v.1 + v.2, v.2)

@[simp]

theorem MeasureTheory.shearYR_apply (v : ℝ × ℝ) : shearYR v = (v.1, v.1 + v.2)

theorem MeasureTheory.shearX_coe (x y : ℝ) : shearX (↑x, ↑y) = (↑(shearXR (x, y)).1, ↑(shearXR (x, y)).2)

shearX is shearXR read modulo ℤ².

theorem MeasureTheory.shearY_coe (x y : ℝ) : shearY (↑x, ↑y) = (↑(shearYR (x, y)).1, ↑(shearYR (x, y)).2)

shearY is shearYR read modulo ℤ².

theorem MeasureTheory.catR_eq_shearXR_comp_shearYR : catR = shearXR ∘SL shearYR

★ The cat matrix is the product of the two shear matrices.

The shears are symplectic

theorem MeasureTheory.shearXR_area (u v : ℝ × ℝ) : (shearXR u).1 * (shearXR v).2 - (shearXR u).2 * (shearXR v).1 = u.1 * v.2 - u.2 * v.1

The horizontal shear preserves the area form u₁v₂ − u₂v₁.

theorem MeasureTheory.shearYR_area (u v : ℝ × ℝ) : (shearYR u).1 * (shearYR v).2 - (shearYR u).2 * (shearYR v).1 = u.1 * v.2 - u.2 * v.1

The vertical shear preserves the area form u₁v₂ − u₂v₁.

theorem MeasureTheory.catR_area (u v : ℝ × ℝ) : (catR u).1 * (catR v).2 - (catR u).2 * (catR v).1 = u.1 * v.2 - u.2 * v.1

The cat matrix preserves the area form — as the composition of two maps that do.

Neither shear stretches

theorem MeasureTheory.shearXR_pow_apply (n : ℕ) (v : ℝ × ℝ) : (shearXR ^ n) v = (v.1 + ↑n * v.2, v.2)

The iterates of the horizontal shear: (x, y) ↦ (x + n y, y).

theorem MeasureTheory.shearYR_pow_apply (n : ℕ) (v : ℝ × ℝ) : (shearYR ^ n) v = (v.1, ↑n * v.1 + v.2)

The iterates of the vertical shear: (x, y) ↦ (x, n x + y).

theorem MeasureTheory.norm_shear_pair_le (x y : ℝ) (n : ℕ) : ‖(x + ↑n * y, y)‖ ≤ ‖(x, y)‖ * (↑n + 1)

A pair whose first entry is x + n y has norm at most (n + 1) times the norm of (x, y).

theorem MeasureTheory.norm_shear_pair_le' (x y : ℝ) (n : ℕ) : ‖(x, ↑n * x + y)‖ ≤ ‖(x, y)‖ * (↑n + 1)

The vertical twin: a pair whose second entry is n x + y has norm at most (n + 1) times the norm of (x, y).

theorem MeasureTheory.hasLyapunovExponent_shearXR (v : ℝ × ℝ) : HasLyapunovExponent shearXR v 0

★★ The horizontal shear has Lyapunov exponent 0 in every direction.

theorem MeasureTheory.hasLyapunovExponent_shearYR (v : ℝ × ℝ) : HasLyapunovExponent shearYR v 0

★★ The vertical shear has Lyapunov exponent 0 in every direction.

★★★ The package

theorem MeasureTheory.cat_two_shears : cat = shearX ∘ shearY ∧ MeasurePreserving shearX volume volume ∧ MeasurePreserving shearY volume volume ∧ catR = shearXR ∘SL shearYR ∧ (∀ (v : ℝ × ℝ), HasLyapunovExponent shearXR v 0) ∧ (∀ (v : ℝ × ℝ), HasLyapunovExponent shearYR v 0) ∧ ∀ (v : ℝ × ℝ), ellUR v ≠ 0 → HasLyapunovExponent catR v (2 * Real.log Real.goldenRatio)

★★★ The cat map is two transverse shears, and the stretching belongs to neither. The cat map is the vertical shear followed by the horizontal one; each shear preserves Haar measure; the lift of each shear has Lyapunov exponent 0 in every direction; and their composition catR has exponent 2 log φ in every direction off the stable line. Hyperbolicity is the work of the transversality, not of either factor.