Silver via the classical category route (Miller): interface layer

This file holds the route to gandy_harrington_for_relation (now fully proved): Benjamin Miller's classical, forcing-free, effective-DST-free proof of Silver's theorem ["The graph-theoretic approach to descriptive set theory", BSL 18(4), 2012, Theorem 11; also "Forceless, ineffective, powerless proofs of descriptive dichotomy theorems, Lecture I"]. The proof composes:

1. KST G₀-dichotomy (classical proof via the σ-ideal of Borel G-independent sets): for the graph G = ¬E off the diagonal, either there is a Borel ℵ₀-coloring — giving countably many classes — or a continuous homomorphism φ : 2^ℕ → α from G_S(2^ℕ) to G.
2. Pullback + Kuratowski–Ulam: every class of E' = (φ × φ)⁻¹(E) is G_S-independent, hence meager (for dense S); Kuratowski–Ulam then makes E' itself meager.
3. Mycielski: a meager equivalence relation on Cantor space admits a continuous map ψ : 2^ℕ → 2^ℕ with distinct points inequivalent.
4. f = φ ∘ ψ is the desired perfect antichain.

Steps 1–2 are packaged here as CategoryReductionHypothesis, step 3 as MycielskiCantorHypothesis, and step 4 is proved: gandy_harrington_of_category_route derives the exact statement of gandy_harrington_for_relation from the two hypotheses.

Design note (audit outcome)

An earlier candidate design — a Gandy–Harrington-style forcing layer (Cond/split/fusion on subsets of α) feeding CantorScheme.exists_antichain_map — does NOT match this route: in Miller's proof the forcing-style largeness lives on spaces of finite partial homomorphisms 2^n → α (the I_n-positive sets inside the classical G₀-dichotomy proof), not on subsets of α, and the final antichain is a composite φ ∘ ψ rather than the limit of a scheme on α. Sibling cross-avoidance at finite stages is impossible for dense relations (e.g. the pullback of E₀), so exists_antichain_map is not the assembly point for this route; it remains the assembly point for the closed case (silver_core_closed).

Route decomposition (all classical; no effective DST; all proved)

• MycielskiCantorHypothesis — proved as mycielskiCantorHypothesis_holds, via mycielski_cantor in InfinitaryLogic/Descriptive/Mycielski.lean.
• CategoryReductionHypothesis — decomposes into: Kuratowski–Ulam (isMeagre_of_isMeagre_sections in InfinitaryLogic/Descriptive/KuratowskiUlam.lean); the G_S(2^ℕ) graphs with the dense-S independence lemma (exists_gSGraph_edge_of_not_isMeagre and isMeagre_pullback_class_of_gSGraph_hom in InfinitaryLogic/Descriptive/GSGraph.lean); and the classical G₀-dichotomy (Miller's proof of KST via I_n-positive sets of partial homomorphisms — the hard core, proved by the fusion construction G0Fusion.exists_gsGraph_hom over the positivity machinery of InfinitaryLogic/Descriptive/G0Dichotomy.lean). The wiring categoryReductionHypothesis_of_gSGraphHom reduces it to the single Prop GSGraphHomHypothesis — a continuous homomorphism from GSGraph canonicalS (dense and sparse, see denseWords_canonicalS / sparseWords_canonicalS) into ¬r whenever r is Borel with uncountable quotient — proved below as gSGraphHomHypothesis_holds, so the whole chain through gandy_harrington_of_gSGraphHom is unconditional.

def CategoryReductionHypothesis : Prop

Category reduction (hypothesis form): a Borel equivalence relation with uncountably many classes on a Polish space admits a continuous φ : 2^ℕ → α whose pullback relation is meager. This packages steps 1–2 of Miller's classical proof of Silver's theorem: the G₀-dichotomy applied to the complement graph ¬r (the coloring side is impossible with uncountably many classes), followed by G_S-independence of the pullback classes and Kuratowski–Ulam.

Equations

• One or more equations did not get rendered due to their size.

def GSGraphHomHypothesis : Prop

The G₀-dichotomy input (hypothesis form; proved below as gSGraphHomHypothesis_holds): a Borel equivalence relation with uncountably many classes on a Polish space admits a continuous graph homomorphism from GSGraph canonicalS into its complement. This is the homomorphism half of the Kechris–Solecki–Todorcevic G₀-dichotomy applied to the graph ¬r (the coloring half is impossible: a Borel ℵ₀-coloring of ¬r would make the quotient countable); canonicalS is dense (consumed by isMeagre_pullback_class_of_gSGraph_hom) and sparse (required for the dichotomy itself; see sparseWords_canonicalS).

Equations

• One or more equations did not get rendered due to their size.

theorem gandy_harrington_of_gSGraphHom (h : GSGraphHomHypothesis) {α : 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)

The full chain: the G₀-dichotomy input alone yields the exact statement of gandy_harrington_for_relation; it is fed gSGraphHomHypothesis_holds below.

theorem gSGraphHomHypothesis_holds : GSGraphHomHypothesis

The G₀-dichotomy input holds (2C-b complete): proved by the fusion construction G0Fusion.exists_gsGraph_hom over the positivity machinery of G0Dichotomy.lean. The complement graph is Borel hence analytic, nonempty (else the quotient is a singleton), and mathlib's AnalyticSet definition provides the continuous parametrization g whose witnesses drive the fusion.