An invertible correlation-decay witness: Arnold's cat map on T²

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

CorrelationDecayWitness.lean shows HasCorrelationDecay is satisfiable, using the doubling endomorphism on the circle. That witness is not invertible, and the gap is load-bearing for its consumer: a symplectic Σ-flow would be invertible, so a non-invertible witness shows the predicate is inhabited without showing it is inhabited by anything of the right kind (LF4/KahlerFibreMixing.lean, honest-scope caveat (2)).

This file supplies the invertible witness: Arnold's cat map (x,y) ↦ (2x+y, x+y) on T² = (ℝ/ℤ)², a bijection, with the observable catObs (x,y) = Re e^{2πix}.

Why the doubling map's proof does not transfer

CorrelationDecayWitness uses no Fourier analysis: it rotates by 2^{-(s+1)}, which flips the s-factor's sign and fixes the later factors because 2^t / 2^{s+1} is an integer. That trick needs the map to kill a torsion point, and a bijection cannot: A^t ρ = 0 ⟹ ρ = 0. So the argument here is the standard character-orthogonality one instead, which the doubling witness deliberately avoided.

The construction

• cat is an AddMonoidHom (catHom), continuous and surjective, so it preserves Haar measure — measurePreserving_cat, from AddMonoidHom.measurePreserving. ⚠️ This is the step MATHLIB-GAPS.md recorded as the missing piece ("Haar invariance of a toral automorphism, which Mathlib does not provide"); that row was factually wrong and is corrected — the lemma is upstream, it is the to_additive twin of MonoidHom.measurePreserving.
• Characters chi (m,n) (x,y) = e^{2πimx} e^{2πiny} transport by the transpose catZ (m,n) = (2m+n, m+n) (chi_cat), so a correlation at lag u is an integral of characters indexed by catZ^[u].
• A nontrivial character integrates to zero (integral_chi_eq_zero), by translating to a point where it takes the value -1 (fourier_add_half_inv_index).
• The orbit catZ^[u] (1,0) has both coordinates ≥ 1 for u ≥ 1 (catZ_orbit_pos, a two-line omega induction on the Fibonacci-positive recursion), so it is never ±(1,0) — which is exactly the non-degeneracy the four-term expansion needs.

Honest scope

• This is a witness, not a theorem about Σ. It shows HasCorrelationDecay is inhabited by an invertible measure-preserving map; it does not show any Σ-flow is one. That separation is the same one CorrelationDecayWitness states, and not_hasCorrelationDecay_of_compactGroup still rules out the flows generated by a compact group.
• Not ergodicity, and not mixing in general. Only the single observable catObs is treated. Ergodic cat would need decay for every character (so catZ^[u] v ≠ v for arbitrary v ≠ 0, a genuine eigenvalue argument) plus L²-density of characters on T²; Mathlib's torus ergodicity is one-dimensional (AddCircle.ergodic_zsmul) and it has no definition of mixing at all. Not attempted here.
• The concrete matrix only. [[2,1],[1,1]] on the binary product, not a general hyperbolic A ∈ GL_n(ℤ); the general case needs Matrix.toLin on Fin n → AddCircle 1 and "no eigenvalue is a root of unity", which is a different and larger job.
• ⚠️ Q12-d's mixing formulation was retired as mis-specified (2026-08-24), so this unblocks no live frontier item. What it does is discharge the invertibility caveat: the obstruction to a Σ-flow witness is the choice of map, not the ontic space.

Reference: Arnold–Avez, Ergodic Problems of Classical Mechanics (1968), §1.16 (the cat map). In-corpus: Mathlib/Dynamics/CorrelationDecay.lean (the engine), CorrelationDecayWitness.lean (the non-invertible sibling), CompactGroupNoMixing.lean (what any witness must dodge).

The torus and its Haar measure

@[reducible, inline]

abbrev MeasureTheory.Torus2 : Type

The two-torus (ℝ ⧸ ℤ)². ⚠️ Deliberately does not re-declare a Circ abbreviation: CorrelationDecayWitness.lean already has one in this namespace, and two would collide.

Equations

• MeasureTheory.Torus2 = (AddCircle 1 × AddCircle 1)

instance MeasureTheory.instProbAddCircleOne : IsProbabilityMeasure volume

instance MeasureTheory.instProbTorus2 : IsProbabilityMeasure volume

instance MeasureTheory.instHaarTorus2 : volume.IsAddHaarMeasure

The cat map

noncomputable def MeasureTheory.cat : Torus2 → Torus2

Arnold's cat map (x,y) ↦ (2x + y, x + y) on T².

Equations

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

theorem MeasureTheory.cat_add (a b : Torus2) : cat (a + b) = cat a + cat b

noncomputable def MeasureTheory.catHom : Torus2 →+ Torus2

The cat map as an additive monoid hom — the form AddMonoidHom.measurePreserving consumes.

Equations

• MeasureTheory.catHom = AddMonoidHom.mk' MeasureTheory.cat MeasureTheory.cat_add

theorem MeasureTheory.continuous_cat : Continuous cat

noncomputable def MeasureTheory.catInv : Torus2 → Torus2

The inverse (x,y) ↦ (x − y, −x + 2y): det [[2,1],[1,1]] = 1.

Equations

• MeasureTheory.catInv q = (q.1 - q.2, -q.1 + 2 • q.2)

theorem MeasureTheory.cat_catInv (q : Torus2) : cat (catInv q) = q

theorem MeasureTheory.catInv_cat (p : Torus2) : catInv (cat p) = p

theorem MeasureTheory.surjective_cat : Function.Surjective cat

theorem MeasureTheory.injective_cat : Function.Injective cat

theorem MeasureTheory.bijective_cat : Function.Bijective cat

★ The cat map is a bijection — the property the doubling witness lacks.

theorem MeasureTheory.measurePreserving_cat : MeasurePreserving cat volume volume

★ The cat map preserves Haar measure. A continuous surjective endomorphism of a compact group preserves the Haar probability measure; AddMonoidHom.measurePreserving is exactly that.

theorem MeasureTheory.measurable_cat : Measurable cat

Characters on T²

noncomputable def MeasureTheory.chi (v : ℤ × ℤ) : Torus2 → ℂ

The character χ_(m,n)(x,y) = e^{2πimx} · e^{2πiny}.

Equations

• MeasureTheory.chi v p = (fourier v.1) p.1 * (fourier v.2) p.2

theorem MeasureTheory.continuous_chi (v : ℤ × ℤ) : Continuous (chi v)

theorem MeasureTheory.norm_chi (v : ℤ × ℤ) (p : Torus2) : ‖chi v p‖ = 1

theorem MeasureTheory.integrable_chi (v : ℤ × ℤ) : Integrable (chi v) volume

theorem MeasureTheory.chi_arg_add (v : ℤ × ℤ) (p q : Torus2) : chi v (p + q) = chi v p * chi v q

theorem MeasureTheory.chi_index_add (a b : ℤ × ℤ) (p : Torus2) : chi (a + b) p = chi a p * chi b p

theorem MeasureTheory.chi_index_neg (a : ℤ × ℤ) (p : Torus2) : chi (-a) p = (starRingEnd ℂ) (chi a p)

theorem MeasureTheory.integral_chi_eq_zero {v : ℤ × ℤ} (hv : v ≠ 0) : ∫ (p : Torus2), chi v p = 0

★ A nontrivial character integrates to zero. Translate by a point where the character is -1; Haar is translation-invariant, so the integral equals its own negative.

theorem MeasureTheory.chi_zero (p : Torus2) : chi 0 p = 1

The trivial character is 1.

Transport: characters move by the transpose matrix

def MeasureTheory.catZ : ℤ × ℤ → ℤ × ℤ

The transpose action on character indices.

Equations

• MeasureTheory.catZ v = (2 * v.1 + v.2, v.1 + v.2)

theorem MeasureTheory.fourier_arg_add_index (n : ℤ) (x y : AddCircle 1) : (fourier n) (x + y) = (fourier n) x * (fourier n) y

Argument-additivity at a general index. ⚠️ Named apart from CorrelationDecayWitness.fourier_arg_add, which is the index-1 special case in this same namespace; Mathlib itself has only index-additivity (fourier_add).

theorem MeasureTheory.fourier_zsmul_arg (m k : ℤ) (x : AddCircle 1) : (fourier m) (k • x) = (fourier (m * k)) x

theorem MeasureTheory.chi_cat (v : ℤ × ℤ) (p : Torus2) : chi v (cat p) = chi (catZ v) p

★ The transport rule χ_v ∘ cat = χ_{catZ v}.

theorem MeasureTheory.chi_cat_iterate (v : ℤ × ℤ) (u : ℕ) (p : Torus2) : chi v (cat^[u] p) = chi (catZ^[u] v) p

theorem MeasureTheory.catZ_orbit_pos (u : ℕ) : 1 ≤ (catZ^[u + 1] (1, 0)).1 ∧ 1 ≤ (catZ^[u + 1] (1, 0)).2

★ Orbit positivity. Both coordinates of catZ^[u+1] (1,0) are ≥ 1: the recursion is Fibonacci-positive, so no eigenvalue theory is needed for the concrete matrix.

theorem MeasureTheory.catZ_orbit_ne (u : ℕ) : catZ^[u + 1] (1, 0) ≠ (1, 0) ∧ catZ^[u + 1] (1, 0) ≠ (-1, 0)

The orbit never returns to ±(1,0) after the first step — the non-degeneracy the four-term expansion needs.

The observable and its correlations

noncomputable def MeasureTheory.catObs : Torus2 → ℝ

The observable catObs (x,y) = Re e^{2πix} — the same function the doubling witness uses, read on the first coordinate.

Equations

• MeasureTheory.catObs p = (MeasureTheory.chi (1, 0) p).re

theorem MeasureTheory.measurable_catObs : Measurable catObs

theorem MeasureTheory.abs_catObs_le_one (p : Torus2) : |catObs p| ≤ 1

theorem MeasureTheory.integrable_catObs : Integrable catObs volume

theorem MeasureTheory.integrable_catObs_iterate (u : ℕ) : Integrable (fun (p : Torus2) => catObs (cat^[u] p)) volume

theorem MeasureTheory.integrable_catObs_pair (u : ℕ) : Integrable (fun (p : Torus2) => catObs p * catObs (cat^[u] p)) volume

theorem MeasureTheory.re_mul_re (z w : ℂ) : z.re * w.re = ((z * w + z * (starRingEnd ℂ) w + (starRingEnd ℂ) z * w + (starRingEnd ℂ) z * (starRingEnd ℂ) w) / 4).re

The four-term expansion of a product of real parts.

theorem MeasureTheory.integral_catObs : ∫ (p : Torus2), catObs p = 0

The mean of the observable is zero.

theorem MeasureTheory.integral_chi_re (z : ℤ × ℤ) : ∫ (p : Torus2), (chi z p).re = if z = 0 then 1 else 0

The real part of a character integrates to 1 at the trivial index and 0 otherwise.

def MeasureTheory.catIdx (u : ℕ) : ℤ × ℤ

The lag-u orbit index of the base character (1,0).

Equations

• MeasureTheory.catIdx u = MeasureTheory.catZ^[u] (1, 0)

theorem MeasureTheory.catObs_mul_iterate (u : ℕ) (p : Torus2) : catObs p * catObs (cat^[u] p) = ((chi ((1, 0) + catIdx u) p).re + (chi ((1, 0) + -catIdx u) p).re + (chi (-(1, 0) + catIdx u) p).re + (chi (-(1, 0) + -catIdx u) p).re) / 4

The four-character expansion of the lag-u integrand.

theorem MeasureTheory.integral_four (f₁ f₂ f₃ f₄ : Torus2 → ℝ) (h₁ : Integrable f₁ volume) (h₂ : Integrable f₂ volume) (h₃ : Integrable f₃ volume) (h₄ : Integrable f₄ volume) : ∫ (p : Torus2), f₁ p + f₂ p + f₃ p + f₄ p = (((∫ (p : Torus2), f₁ p) + ∫ (p : Torus2), f₂ p) + ∫ (p : Torus2), f₃ p) + ∫ (p : Torus2), f₄ p

Additivity of the integral over a four-term real sum, in the shape the expansion produces.

theorem MeasureTheory.integral_catObs_pair (u : ℕ) : ∫ (p : Torus2), catObs p * catObs (cat^[u] p) = if u = 0 then 1 / 2 else 0

★ The correlations vanish at every nonzero lag, and equal 1/2 at lag zero.

★★ The witness

noncomputable def MeasureTheory.catEnv : ℕ → ℝ

The finitely-supported decay envelope: 1/2 at lag zero, 0 afterwards.

Equations

• MeasureTheory.catEnv u = if u = 0 then 1 / 2 else 0

theorem MeasureTheory.cat_hasCorrelationDecay : HasCorrelationDecay volume cat catObs catEnv

★★ An INVERTIBLE map satisfies HasCorrelationDecay. Arnold's cat map on T², with the observable Re e^{2πix}, has vanishing correlations at every nonzero lag. Unlike the doubling witness this map is a bijection (bijective_cat), so the predicate is inhabited by a map of the kind a symplectic Σ-flow could be.

theorem MeasureTheory.cat_nontrivial : ∫ (p : Torus2), catObs p * catObs p ≠ (∫ (p : Torus2), catObs p) ^ 2

★ The witness is not the trivial constant observable: ⟨f²⟩ = 1/2 ≠ 0 = ⟨f⟩².