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 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

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

A canonical dense and sparse set of words

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 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

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_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 φ.