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

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

Level-indexed stages

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.