Silver's Theorem for Borel Equivalence Relations

This file provides:

1. gandy_harrington_for_relation: Silver's theorem for Borel equivalence relations on Polish spaces — a Borel equivalence relation with uncountably many classes contains a perfect set of pairwise-inequivalent points.
2. silver_core_polish: the dichotomy form (countable quotient or perfect set of inequivalent points), derived as a thin wrapper.
3. silverBurgessDichotomy: the full dichotomy for standard Borel spaces.

The equality case gandy_harrington_for_eq (via Cantor–Bendixson) is kept as a simple direct proof of the smooth end of the dichotomy.

Why there was no easy reduction to a "closed relation" case. A tempting plan is to refine the Polish topology so the Borel relation becomes closed and then run a Cantor scheme. This is invalid in general: a closed equivalence relation on a Polish space is smooth (the class map x ↦ [x] into the Effros–Borel space is Borel), so "potentially closed ⟹ smooth". But E₀ (eventual equality on 2^ℕ) is a Borel equivalence relation with continuum-many classes — so Silver applies — that is not smooth (Glimm–Effros), hence not potentially closed. So the hard core of Silver is exactly the non-smooth relations — the G₀-dichotomy content of the category route.

theorem gandy_harrington_for_relation {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (r : Setoid α) (hr : MeasurableSet {p : α × α | r p.1 p.2}) (hunc : ¬Countable (Quotient r)) : ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬r (f a) (f b)

Silver's theorem for Borel equivalence relations. A Borel equivalence relation on a Polish space with uncountably many classes contains a perfect set of pairwise-inequivalent points: there is a continuous injection f : (ℕ → Bool) → α such that distinct inputs produce r-inequivalent outputs.

Proved via Miller's classical category route: the G₀-dichotomy homomorphism (gSGraphHomHypothesis_holds, by the fusion construction G0Fusion.exists_gsGraph_hom), Miller's independence lemma, Kuratowski–Ulam, and Mycielski's theorem, assembled by gandy_harrington_of_gSGraphHom.

theorem silver_core_polish {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (r : Setoid α) (hr : MeasurableSet {p : α × α | r p.1 p.2}) : Countable (Quotient r) ∨ ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬r (f a) (f b)

Silver's theorem (dichotomy form) for Borel equivalence relations on Polish spaces. Either the quotient is countable, or there exists a perfect set of pairwise-inequivalent points.

Silver-Burgess dichotomy

theorem FirstOrder.Language.silverBurgessDichotomy : SilverBurgessDichotomy

The Silver-Burgess dichotomy for Borel equivalence relations on standard Borel spaces, derived from silver_core_polish.