Towards the classical G₀-dichotomy: independence and positivity machinery

Foundations for the proof of GSGraphHomHypothesis (the KST/Miller G₀-dichotomy core; see InfinitaryLogic/Conditional/SilverCategoryRoute.lean and docs/silver-phase2-route.md). This file provides the two pillars of the classical (forcing-free, effective-DST-free) proof:

• The separation core (exists_measurableSet_relIndependent_superset): for an analytic relation G on a Polish space, every analytic G-independent set is contained in a Borel G-independent set. This is the Kechris–Solecki–Todorcevic lemma, proved here by an ω-recursion of Lusin separations (AnalyticSet.measurablySeparable): build a decreasing sequence of Borel sets C n ⊇ A, each separated from the G-neighborhood of the previous one; the intersection is Borel and independent.

• The positivity machinery (SmallFam): a family Φ of finite assignments ι → α is small if countably many Borel G-independent sets capture a value of every member — Miller's ideal I_n on partial homomorphisms. Smallness is monotone and countably additive (SmallFam.iUnion_of_forall), giving the pigeonhole (exists_not_smallFam_inter) used to refine positive families by vertex-value and witness-prefix constraints. For the graph ¬r of a Borel equivalence relation with uncountably many classes, the full family is not small (not_smallFam_univ): every ¬r-independent set lies in a single class, so a countable capture family would make the quotient countable.

• Combination positivity (not_smallFam_comb_cross, with not_smallFam_comb_pairs for levels with no fresh constraint): combining pairs of assignments from a positive analytic family across a fresh G-edge constraint at a designated index yields a positive family. This is Miller's "combining pairs of homomorphisms preserves I_n-positivity": if a countable Borel independent family captured the combined family, the assignments avoiding the capture would form a positive analytic family whose values at the cross index are G-independent, and the KST superset lemma would capture it — contradiction. The analyticity side (analyticSet_comb_pairs/analyticSet_comb_cross) keeps the recursion going; the closure facts needed (AnalyticSet.inter, AnalyticSet.inter_measurableSet, AnalyticSet.prod) are proved here.

The level recursion (vertex-shrinking and witness-extension pigeonholes) and the fusion extracting the continuous homomorphism build on these in InfinitaryLogic/Descriptive/G0Fusion.lean; see docs/silver-phase2-route.md for the completed proof map.

Independent sets and neighborhoods

def RelIndependent {α : Type u_1} (G : Set (α × α)) (A : Set α) : Prop

A set is independent for a relation G (a set of pairs) if it contains no G-edge.

Equations

• RelIndependent G A = ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → (a, b) ∉ G

theorem RelIndependent.mono {α : Type u_1} {G : Set (α × α)} {A B : Set α} (hBA : B ⊆ A) (hA : RelIndependent G A) : RelIndependent G B

def relNbhd {α : Type u_1} (G : Set (α × α)) (C : Set α) : Set α

The set of points G-adjacent (in either orientation) to some point of C.

Equations

• relNbhd G C = {x : α | ∃ y ∈ C, (x, y) ∈ G ∨ (y, x) ∈ G}

theorem relNbhd_mono {α : Type u_1} {G : Set (α × α)} {C D : Set α} (h : C ⊆ D) : relNbhd G C ⊆ relNbhd G D

theorem RelIndependent.disjoint_relNbhd {α : Type u_1} {G : Set (α × α)} {A : Set α} (hA : RelIndependent G A) : Disjoint A (relNbhd G A)

theorem analyticSet_relNbhd {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {G : Set (α × α)} (hG : MeasureTheory.AnalyticSet G) {C : Set α} (hC : MeasureTheory.AnalyticSet C) : MeasureTheory.AnalyticSet (relNbhd G C)

theorem exists_measurableSet_relIndependent_superset {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} (hG : MeasureTheory.AnalyticSet G) {A : Set α} (hA : MeasureTheory.AnalyticSet A) (hAind : RelIndependent G A) : ∃ (B : Set α), MeasurableSet B ∧ A ⊆ B ∧ RelIndependent G B

The KST independent-superset lemma: every analytic independent set for an analytic relation on a Polish space is contained in a Borel independent set. Proved by an ω-recursion of Lusin separations.

The smallness ideal on families of finite assignments

def SmallFam {α : Type u_1} [MeasurableSpace α] (G : Set (α × α)) {ι : Type u_2} (Φ : Set (ι → α)) : Prop

A family Φ of assignments ι → α is small for G if countably many Borel G-independent sets capture a value of every member of Φ. This is Miller's ideal I_n on the spaces of partial homomorphisms.

Equations

• SmallFam G Φ = ∃ (C : ℕ → Set α), (∀ (k : ℕ), MeasurableSet (C k) ∧ RelIndependent G (C k)) ∧ ∀ φ ∈ Φ, ∃ (i : ι) (k : ℕ), φ i ∈ C k

theorem SmallFam.mono {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Φ Ψ : Set (ι → α)} (hΨΦ : Ψ ⊆ Φ) (h : SmallFam G Φ) : SmallFam G Ψ

theorem SmallFam.empty {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} : SmallFam G ∅

theorem SmallFam.iUnion_of_forall {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Ψ : ℕ → Set (ι → α)} (h : ∀ (n : ℕ), SmallFam G (Ψ n)) : SmallFam G (⋃ (n : ℕ), Ψ n)

Smallness is countably additive.

theorem exists_not_smallFam_inter {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Φ : Set (ι → α)} (hΦ : ¬SmallFam G Φ) {Ψ : ℕ → Set (ι → α)} (hcov : Φ ⊆ ⋃ (n : ℕ), Ψ n) : ∃ (n : ℕ), ¬SmallFam G (Φ ∩ Ψ n)

Positivity pigeonhole: a non-small family covered by countably many pieces has a non-small piece. Used to refine positive families by vertex-value and witness-prefix constraints.

theorem nonempty_of_not_smallFam {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Φ : Set (ι → α)} (hΦ : ¬SmallFam G Φ) : Φ.Nonempty

Non-small families are nonempty.

The seed: positivity of the full family for ¬r

theorem rel_of_relIndependent_compl {α : Type u_1} (r : Setoid α) {C : Set α} (hC : RelIndependent {p : α × α | ¬r p.1 p.2} C) ⦃a : α⦄ : a ∈ C → ∀ ⦃b : α⦄, b ∈ C → r a b

For the complement graph of an equivalence relation, independent sets lie in a single class.

theorem not_smallFam_univ {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} [Nonempty ι] (r : Setoid α) (hunc : ¬Countable (Quotient r)) : ¬SmallFam {p : α × α | ¬r p.1 p.2} Set.univ

The seed: if a Borel equivalence relation has uncountably many classes, then the full family of assignments is not small for the complement graph — a countable capture family of independent (hence single-class) Borel sets would make the quotient countable.

theorem SmallFam.union {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Φ₁ Φ₂ : Set (ι → α)} (h₁ : SmallFam G Φ₁) (h₂ : SmallFam G Φ₂) : SmallFam G (Φ₁ ∪ Φ₂)

Smallness is binary additive.

Analytic-set closure helpers

theorem MeasureTheory.AnalyticSet.inter {α : Type u_1} [TopologicalSpace α] [T2Space α] {A B : Set α} (hA : AnalyticSet A) (hB : AnalyticSet B) : AnalyticSet (A ∩ B)

theorem MeasureTheory.AnalyticSet.inter_measurableSet {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {A B : Set α} (hA : AnalyticSet A) (hB : MeasurableSet B) : AnalyticSet (A ∩ B)

theorem MeasureTheory.AnalyticSet.prod {α : Type u_1} [TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {A : Set α} {B : Set β} (hA : AnalyticSet A) (hB : AnalyticSet B) : AnalyticSet (A ×ˢ B)

Combination positivity

theorem not_smallFam_comb_pairs {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {κ : Type u_3} {Φ : Set (ι → α)} (hΦ : ¬SmallFam G Φ) (comb : (ι → α) → (ι → α) → κ → α) (hvals : ∀ (φ₀ φ₁ : ι → α) (v : κ), (∃ (i : ι), comb φ₀ φ₁ v = φ₀ i) ∨ ∃ (i : ι), comb φ₀ φ₁ v = φ₁ i) : ¬SmallFam G {ψ : κ → α | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, ψ = comb φ₀ φ₁}

Capture transfer for the plain combination (a level with no fresh cross constraint): combining pairs from a positive family yields a positive family.

theorem not_smallFam_comb_cross {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {ι : Type u_2} {κ : Type u_3} [Countable ι] (hG : MeasureTheory.AnalyticSet G) {Φ : Set (ι → α)} (hΦa : MeasureTheory.AnalyticSet Φ) (hΦ : ¬SmallFam G Φ) (s : ι) (comb : (ι → α) → (ι → α) → κ → α) (hvals : ∀ (φ₀ φ₁ : ι → α) (v : κ), (∃ (i : ι), comb φ₀ φ₁ v = φ₀ i) ∨ ∃ (i : ι), comb φ₀ φ₁ v = φ₁ i) : ¬SmallFam G {ψ : κ → α | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, (φ₀ s, φ₁ s) ∈ G ∧ ψ = comb φ₀ φ₁}

Combination positivity across a fresh edge (the core lemma of the classical G₀-dichotomy; Miller's "combining pairs of homomorphisms preserves I_n-positivity"): combining pairs of assignments from a positive analytic family subject to a fresh G-edge constraint between the values at s yields a positive family.

If a countable Borel independent family captured the combined family, the members of Φ avoiding its union would form a positive analytic subfamily Φ' (positivity by additivity, analyticity since the avoided set is Borel); no two members of Φ' can satisfy the cross constraint (the combination would escape the capture), so the values of Φ' at s form an analytic G-independent set, and the KST superset lemma yields a single Borel independent set capturing Φ' — contradiction.

theorem analyticSet_comb_pairs {α : Type u_1} [TopologicalSpace α] {ι : Type u_2} {κ : Type u_3} {Φ : Set (ι → α)} (hΦa : MeasureTheory.AnalyticSet Φ) (comb : (ι → α) → (ι → α) → κ → α) (hcomb : Continuous fun (p : (ι → α) × (ι → α)) => comb p.1 p.2) : MeasureTheory.AnalyticSet {ψ : κ → α | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, ψ = comb φ₀ φ₁}

Analyticity of the plain combined family.

theorem analyticSet_comb_cross {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {G : Set (α × α)} {ι : Type u_2} {κ : Type u_3} [Countable ι] (hG : MeasureTheory.AnalyticSet G) {Φ : Set (ι → α)} (hΦa : MeasureTheory.AnalyticSet Φ) (s : ι) (comb : (ι → α) → (ι → α) → κ → α) (hcomb : Continuous fun (p : (ι → α) × (ι → α)) => comb p.1 p.2) : MeasureTheory.AnalyticSet {ψ : κ → α | ∃ φ₀ ∈ Φ, ∃ φ₁ ∈ Φ, (φ₀ s, φ₁ s) ∈ G ∧ ψ = comb φ₀ φ₁}

Analyticity of the combined family with a fresh edge constraint.