Silver-Burgess Dichotomy for Borel Equivalence Relations

This file proves the Silver-Burgess splitting lemmas and Silver's theorem for closed equivalence relations on Polish spaces; the Borel case and the full SilverBurgessDichotomy for standard Borel spaces are derived in GandyHarrington.lean (sorry-free since 2026-06-10).

Main Results

The perfect-set and Polish-quotient cardinal facts this file used to open with now live in InfinitaryLogic/Descriptive/PerfectAntichain.lean (Perfect.mk_eq_continuum, continuum_classes_of_perfect_transversal, and the three companions). The names are the same, but the statements are not identical: several now assume less than they did here — in particular continuum_classes_of_perfect_transversal no longer requires second countability. None of them mentions a dichotomy or a splitting hypothesis.

• splitting_lemma_closed: Closed equiv relation with uncountably many classes splits into disjoint closed pieces, each uncountable, cross-inequivalent.
• splitting_lemma_closed_small_diam: the same splitting with diameter ≤ ε control (shrink around a condensation point first).
• silver_core_closed: Silver's theorem for closed equivalence relations on Polish spaces, obtained by feeding splitting_lemma_closed_small_diam to the abstract Cantor-antichain builder CantorScheme.exists_antichain_map_of_splitting (InfinitaryLogic/Descriptive/CantorAntichain.lean).
• silver_core_polish and silverBurgessDichotomy live in GandyHarrington.lean, derived from gandy_harrington_for_relation (proved via the category route in SilverCategoryRoute.lean).

Splitting lemma for closed equivalence relations

def IsClassCondensationPt {α : Type u_1} (r : Setoid α) [TopologicalSpace α] (U : Set α) (x : α) : Prop

A condensation point for E-classes in U: every open neighborhood meets uncountably many E-classes.

Equations

• IsClassCondensationPt r U x = (x ∈ U ∧ ∀ (V : Set α), IsOpen V → x ∈ V → ¬{q : Quotient r | ∃ y ∈ U ∩ V, ⟦y⟧ = q}.Countable)

theorem exists_classCondensationPt_of_uncountable {α : Type u} [TopologicalSpace α] [SecondCountableTopology α] (r : Setoid α) {U : Set α} (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ∃ (x : α), IsClassCondensationPt r U x

In a second-countable space, if U meets uncountably many E-classes, there exist condensation points in uncountably many classes.

theorem uncountable_classCondensationPt_classes {α : Type u} [TopologicalSpace α] [SecondCountableTopology α] (r : Setoid α) {U : Set α} (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ¬{q : Quotient r | ∃ (x : α), IsClassCondensationPt r U x ∧ ⟦x⟧ = q}.Countable

In a second-countable space, if U meets uncountably many E-classes, then uncountably many classes have a condensation point representative in U.

theorem splitting_lemma_closed {α : Type u} [MetricSpace α] [SecondCountableTopology α] (r : Setoid α) (hclosed_r : IsClosed {p : α × α | r p.1 p.2}) {U : Set α} (hU : IsClosed U) (hunc : ¬{q : Quotient r | ∃ y ∈ U, ⟦y⟧ = q}.Countable) : ∃ (U₀ : Set α) (U₁ : Set α), IsClosed U₀ ∧ IsClosed U₁ ∧ U₀ ⊆ U ∧ U₁ ⊆ U ∧ Disjoint U₀ U₁ ∧ ¬{q : Quotient r | ∃ y ∈ U₀, ⟦y⟧ = q}.Countable ∧ ¬{q : Quotient r | ∃ y ∈ U₁, ⟦y⟧ = q}.Countable ∧ ∀ x ∈ U₀, ∀ y ∈ U₁, ¬r x y

Splitting lemma for closed equivalence relations on metric spaces. If a closed set U meets uncountably many classes of a closed equivalence relation, it contains disjoint closed subsets each meeting uncountably many classes with no cross-equivalence.

theorem splitting_lemma_closed_small_diam {α : Type u} [MetricSpace α] [SecondCountableTopology α] (r : Setoid α) (hclosed_r : IsClosed {p : α × α | r p.1 p.2}) {E : Set α} (hE_cl : IsClosed E) (hE_unc : ¬{q : Quotient r | ∃ y ∈ E, ⟦y⟧ = q}.Countable) {ε : ENNReal} (hε : 0 < ε) : ∃ (E₀ : Set α) (E₁ : Set α), (IsClosed E₀ ∧ E₀.Nonempty ∧ E₀ ⊆ E ∧ Metric.ediam E₀ ≤ ε ∧ ¬{q : Quotient r | ∃ y ∈ E₀, ⟦y⟧ = q}.Countable) ∧ (IsClosed E₁ ∧ E₁.Nonempty ∧ E₁ ⊆ E ∧ Metric.ediam E₁ ≤ ε ∧ ¬{q : Quotient r | ∃ y ∈ E₁, ⟦y⟧ = q}.Countable) ∧ Disjoint E₀ E₁ ∧ ∀ x ∈ E₀, ∀ y ∈ E₁, ¬r x y

Small-diameter splitting for closed equivalence relations: a closed set meeting uncountably many classes splits into two disjoint closed pieces of diameter ≤ ε, each nonempty, each meeting uncountably many classes, with no cross-equivalence. Obtained from splitting_lemma_closed by first shrinking around a condensation point.

Core Silver theorem

theorem silver_core_closed {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] (r : Setoid α) (hclosed_r : IsClosed {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 (core Polish space version, for closed equivalence relations): A closed equivalence relation on a Polish space has countably many equivalence classes, or admits a continuous injection from Cantor space whose images are pairwise inequivalent.