Recurrence of powers in a compact group

Category: 1-Mathlib. A single elementary fact with no CSD content: in a compact topological group, the powers of any element return to every neighbourhood of the identity, at arbitrarily large exponents.

This is the classical pigeonhole behind almost periodicity, and it is what the equilibration arc (specs/equilibration-arc-plan.md E5) needs in order to say that finite-dimensional unitary dynamics cannot have decaying correlations: a system whose evolution keeps returning near its starting configuration cannot forget it.

The argument

The sequence n ↦ U ^ n lives in a compact space, so it has a cluster point g. Every neighbourhood of g therefore contains U ^ n for infinitely many n; pick two such exponents i < j as far apart as desired. Continuity of (x, y) ↦ y * x⁻¹ at (g, g) lets us choose that neighbourhood small enough that U ^ j * (U ^ i)⁻¹ lands in the target neighbourhood of 1, and powers of a single element commute, so that product is U ^ (j - i).

No metric and no second countability are used, only CompactSpace and IsTopologicalGroup.

Reference: specs/equilibration-arc-plan.md (E5); specs/future-work.md.

theorem exists_le_pow_mem_of_compactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : G) {V : Set G} (hV : V ∈ nhds 1) (M : ℕ) : ∃ (n : ℕ), M ≤ n ∧ U ^ n ∈ V

Powers recur in a compact group. For every neighbourhood V of 1 and every bound M there is an exponent n ≥ M with U ^ n ∈ V.

The M is the whole point: without it the statement is trivially witnessed by n = 0. With it, the conclusion is that the orbit returns near the identity forever, which is what forbids any quantity built from U ^ n from settling to a different value.

theorem exists_le_nsmul_mem_of_compactSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] (U : G) {V : Set G} (hV : V ∈ nhds 0) (M : ℕ) : ∃ (n : ℕ), M ≤ n ∧ n • U ∈ V