The graphs G_S(2^ℕ) and Miller's independence lemma

This file defines the graphs G_S on Cantor space associated to a set S of finite binary words, and proves Miller's Proposition 6 ["The graph-theoretic approach to descriptive set theory", BSL 18(4), 2012]: for dense S (every word extends into S), a non-meager set with the Baire property contains a G_S-edge. Consequently every class of an equivalence relation avoiding G_S is meager (isMeagre_class_of_gSGraph_disjoint), and in pullback form (isMeagre_pullback_class_of_gSGraph_hom): a continuous φ : 2^ℕ → α that is a graph homomorphism from G_S to the complement of a Borel equivalence relation E makes every section {b | E (φ a) (φ b)} meager.

This is step 2 of the classical category route to Silver's theorem (InfinitaryLogic/Conditional/SilverCategoryRoute.lean; see docs/silver-phase2-route.md): combined with Kuratowski–Ulam (isMeagre_of_isMeagre_sections) and Mycielski (mycielski_cantor), it reduces CategoryReductionHypothesis to exactly the classical G₀-dichotomy.

Definitions

• prependWord w x: the element of Cantor space starting with the word w and continuing with x; wordCylinder w is its range, the basic clopen set of sequences extending w.
• GSGraph S y z: y = s ⌢ i ⌢ x and z = s ⌢ !i ⌢ x for some s ∈ S, i, x — the two sequences extend the same s ∈ S, differ at position s.length, and share the tail.
• DenseWords S: every finite word has an extension in S.

Proof of the independence lemma

By the Baire property, a non-meager B is comeager in some nonempty open set, hence in some word cylinder wordCylinder r; pick s ∈ S extending r. The two injections prependWord (s ++ [i]) : 2^ℕ → wordCylinder (s ++ [i]) are continuous open maps, so the sets of x with prependWord (s ++ [i]) x ∉ B are meager (IsMeagre.preimage_of_isOpenMap applied to the part of the symmetric difference inside each child cylinder). A common point x outside both meager sets yields the edge (prependWord (s ++ [false]) x, prependWord (s ++ [true]) x) inside B.

Words and word cylinders

def prependWord (w : List Bool) (x : ℕ → Bool) : ℕ → Bool

The element of Cantor space that starts with the finite word w and continues with x.

Equations

• prependWord w x n = if n < w.length then w.getD n false else x (n - w.length)

theorem prependWord_apply_of_lt {w : List Bool} {n : ℕ} (h : n < w.length) (x : ℕ → Bool) : prependWord w x n = w.getD n false

theorem prependWord_apply_of_le {w : List Bool} {n : ℕ} (h : w.length ≤ n) (x : ℕ → Bool) : prependWord w x n = x (n - w.length)

def wordCylinder (w : List Bool) : Set (ℕ → Bool)

The basic clopen set of sequences extending the word w.

Equations

• wordCylinder w = Set.range (prependWord w)

theorem mem_wordCylinder_iff {w : List Bool} {y : ℕ → Bool} : y ∈ wordCylinder w ↔ ∀ n < w.length, y n = w.getD n false

theorem prependWord_mem_wordCylinder (w : List Bool) (x : ℕ → Bool) : prependWord w x ∈ wordCylinder w

theorem wordCylinder_subset_of_prefix {r s : List Bool} (h : r <+: s) : wordCylinder s ⊆ wordCylinder r

theorem isOpen_wordCylinder (w : List Bool) : IsOpen (wordCylinder w)

theorem continuous_prependWord (w : List Bool) : Continuous (prependWord w)

theorem image_prependWord_cylinder (w : List Bool) (x : ℕ → Bool) (n : ℕ) : prependWord w '' PiNat.cylinder x n = PiNat.cylinder (prependWord w x) (w.length + n)

theorem isOpenMap_prependWord (w : List Bool) : IsOpenMap (prependWord w)

def wordOf (x : ℕ → Bool) (n : ℕ) : List Bool

The word formed by the first n values of x.

Equations

• wordOf x n = List.ofFn fun (i : Fin n) => x ↑i

@[simp]

theorem length_wordOf (x : ℕ → Bool) (n : ℕ) : (wordOf x n).length = n

theorem getD_wordOf {x : ℕ → Bool} {n i : ℕ} (h : i < n) : (wordOf x n).getD i false = x i

theorem wordCylinder_wordOf (x : ℕ → Bool) (n : ℕ) : wordCylinder (wordOf x n) = PiNat.cylinder x n

The graphs G_S

def GSGraph (S : Set (List Bool)) (y z : ℕ → Bool) : Prop

The graph G_S(2^ℕ) on Cantor space associated to a set S of finite binary words: edges connect s ⌢ i ⌢ x and s ⌢ !i ⌢ x for s ∈ S.

Equations

• GSGraph S y z = ∃ s ∈ S, ∃ (i : Bool) (x : ℕ → Bool), y = prependWord (s ++ [i]) x ∧ z = prependWord (s ++ [!i]) x

def DenseWords (S : Set (List Bool)) : Prop

A set of words is dense if every word has an extension in it.

Equations

• DenseWords S = ∀ (r : List Bool), ∃ s ∈ S, r <+: s

def SparseWords (S : Set (List Bool)) : Prop

A set of words is sparse if it contains at most one word of each length. The graphs G_S for sparse S are acyclic, and the G₀-dichotomy holds for them.

Equations

• SparseWords S = ∀ ⦃s : List Bool⦄, s ∈ S → ∀ ⦃t : List Bool⦄, t ∈ S → s.length = t.length → s = t

A canonical dense and sparse set of words

def wordEnum (n : ℕ) : List Bool

An enumeration of all finite binary words.

Equations

• wordEnum n = (Encodable.decode n).getD []

theorem wordEnum_encode (w : List Bool) : wordEnum (Encodable.encode w) = w

def padTo (w : List Bool) (n : ℕ) : List Bool

Pad a word with false up to length n.

Equations

• padTo w n = w ++ List.replicate (n - w.length) false

theorem length_padTo {w : List Bool} {n : ℕ} (h : w.length ≤ n) : (padTo w n).length = n

theorem prefix_padTo (w : List Bool) (n : ℕ) : w <+: padTo w n

def canonicalLen : ℕ → ℕ

A strictly increasing length schedule dominating the word enumeration.

Equations

• canonicalLen 0 = (wordEnum 0).length
• canonicalLen n.succ = max (wordEnum (n + 1)).length (canonicalLen n + 1)

theorem le_canonicalLen (n : ℕ) : (wordEnum n).length ≤ canonicalLen n

theorem canonicalLen_strictMono : StrictMono canonicalLen

def canonicalWord (n : ℕ) : List Bool

The n-th canonical word: the n-th word of the enumeration, padded to the n-th length of the schedule.

Equations

• canonicalWord n = padTo (wordEnum n) (canonicalLen n)

theorem length_canonicalWord (n : ℕ) : (canonicalWord n).length = canonicalLen n

def canonicalS : Set (List Bool)

The canonical dense and sparse set of finite binary words.

Equations

• canonicalS = Set.range canonicalWord

theorem denseWords_canonicalS : DenseWords canonicalS

theorem sparseWords_canonicalS : SparseWords canonicalS

Miller's independence lemma (Prop. 6)

theorem exists_gSGraph_edge_of_not_isMeagre {S : Set (List Bool)} (hS : DenseWords S) {B : Set (ℕ → Bool)} (hB : BaireMeasurableSet B) (hBnm : ¬IsMeagre B) : ∃ y ∈ B, ∃ z ∈ B, GSGraph S y z

Miller, Prop. 6: for a dense set S of words, a non-meager set with the Baire property contains a G_S-edge (it is not G_S-independent).

theorem isMeagre_class_of_gSGraph_disjoint {S : Set (List Bool)} (hS : DenseWords S) (E : Setoid (ℕ → Bool)) (hBP : ∀ (a : ℕ → Bool), BaireMeasurableSet {b : ℕ → Bool | E a b}) (hhom : ∀ (y z : ℕ → Bool), GSGraph S y z → ¬E y z) (a : ℕ → Bool) : IsMeagre {b : ℕ → Bool | E a b}

For dense S, every class of an equivalence relation disjoint from G_S (with Baire measurable classes) is meager.

theorem isMeagre_pullback_class_of_gSGraph_hom {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (E : Setoid α) (hE : MeasurableSet {p : α × α | E p.1 p.2}) {S : Set (List Bool)} (hS : DenseWords S) {φ : (ℕ → Bool) → α} (hφ : Continuous φ) (hhom : ∀ (y z : ℕ → Bool), GSGraph S y z → ¬E (φ y) (φ z)) (a : ℕ → Bool) : IsMeagre {b : ℕ → Bool | E (φ a) (φ b)}

Pullback form (the deliverable for the category route): if φ : 2^ℕ → α is continuous and a graph homomorphism from G_S (with S dense) to the complement of a Borel equivalence relation E, then every pullback section {b | E (φ a) (φ b)} is meager. Combined with Kuratowski–Ulam this makes the pullback relation meager, and with Mycielski it produces the perfect antichain; the missing input is exactly the classical G₀-dichotomy producing φ.