Cantor schemes with antichain branches

General descriptive-set-theoretic infrastructure for extracting a continuous injection (ℕ → Bool) → α whose distinct image points are pairwise inequivalent for an equivalence relation r, from a Cantor scheme whose sibling pieces are cross-r-inequivalent.

This is the reusable "perfect antichain" extraction layer of Silver-type arguments, factored out of silver_core_closed (InfinitaryLogic/Conditional/SilverBurgess.lean).

Main results

• CantorScheme.exists_antichain_map: the completeness-free core. A Bool-scheme with vanishing diameter, nonempty branch intersections, and r-inequivalent siblings induces a continuous injection of Cantor space with pairwise r-inequivalent images. Branch-limit membership in the actual scheme sets is a hypothesis rather than being derived from closure-nesting: in the eventual Gandy–Harrington argument the scheme pieces are Σ¹₁ (not closed) and branch limits are supplied by strong-Choquet fusion. No closedness, disjointness, or completeness is assumed; injectivity follows from the antichain property and reflexivity of r.
• CantorScheme.exists_antichain_map_of_splitting: the splitting-predicate builder. Given a "largeness" predicate P on closed subsets of a complete space, stable under splitting into two small-diameter cross-r-inequivalent pieces, this builds the scheme by recursion and discharges the branch-limit hypothesis via ClosureAntitone.map_of_vanishingDiam.

theorem CantorScheme.mem_inducedMap_fst_iff {β : Type u_1} {α : Type u_2} {A : List β → Set α} {x : ℕ → β} : x ∈ (inducedMap A).fst ↔ (⋂ (n : ℕ), A (PiNat.res x n)).Nonempty

Membership in the domain of inducedMap is definitionally nonemptiness of the branch intersection.

theorem CantorScheme.exists_antichain_map {α : Type u} [PseudoMetricSpace α] (r : Setoid α) {A : List Bool → Set α} (hlim : ∀ (x : ℕ → Bool), (⋂ (n : ℕ), A (PiNat.res x n)).Nonempty) (hdiam : VanishingDiam A) (hcross : ∀ (l : List Bool), ∀ x ∈ A (false :: l), ∀ y ∈ A (true :: l), ¬r x y) : ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ (∀ (a : ℕ → Bool) (n : ℕ), f a ∈ A (PiNat.res a n)) ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬r (f a) (f b)

Cantor scheme → perfect antichain (core extraction). A Bool-scheme with vanishing diameter, nonempty branch intersections, and r-inequivalent siblings induces a continuous injection f : (ℕ → Bool) → α whose images lie along the scheme and are pairwise r-inequivalent.

No completeness, closedness, or sibling-disjointness is assumed: injectivity follows from the antichain property together with reflexivity of r. The branch-limit hypothesis hlim is exactly totality of inducedMap (see mem_inducedMap_fst_iff); for schemes of closed sets in a complete space it can be discharged by ClosureAntitone.map_of_vanishingDiam (see exists_antichain_map_of_splitting), while a Gandy–Harrington fusion argument can supply it for non-closed pieces.

theorem CantorScheme.exists_antichain_map_of_splitting {α : Type u} [MetricSpace α] [CompleteSpace α] (r : Setoid α) (P : Set α → Prop) (hcl : ∀ (F : Set α), P F → IsClosed F) (hne : ∀ (F : Set α), P F → F.Nonempty) {E : Set α} (hE : P E) (hsplit : ∀ (F : Set α), P F → ∀ (ε : ENNReal), 0 < ε → ∃ (F₀ : Set α) (F₁ : Set α), P F₀ ∧ P F₁ ∧ F₀ ⊆ F ∧ F₁ ⊆ F ∧ Metric.ediam F₀ ≤ ε ∧ Metric.ediam F₁ ≤ ε ∧ ∀ x ∈ F₀, ∀ y ∈ F₁, ¬r x y) : ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ (∀ (a : ℕ → Bool), f a ∈ E) ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬r (f a) (f b)

Splitting predicate → perfect antichain. Let P be a "largeness" predicate on closed subsets of a complete metric space such that every large set splits into two large pieces of arbitrarily small diameter with no cross-r-equivalence. Then from any large set E one can extract a continuous injection f : (ℕ → Bool) → α into E whose images are pairwise r-inequivalent.

Sibling disjointness is not required of the splitting: it is never used (injectivity comes from the antichain property and reflexivity of r).