What returns under a shear: the torsion circles

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

The t-th iterate of the horizontal shear (x, y) ↦ (x + y, y) is (x, y) ↦ (x + t·y, y), so a point returns after t strokes iff t·y = 0: the return set is the union of the t circles over the t-torsion points of the read coordinate, infinite at every stroke. So a shear fails the return criterion (#177) at every stroke, not merely at one — the finite clause never holds.

• MeasureTheory.shearX_iterate, shearY_iterate — the iterates in closed form;
• ★★ MeasureTheory.shearX_iterate_fixed_iff, shearY_iterate_fixed_iff — a point returns iff its read coordinate is t-torsion;
• ★ MeasureTheory.infinite_fixedPoints_shearX_iterate, infinite_fixedPoints_shearY_iterate — the return set at every stroke is infinite (it contains a whole circle);
• ★★ MeasureTheory.not_hasReturnGrowth_shearX, not_hasReturnGrowth_shearY.

Honest scope

• The count of t-torsion points of the circle (t of them) is not used: only t • y = 0 is, which is the definition of t-torsion.
• Both shears are elements of SL₂(ℤ) with trace 2, so #179 already gives "no return growth" abstractly; this file says which configurations return, and that the failure is at every stroke.

References: Mathlib/Dynamics/CatMapShears.lean (#153, shearX, shearY, cat_eq_shearX_comp_shearY), Mathlib/Dynamics/ReturnCriterion.lean (#177); specs/BACKLOG.md #181, #19.

The iterates

theorem MeasureTheory.shearX_iterate (t : ℕ) : shearX^[t] = fun (p : Torus2) => (p.1 + t • p.2, p.2)

theorem MeasureTheory.shearY_iterate (t : ℕ) : shearY^[t] = fun (p : Torus2) => (p.1, p.2 + t • p.1)

What returns: the torsion circles

theorem MeasureTheory.shearX_iterate_fixed_iff (t : ℕ) (p : Torus2) : shearX^[t] p = p ↔ t • p.2 = 0

★★ A point returns under t horizontal shears iff its read coordinate is t-torsion.

theorem MeasureTheory.shearY_iterate_fixed_iff (t : ℕ) (p : Torus2) : shearY^[t] p = p ↔ t • p.1 = 0

★★ A point returns under t vertical shears iff its read coordinate is t-torsion.

The return sets are infinite at every stroke

theorem MeasureTheory.infinite_fixedPoints_shearX_iterate (t : ℕ) : Infinite { p : Torus2 // shearX^[t] p = p }

The circle {(x, 0)} lies in every return set of the horizontal shear.

theorem MeasureTheory.infinite_fixedPoints_shearY_iterate (t : ℕ) : Infinite { p : Torus2 // shearY^[t] p = p }

The circle {(0, y)} lies in every return set of the vertical shear.

theorem MeasureTheory.not_hasReturnGrowth_shearX (h : ℝ) : ¬HasReturnGrowth shearX h

★★ A shear has no return growth: its finite clause fails at every stroke.

theorem MeasureTheory.not_hasReturnGrowth_shearY (h : ℝ) : ¬HasReturnGrowth shearY h