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.

Status

PROVED (2026-06-10). gandy_harrington_for_relation is now sorry-free: it is the endpoint of Miller's classical category route, fully formalized in this project (see docs/silver-phase2-route.md for the development record):

• G0Fusion.exists_gsGraph_hom — the classical Kechris–Solecki–Todorcevic G₀-dichotomy construction (positivity ideals, Lusin separation, fusion);
• gSGraphHomHypothesis_holds — the homomorphism input, in SilverCategoryRoute.lean;
• isMeagre_pullback_class_of_gSGraph_hom (Miller Prop. 6), isMeagre_of_isMeagre_sections (Kuratowski–Ulam), and mycielski_cantor (Mycielski) — the category glue;
• gandy_harrington_of_gSGraphHom — the assembly used below.

Consequently silver_core_polish, silverBurgessDichotomy, and the instantiation of morley_counting are unconditional, with axioms exactly [propext, Classical.choice, Quot.sound].

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.

Status

Audited invariant (axioms confirmed via #print axioms): the project's descriptive-set-theory chain is sorry-free. gandy_harrington_for_relation, silver_core_polish, silverBurgessDichotomy, and the unconditional instantiation of morley_counting all report exactly [propext, Classical.choice, Quot.sound].

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 gandy_harrington_for_eq {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (hunc : ¬Countable α) : ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ ∀ (a b : ℕ → Bool), a ≠ b → f a ≠ f b

[Equality case, unconditional] Silver's theorem when the relation is equality (r = ⊥): an uncountable Polish space already contains a continuous injection (ℕ → Bool) → α, so distinct inputs give distinct (hence ⊥-inequivalent) outputs.

This is exactly gandy_harrington_for_relation instantiated at r = ⊥ — but, unlike the general Borel case, it needs no descriptive-set-theory machinery beyond mathlib's Cantor–Bendixson theorem (IsClosed.exists_nat_bool_injection_of_not_countable applied to Set.univ). It is the smooth end of the dichotomy; the hard content of Silver lives entirely in the non-smooth relations (see the E₀ note on gandy_harrington_for_relation).

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.