Furstenberg–Weiss topological multiple recurrence (single-transformation form)

furstenberg_topological

Submitter: Kim Morrison.

Notes: Single-transformation form of the Furstenberg–Weiss topological multiple recurrence theorem (1978), as stated in §56 of Knill's 'Some Fundamental Theorems in Mathematics'. For every homeomorphism T of a nonempty compact metric space X, there is a multiply recurrent point: for every d ≥ 1 there is a strictly increasing n : ℕ → ℕ with T^{j · n_k}(x) → x for every j ∈ {1, …, d}. The file ships the IsMultiplyRecurrent predicate. Compact-Hausdorff alone is insufficient for the sequential formulation (the shift on Ultrafilter ℤ is a counterexample); first-countability would suffice, but the standard Furstenberg–Weiss statement uses compact metric. This is the specialisation to the family T, T², …, T^d of the more general theorem for commuting homeomorphisms.

Source: H. Furstenberg and B. Weiss, *Topological dynamics and combinatorial number theory*, Journal d'Analyse Mathématique 34 (1978), 61-85. Listed as §56 (main theorem) in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Standard proof via compactness + Zorn's lemma. Consider the product diagonal T̃ := (T, T², …, T^d) acting on the product Xᵈ, and pass to a minimal nonempty closed T̃-invariant subset M ⊆ Xᵈ (Zorn). The diagonal point (x, x, …, x) ∈ M for some x ∈ X is the multiply recurrent point: the recurrence of (x, …, x) under T̃ is exactly simultaneous return of T(x), …, T^d(x) to x. Showing the diagonal point lies in M requires the multiple-recurrence content of the proof, typically via topological IP-recurrence in product systems or via Furstenberg's correspondence principle reducing to van der Waerden / Hales–Jewett. The d = 1 case is the classical Birkhoff recurrence, which uses the same Zorn-minimality argument.

theorem declaration uses `sorry`furstenberg_topological_recurrence {X : Type*} [MetricSpace X]
    [CompactSpace X] [Nonempty X] (T : X ≃ₜ X) :
    ∃ x : X, LeanEval.Dynamics.IsMultiplyRecurrent (T : X → X) x := byX:Type u_1inst✝²:MetricSpace Xinst✝¹:CompactSpace Xinst✝:Nonempty XT:X ≃ₜ X⊢ ∃ x, IsMultiplyRecurrent (⇑T) x
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 29, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 31, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 31, 2026