Mycielski's theorem for Cantor space

mycielski_cantor: for a meager set M ⊆ (ℕ → Bool) × (ℕ → Bool) there is a continuous ψ : (ℕ → Bool) → (ℕ → Bool) with (ψ a, ψ b) ∉ M for all a ≠ b. This is Mycielski's independent-set theorem (Kechris, CDST 19.1) specialized to Cantor space and binary relations — step 4 of the classical category route to Silver's theorem (see InfinitaryLogic/Conditional/SilverCategoryRoute.lean and docs/silver-phase2-route.md).

Construction

Write the complement of M over a countable family of dense open sets U k. Build, by recursion on levels, a family of pointed cylinders (anchor, depth) indexed by List Bool nodes:

• split: each node l of level m gets two children b :: l whose anchors differ at the parent's depth coordinate;
• pair-killing fold: all (finitely many) pairs of distinct level-(m+1) nodes are then refined, one pair at a time, so that the product of their cylinders lands inside ⋂ k ≤ m, U k — a dense open set (finite intersection of dense opens, dense by the Baire property of the complete product space).

The scheme of (closed) cylinders has vanishing diameter and contains the closures of its children, so CantorScheme.inducedMap is total and continuous. For distinct branches a ≠ b and any k, at any level m > max (firstDiff a b) k the branch nodes are distinct, so the image pair lies in U k; hence it lies in ⋂ k, U k ⊆ Mᶜ.

Avoidance is achieved only in the limit — for dense M no two cylinders can have cross-product avoiding M — which is why this construction does not factor through CantorScheme.exists_antichain_map (whose sibling cross-avoidance hypothesis is exactly finite-stage avoidance). Injectivity of ψ is not claimed; downstream consumers recover it from reflexivity of the relation being avoided.

Implementation note

Cantor space carries the PiNat metric via PiNat.metricSpaceOfDiscreteUniformity, whose uniformity is definitionally the product uniformity (see the warning on PiNat.metricSpace: since Bool has a UniformSpace instance, the plain PiNat.metricSpace would create a second, non-defeq uniform structure).

Cylinder prerequisites

theorem MycielskiCantor.isClosed_cylinder (x : ℕ → Bool) (n : ℕ) : IsClosed (PiNat.cylinder x n)

Cylinders are closed (they are in fact clopen).

theorem MycielskiCantor.ediam_cylinder_le (x : ℕ → Bool) (n : ℕ) : Metric.ediam (PiNat.cylinder x n) ≤ ENNReal.ofReal ((1 / 2) ^ n)

theorem MycielskiCantor.exists_cylinder_subset {V : Set (ℕ → Bool)} (hV : IsOpen V) {x : ℕ → Bool} (hx : x ∈ V) : ∃ (n : ℕ), PiNat.cylinder x n ⊆ V

Every open neighborhood contains a cylinder around the point.

Pointed cylinders and refinement

def MycielskiCantor.Refines (q p : (ℕ → Bool) × ℕ) : Prop

Refines q p: the pointed cylinder q = (anchor, depth) is at least as deep as p and its cylinder is contained in that of p.

Equations

• MycielskiCantor.Refines q p = (p.2 ≤ q.2 ∧ PiNat.cylinder q.1 q.2 ⊆ PiNat.cylinder p.1 p.2)

theorem MycielskiCantor.Refines.refl (p : (ℕ → Bool) × ℕ) : Refines p p

theorem MycielskiCantor.Refines.trans {r q p : (ℕ → Bool) × ℕ} (h₁ : Refines r q) (h₂ : Refines q p) : Refines r p

theorem MycielskiCantor.exists_refines_box_subset {U : Set ((ℕ → Bool) × (ℕ → Bool))} (hUo : IsOpen U) (hUd : Dense U) (p q : (ℕ → Bool) × ℕ) : ∃ (p' : (ℕ → Bool) × ℕ) (q' : (ℕ → Bool) × ℕ), Refines p' p ∧ Refines q' q ∧ PiNat.cylinder p'.1 p'.2 ×ˢ PiNat.cylinder q'.1 q'.2 ⊆ U

Single pair-killing move: two pointed cylinders can be refined so that the product of their cylinders lands inside a given dense open subset of the square.

theorem MycielskiCantor.exists_refines_forall_pairs {ι : Type u_1} [DecidableEq ι] {U : Set ((ℕ → Bool) × (ℕ → Bool))} (hUo : IsOpen U) (hUd : Dense U) (s : Finset (ι × ι)) (P : ι → (ℕ → Bool) × ℕ) : ∃ (Q : ι → (ℕ → Bool) × ℕ), (∀ (i : ι), Refines (Q i) (P i)) ∧ ∀ ab ∈ s, ab.1 ≠ ab.2 → PiNat.cylinder (Q ab.1).1 (Q ab.1).2 ×ˢ PiNat.cylinder (Q ab.2).1 (Q ab.2).2 ⊆ U

Pair-killing fold: a family of pointed cylinders can be refined so that all pairs of distinct indices from a given finite set of pairs have cylinder products inside a dense open subset of the square.

Level-indexed stages

def MycielskiCantor.boolLists : ℕ → Finset (List Bool)

All binary lists of a given length, as a finset.

Equations

• MycielskiCantor.boolLists 0 = {[]}
• MycielskiCantor.boolLists n.succ = (MycielskiCantor.boolLists n).biUnion fun (l : List Bool) => {false :: l, true :: l}

theorem MycielskiCantor.mem_boolLists_of_length {n : ℕ} {l : List Bool} : l.length = n → l ∈ boolLists n

structure MycielskiCantor.Stage (U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))) (m : ℕ) : Type

Stage m of the construction: a pointed cylinder for every node, such that level-m nodes have depth at least m and all pairs of distinct level-m nodes have cylinder products inside U k for every k < m.

• f : List Bool → (ℕ → Bool) × ℕ
• le_depth (l : List Bool) : l.length = m → m ≤ (self.f l).2
• avoid (l₁ l₂ : List Bool) : l₁.length = m → l₂.length = m → l₁ ≠ l₂ → ∀ k < m, PiNat.cylinder (self.f l₁).1 (self.f l₁).2 ×ˢ PiNat.cylinder (self.f l₂).1 (self.f l₂).2 ⊆ U k

def MycielskiCantor.base (U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))) : Stage U 0

The root stage: every node gets the full space.

Equations

• MycielskiCantor.base U = { f := fun (x : List Bool) => (fun (x : ℕ) => false, 0), le_depth := MycielskiCantor.base._proof_1, avoid := ⋯ }

def MycielskiCantor.presplit {U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))} {m : ℕ} (S : Stage U m) : List Bool → (ℕ → Bool) × ℕ

The split step: each child b :: l refines its parent l by fixing the coordinate at the parent's depth to b.

Equations

• MycielskiCantor.presplit S [] = S.f []
• MycielskiCantor.presplit S (b :: l) = (Function.update (S.f l).1 (S.f l).2 b, (S.f l).2 + 1)

theorem MycielskiCantor.presplit_refines {U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))} {m : ℕ} (S : Stage U m) (b : Bool) (l : List Bool) : Refines (presplit S (b :: l)) (S.f l)

theorem MycielskiCantor.exists_step {U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))} {m : ℕ} (hUo : ∀ (k : ℕ), IsOpen (U k)) (hUd : ∀ (k : ℕ), Dense (U k)) (S : Stage U m) : ∃ (T : Stage U (m + 1)), ∀ (l : List Bool) (b : Bool), l.length = m → Refines (T.f (b :: l)) (S.f l)

The inductive step: split every node, then run the pair-killing fold against the (dense open) intersection of the first m + 1 dense open sets.

noncomputable def MycielskiCantor.stages (U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))) (hUo : ∀ (k : ℕ), IsOpen (U k)) (hUd : ∀ (k : ℕ), Dense (U k)) (m : ℕ) : Stage U m

The full tower of stages, with each level refining the previous one.

Equations

• MycielskiCantor.stages U hUo hUd 0 = MycielskiCantor.base U
• MycielskiCantor.stages U hUo hUd n.succ = Classical.choose ⋯

theorem MycielskiCantor.stages_refines {U : ℕ → Set ((ℕ → Bool) × (ℕ → Bool))} (hUo : ∀ (k : ℕ), IsOpen (U k)) (hUd : ∀ (k : ℕ), Dense (U k)) (m : ℕ) (l : List Bool) (b : Bool) (hl : l.length = m) : Refines ((stages U hUo hUd (m + 1)).f (b :: l)) ((stages U hUo hUd m).f l)

theorem mycielski_cantor {M : Set ((ℕ → Bool) × (ℕ → Bool))} (hM : IsMeagre M) : ∃ (ψ : (ℕ → Bool) → ℕ → Bool), Continuous ψ ∧ ∀ (a b : ℕ → Bool), a ≠ b → (ψ a, ψ b) ∉ M

Mycielski's theorem for Cantor space: for a meager set M in the square of Cantor space, there is a continuous ψ : (ℕ → Bool) → (ℕ → Bool) such that (ψ a, ψ b) ∉ M whenever a ≠ b. (Kechris, CDST 19.1, specialized.) Injectivity of ψ is not asserted; when avoiding a reflexive relation it is automatic.