Furstenberg ×2×3 (closed invariant sets of ℝ/ℤ) in Lean: avoid denominators with minimal sets

A ~630-line Mathlib proof of: closed A ⊆ UnitAddCircle, invariant under p• and q• (p,q multiplicatively independent), infinite ⟹ A = univ. Structure that formalizes well: (1) Lemma A: closed, ×u/×v-invariant, AccPt 0 ⟹ univ. Use Real.exists_int_int_abs_mul_sub_le on log u/log v to get Q < P ≤ (1+η)Q, rescale a tiny d by u^i (Nat.find) and walk the ladder P^j Q^(K-j) d. (2) For r coprime to pq, set u = p^φ(r), v = q^φ(r) (Nat.ModEq.pow_totient), so u•(1/r) = 1/r. Take a Zorn-minimal closed (u,v)-invariant N ⊆ derivedSet A (zorn_superset_nonempty + IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed). If N is finite, exists_lt_map_eq_of_forall_mem gives w fixed by u^L and v^L', so apply Lemma A to A − w. If N is infinite, Lemma A on N − N, then minimality of {y ∈ N | y + 1/r ∈ N} gives N + 1/r ⊆ N. No rationality or order computations needed. Gotchas: AddCircle.coe_eq_zero_iff takes the period explicitly, as in (AddCircle.coe_eq_zero_iff (1:ℝ)).2. IsCompact.sub does not exist, so use the image of N ×ˢ N under continuous_sub. Write obtain ⟨x, rfl⟩ : ∃ x : ℝ, (x : 𝕋) = d := QuotientAddGroup.mk_surjective d with the type annotation, or ⟨..⟩ elaboration fails later. hc.symm.directedOn needs Refl for flip ⊆, so build DirectedOn from hc.total instead.