Hyperbolic toral automorphisms have return growth: the criterion by the trace

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #178 (out of #19 and #177).

For an integer matrix B ∈ SL₂(ℤ) with |tr B| > 2, the toral automorphism toral B of T² has return growth log ρ, ρ = (|tr B| + √(tr B² − 4)) / 2 > 1 its spectral radius (★★★ hasReturnGrowth_toral). The whole statement is read off one integer, the trace. Three facts replace #176's Fibonacci-specific steps:

• the kernel of a toral endomorphism toral C with det C ≠ 0 has exactly |det C| points (★★★ card_ker_toral): #176's parametrisation m ↦ (1/det C)·adj(C)·m mod ℤ² with the 2 × 2 adjugate written out, and Mathlib's Submodule.natAbs_det_basis_change for the lattice index;
• det(M − 1) = det M − tr M + 1 for 2 × 2 matrices, so the fixed points of toral Bᵗ are |2 − tr Bᵗ| in number (★★ card_fixedPoints_toral_pow);
• Cayley–Hamilton B² = (tr B)·B − (det B)·1 gives the trace recurrence tr Bᵗ⁺² = tr B · tr Bᵗ⁺¹ − tr Bᵗ, solved in closed form by εᵗ(ρᵗ + ρ⁻ᵗ) with ε = ±1 the sign of the trace (★★ trace_pow_eq); tr Bᵗ = 2 would force ρᵗ = 1, impossible, so every return set is finite and nonempty, and (1 − ρ⁻¹)² ρᵗ ≤ #Fix ≤ 4 ρᵗ squeezes the growth to log ρ.

The cat matrix is the instance tr = 3, ρ = φ², recovering #176's 2 log φ (cat_eq_toral, spectralRadius_catMat).

Honest scope

• det B = 1 throughout; det B = −1 (orientation-reversing automorphisms) would need det(Bᵗ − 1) = (−1)ᵗ − tr Bᵗ + 1 and is not treated.
• The converse — |tr B| ≤ 2 never has return growth — is #179.
• The sign of the trace is carried by ε = ±1 and never split on: |εᵗ(ρᵗ + ρ⁻ᵗ)| = ρᵗ + ρ⁻ᵗ.

References: Katok–Hasselblatt, Introduction to the Modern Theory of Dynamical Systems, §1.8, §3.2; Mathlib/Dynamics/CatMapPeriodicPoints.lean (#176, the cat-matrix case this generalises), Mathlib/Dynamics/ReturnCriterion.lean (#177, HasReturnGrowth); specs/BACKLOG.md #178, #19.

Toral endomorphisms

noncomputable def MeasureTheory.toral (B : Matrix (Fin 2) (Fin 2) ℤ) (p : Torus2) : Torus2

The toral endomorphism of an integer 2 × 2 matrix.

Equations

• MeasureTheory.toral B p = (B 0 0 • p.1 + B 0 1 • p.2, B 1 0 • p.1 + B 1 1 • p.2)

theorem MeasureTheory.toral_one_apply (p : Torus2) : toral 1 p = p

theorem MeasureTheory.toral_mul (B C : Matrix (Fin 2) (Fin 2) ℤ) : toral (B * C) = toral B ∘ toral C

theorem MeasureTheory.toral_pow (B : Matrix (Fin 2) (Fin 2) ℤ) (t : ℕ) : (toral B)^[t] = toral (B ^ t)

theorem MeasureTheory.toral_sub (B C : Matrix (Fin 2) (Fin 2) ℤ) (p : Torus2) : toral (B - C) p = toral B p - toral C p

theorem MeasureTheory.toral_fixed_iff (B : Matrix (Fin 2) (Fin 2) ℤ) (p : Torus2) : toral B p = p ↔ toral (B - 1) p = 0

Fixed points of toral B are the kernel of toral (B − 1).

The real matrix, its adjugate, and the descent

noncomputable def MeasureTheory.realMat (C : Matrix (Fin 2) (Fin 2) ℤ) (v : ℝ × ℝ) : ℝ × ℝ

The matrix acting on the plane.

Equations

• MeasureTheory.realMat C v = (↑(C 0 0) * v.1 + ↑(C 0 1) * v.2, ↑(C 1 0) * v.1 + ↑(C 1 1) * v.2)

noncomputable def MeasureTheory.adjMat (C : Matrix (Fin 2) (Fin 2) ℤ) (w : ℝ × ℝ) : ℝ × ℝ

The adjugate acting on the plane.

Equations

• MeasureTheory.adjMat C w = (↑(C 1 1) * w.1 - ↑(C 0 1) * w.2, -↑(C 1 0) * w.1 + ↑(C 0 0) * w.2)

theorem MeasureTheory.det_cast (C : Matrix (Fin 2) (Fin 2) ℤ) : ↑C.det = ↑(C 0 0) * ↑(C 1 1) - ↑(C 0 1) * ↑(C 1 0)

theorem MeasureTheory.adjMat_realMat (C : Matrix (Fin 2) (Fin 2) ℤ) (v : ℝ × ℝ) : adjMat C (realMat C v) = ↑C.det • v

theorem MeasureTheory.realMat_adjMat (C : Matrix (Fin 2) (Fin 2) ℤ) (w : ℝ × ℝ) : realMat C (adjMat C w) = ↑C.det • w

theorem MeasureTheory.realMat_smul (C : Matrix (Fin 2) (Fin 2) ℤ) (c : ℝ) (v : ℝ × ℝ) : realMat C (c • v) = c • realMat C v

theorem MeasureTheory.adjMat_add (C : Matrix (Fin 2) (Fin 2) ℤ) (v w : ℝ × ℝ) : adjMat C (v + w) = adjMat C v + adjMat C w

theorem MeasureTheory.realMat_intCast (C : Matrix (Fin 2) (Fin 2) ℤ) (k : Fin 2 → ℤ) : realMat C (↑(k 0), ↑(k 1)) = (↑((Matrix.toLin' C) k 0), ↑((Matrix.toLin' C) k 1))

On integer vectors realMat is Matrix.toLin' C.

theorem MeasureTheory.toral_coe (B : Matrix (Fin 2) (Fin 2) ℤ) (x y : ℝ) : toral B (↑x, ↑y) = (↑(realMat B (x, y)).1, ↑(realMat B (x, y)).2)

toral B descends from realMat B.

The kernel of a toral endomorphism has |det| points

theorem MeasureTheory.toLin'_injective_of_det_ne_zero (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) : Function.Injective ⇑(Matrix.toLin' C)

toLin' C is injective on ℤ² when det C ≠ 0: multiply by the adjugate.

noncomputable def MeasureTheory.kerVec (C : Matrix (Fin 2) (Fin 2) ℤ) (m : Fin 2 → ℤ) : ℝ × ℝ

The real lift of the kernel point attached to m ∈ ℤ²: C⁻¹ m.

Equations

• MeasureTheory.kerVec C m = (↑C.det)⁻¹ • MeasureTheory.adjMat C (↑(m 0), ↑(m 1))

theorem MeasureTheory.realMat_kerVec (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) (m : Fin 2 → ℤ) : realMat C (kerVec C m) = (↑(m 0), ↑(m 1))

theorem MeasureTheory.kerVec_add (C : Matrix (Fin 2) (Fin 2) ℤ) (m n : Fin 2 → ℤ) : kerVec C (m + n) = kerVec C m + kerVec C n

noncomputable def MeasureTheory.kerLift (C : Matrix (Fin 2) (Fin 2) ℤ) : (Fin 2 → ℤ) →+ Torus2

ℤ² → T², m ↦ C⁻¹ m mod ℤ²: the parametrisation of the kernel.

Equations

• MeasureTheory.kerLift C = AddMonoidHom.mk' (fun (m : Fin 2 → ℤ) => (↑(MeasureTheory.kerVec C m).1, ↑(MeasureTheory.kerVec C m).2)) ⋯

theorem MeasureTheory.kerLift_apply (C : Matrix (Fin 2) (Fin 2) ℤ) (m : Fin 2 → ℤ) : (kerLift C) m = (↑(kerVec C m).1, ↑(kerVec C m).2)

theorem MeasureTheory.kerLift_mem (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) (m : Fin 2 → ℤ) : toral C ((kerLift C) m) = 0

theorem MeasureTheory.kerLift_surjective (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) (p : Torus2) (hp : toral C p = 0) : ∃ (m : Fin 2 → ℤ), (kerLift C) m = p

theorem MeasureTheory.kerLift_eq_zero_iff (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) (m : Fin 2 → ℤ) : (kerLift C) m = 0 ↔ m ∈ (Matrix.toLin' C).range

theorem MeasureTheory.card_ker_toral (C : Matrix (Fin 2) (Fin 2) ℤ) (hC : C.det ≠ 0) : Nat.card { p : Torus2 // toral C p = 0 } = C.det.natAbs

★★★ The kernel of a toral endomorphism has |det C| points: it is ℤ² / Cℤ².

Fixed points of a power

theorem MeasureTheory.det_sub_one_fin_two (M : Matrix (Fin 2) (Fin 2) ℤ) : (M - 1).det = M.det - M.trace + 1

det(M − 1) = det M − tr M + 1 for 2 × 2 matrices.

theorem MeasureTheory.card_fixedPoints_toral (M : Matrix (Fin 2) (Fin 2) ℤ) (hM : (M - 1).det ≠ 0) : Nat.card { p : Torus2 // toral M p = p } = (M - 1).det.natAbs

★★ The fixed points of toral (Bᵗ) are |det(Bᵗ − 1)| = |2 − tr Bᵗ| in number, when nonzero.

Cayley–Hamilton and the trace recurrence

theorem MeasureTheory.cayley_hamilton_fin_two (M : Matrix (Fin 2) (Fin 2) ℤ) : M ^ 2 = M.trace • M - M.det • 1

Cayley–Hamilton for 2 × 2 integer matrices.

theorem MeasureTheory.trace_pow_add_two (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1) (t : ℕ) : (B ^ (t + 2)).trace = B.trace * (B ^ (t + 1)).trace - (B ^ t).trace

The trace recurrence tr Bᵗ⁺² = tr B · tr Bᵗ⁺¹ − tr Bᵗ when det B = 1.

The spectral radius and the closed form of the trace

noncomputable def MeasureTheory.spectralRadius (B : Matrix (Fin 2) (Fin 2) ℤ) : ℝ

The spectral radius of a hyperbolic element of SL₂(ℤ): (|tr B| + √(tr B² − 4)) / 2.

Equations

• MeasureTheory.spectralRadius B = (|↑B.trace| + √(↑B.trace ^ 2 - 4)) / 2

theorem MeasureTheory.one_lt_spectralRadius (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) : 1 < spectralRadius B

theorem MeasureTheory.spectralRadius_add_inv (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) : spectralRadius B + (spectralRadius B)⁻¹ = |↑B.trace|

ρ · ρ' = 1 with ρ' = (|tr B| − √(tr B² − 4)) / 2, so ρ⁻¹ = ρ' and ρ + ρ⁻¹ = |tr B|.

noncomputable def MeasureTheory.traceSign (B : Matrix (Fin 2) (Fin 2) ℤ) : ℝ

The sign of the trace.

Equations

• MeasureTheory.traceSign B = if 0 ≤ ↑B.trace then 1 else -1

theorem MeasureTheory.traceSign_sq (B : Matrix (Fin 2) (Fin 2) ℤ) : traceSign B ^ 2 = 1

theorem MeasureTheory.traceSign_mul_abs (B : Matrix (Fin 2) (Fin 2) ℤ) : traceSign B * |↑B.trace| = ↑B.trace

theorem MeasureTheory.abs_traceSign_pow (B : Matrix (Fin 2) (Fin 2) ℤ) (t : ℕ) : |traceSign B ^ t| = 1

theorem MeasureTheory.trace_pow_eq (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) (t : ℕ) : ↑(B ^ t).trace = traceSign B ^ t * (spectralRadius B ^ t + (spectralRadius B)⁻¹ ^ t)

★★ The closed form of the trace: tr Bᵗ = εᵗ (ρᵗ + ρ⁻ᵗ).

Every return set is finite and nonempty

theorem MeasureTheory.det_pow_sub_one (B : Matrix (Fin 2) (Fin 2) ℤ) (hdet : B.det = 1) (t : ℕ) : (B ^ t - 1).det = 2 - (B ^ t).trace

det(Bᵗ − 1) = 2 − tr Bᵗ when det B = 1.

theorem MeasureTheory.trace_pow_ne_two (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) (s : ℕ) : (B ^ (s + 1)).trace ≠ 2

tr Bᵗ ≠ 2 for t ≥ 1: it would force ρᵗ = 1.

theorem MeasureTheory.det_pow_sub_one_ne_zero (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) (s : ℕ) : (B ^ (s + 1) - 1).det ≠ 0

theorem MeasureTheory.card_fixedPoints_toral_pow (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) (s : ℕ) : Nat.card { p : Torus2 // toral (B ^ (s + 1)) p = p } = (2 - (B ^ (s + 1)).trace).natAbs

★★ The fixed points of toral Bᵗ are |2 − tr Bᵗ| in number (t ≥ 1).

theorem MeasureTheory.card_fixedPoints_toral_pow_real (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) (s : ℕ) : ↑(Nat.card { p : Torus2 // toral (B ^ (s + 1)) p = p }) = |2 - traceSign B ^ (s + 1) * (spectralRadius B ^ (s + 1) + (spectralRadius B)⁻¹ ^ (s + 1))|

The count in closed form: |2 − εᵗ (ρᵗ + ρ⁻ᵗ)|.

The return growth is log ρ

theorem MeasureTheory.hasReturnGrowth_toral (B : Matrix (Fin 2) (Fin 2) ℤ) (hτ : 2 < |↑B.trace|) (hdet : B.det = 1) : HasReturnGrowth (toral B) (Real.log (spectralRadius B))

★★★ A hyperbolic toral automorphism has return growth log ρ, ρ its spectral radius.

The cat map as the instance tr = 3

theorem MeasureTheory.cat_eq_toral : cat = toral !![2, 1; 1, 1]

theorem MeasureTheory.trace_catMat : !![2, 1; 1, 1].trace = 3

theorem MeasureTheory.det_catMat : !![2, 1; 1, 1].det = 1

theorem MeasureTheory.spectralRadius_catMat : spectralRadius !![2, 1; 1, 1] = Real.goldenRatio ^ 2

The spectral radius of the cat matrix is φ².

theorem MeasureTheory.log_spectralRadius_catMat : Real.log (spectralRadius !![2, 1; 1, 1]) = 2 * Real.log Real.goldenRatio

#176's exponent recovered: log φ² = 2 log φ.

theorem MeasureTheory.cat_hasReturnGrowth' : HasReturnGrowth cat (Real.log (spectralRadius !![2, 1; 1, 1]))

The cat map has return growth log φ², now as an instance of the general theorem.