Gandy-Harrington Reduction and Silver's Theorem for Borel Relations

This file provides:

1. The Borel-to-closed reduction (borel_to_closed_reduction): if a Borel equivalence relation on a Polish space has uncountably many classes, there exists a Polish space Y with a continuous injective map to α on which the pulled-back relation is closed and still has uncountably many classes.
2. silver_core_polish: Silver's theorem for Borel equivalence relations, derived from the reduction + silver_core_closed.
3. silverBurgessDichotomy: the full dichotomy for standard Borel spaces.

Status

borel_to_closed_reduction requires the Gandy-Harrington topology construction (sorry). Once filled, silver_core_polish and silverBurgessDichotomy become sorry-free, making morley_counting fully unconditional.

Helper lemmas

Gandy-Harrington for a specific relation

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)) : ∃ (Ω : Type u) (x : MetricSpace Ω) (_ : CompleteSpace Ω) (_ : SecondCountableTopology Ω) (i : Ω → α), Continuous i ∧ Function.Injective i ∧ (∀ (x : α), ∃ (y : Ω), r (i y) x) ∧ IsOpen ((fun (p : Ω × Ω) => (i p.1, i p.2)) ⁻¹' {p : α × α | ¬r p.1 p.2})

Gandy-Harrington for a Borel relation: Given a Borel equivalence relation r on a Polish space with uncountably many classes, there exists a Polish Ω with a continuous injective map to α such that:

1. Every r-class meets the range of i.
2. The pullback of Eᶜ is open in Ω × Ω.

The proof requires the Gandy-Harrington topology construction using effective/lightface descriptive set theory (recursively presented Polish spaces, lightface Σ¹₁ sets, countability of codes). This is a genuine DST infrastructure gap not currently available in Mathlib.

GH core existence (derived from relation-specific GH)

Borel-to-closed reduction

theorem borel_to_closed_reduction {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (r : Setoid α) (hr : MeasurableSet {p : α × α | r p.1 p.2}) (hunc : ¬Countable (Quotient r)) : ∃ (Y : Type u) (x : MetricSpace Y) (_ : CompleteSpace Y) (_ : SecondCountableTopology Y) (i : Y → α), Continuous i ∧ Function.Injective i ∧ IsClosed {p : Y × Y | r (i p.1) (i p.2)} ∧ ¬Countable (Quotient (Setoid.comap i r))

Gandy-Harrington reduction: A Borel equivalence relation on a Polish space with uncountably many classes admits a Polish space Y with a continuous injective map to α on which the pulled-back relation is closed and still has uncountably many classes.

Derived from gh_exists_core + not_countable_comap_of_hits_all_classes.

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 for Borel equivalence relations on Polish spaces. Reduces to the closed case via borel_to_closed_reduction, then applies silver_core_closed on the subspace and composes with the embedding.

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.