Fusion for the G₀-dichotomy: level objects and edge bookkeeping

Infrastructure for the fusion recursion of the classical G₀-dichotomy (2C-b sub-block 4; see docs/silver-phase2-route.md), building on the positivity machinery of InfinitaryLogic/Descriptive/G0Dichotomy.lean:

• Finite-word API: coercion-tame access lemmas for Fin.snoc (snoc_apply_of_lt/snoc_apply_last), level restrictions restr n x of branches with restr_succ, and canonical-word vertices cvert m n.
• Edge bookkeeping: LvlEdgeAt m n u v is the oriented level-n trace of the GSGraph canonicalS edge created by canonicalWord m. The three structural lemmas: lvlEdgeAt_fresh (the cross pair at the level just past the word), lvlEdgeAt_succ_elim (every level-(n+1) edge is the fresh cross pair or the snoc of a level-n edge), and lvlEdgeAt_restr (restrictions of a GSGraph edge pair are level edges), with gsGraph_oriented translating GSGraph edges into oriented prepended form.
• Witness words: prepw c w prepends a finite ℕ-word to a Baire-space point; WitSet g u v c is the (analytic) set of assignments whose (u, v)-value pair is g-witnessed through the cylinder of c, with witSet_cover feeding the positivity pigeonhole (exists_not_smallFam_inter) to extend witness words one coordinate at a time (exists_extend_witnesses, a fold over the finitely many tracked edges).
• Vertex shrinking: exists_shrink restricts a positive analytic family so that all members are uniformly (1/2)^n-close at every vertex, by the pigeonhole over a countable cover of α by small balls.

On top of these, the final section builds the fusion recursion itself: the FusionStage tower (exists_fusionStage_zero, exists_fusionStage_succ, fusionTower) and the limit extraction exists_gsGraph_hom — the classical G₀-dichotomy construction completing Silver's theorem.

Finite-word API

theorem G0Fusion.snoc_apply_mk_of_lt {n : ℕ} (u : Fin n → Bool) (i : Bool) {j : ℕ} (hj : j < n) (hj' : j < n + 1) : Fin.snoc u i ⟨j, hj'⟩ = u ⟨j, hj⟩

theorem G0Fusion.snoc_apply_lt {n : ℕ} (u : Fin n → Bool) (i : Bool) (j : Fin (n + 1)) (hj : ↑j < n) : Fin.snoc u i j = u ⟨↑j, hj⟩

Coercion-tame access below the last position.

theorem G0Fusion.snoc_apply_eq {n : ℕ} (u : Fin n → Bool) (i : Bool) (j : Fin (n + 1)) (hj : ↑j = n) : Fin.snoc u i j = i

Coercion-tame access at the last position.

def G0Fusion.restr (n : ℕ) (x : ℕ → Bool) : Fin n → Bool

The level-n restriction of an infinite branch.

Equations

• G0Fusion.restr n x j = x ↑j

theorem G0Fusion.restr_succ (n : ℕ) (x : ℕ → Bool) : restr (n + 1) x = Fin.snoc (restr n x) (x n)

theorem G0Fusion.restr_eq_restr_of_mem_cylinder {x y : ℕ → Bool} {N : ℕ} (h : y ∈ PiNat.cylinder x N) : restr N y = restr N x

def G0Fusion.cvert (m n : ℕ) : Fin n → Bool

The canonical word m as a level-n vertex (positions beyond the word read false).

Equations

• G0Fusion.cvert m n j = (canonicalWord m).getD (↑j) false

Edge bookkeeping

def G0Fusion.LvlEdgeAt (m n : ℕ) (u v : Fin n → Bool) : Prop

The oriented level-n trace of the GSGraph canonicalS edge created by the canonical word m: both vertices extend the word, the cross position carries false on the left and true on the right, and the tails agree.

Equations

• One or more equations did not get rendered due to their size.

theorem G0Fusion.lvlEdgeAt_fresh (m n : ℕ) (h : canonicalLen m = n) : LvlEdgeAt m (n + 1) (Fin.snoc (cvert m n) false) (Fin.snoc (cvert m n) true)

The fresh cross pair at the level just past the canonical word.

theorem G0Fusion.lvlEdgeAt_succ_elim {m n : ℕ} {u v : Fin (n + 1) → Bool} (h : LvlEdgeAt m (n + 1) u v) : canonicalLen m = n ∧ u = Fin.snoc (cvert m n) false ∧ v = Fin.snoc (cvert m n) true ∨ canonicalLen m + 1 ≤ n ∧ u (Fin.last n) = v (Fin.last n) ∧ LvlEdgeAt m n (Fin.init u) (Fin.init v)

Every level-(n + 1) edge is the fresh cross pair (when the word has length exactly n) or the snoc of a level-n edge by a common last bit.

theorem G0Fusion.lvlEdgeAt_snoc {m n : ℕ} {u v : Fin n → Bool} (h : LvlEdgeAt m n u v) (i : Bool) : LvlEdgeAt m (n + 1) (Fin.snoc u i) (Fin.snoc v i)

The snoc of a level edge by a common last bit is a level edge.

theorem G0Fusion.lvlEdgeAt_restr {m n : ℕ} (h : canonicalLen m + 1 ≤ n) (x : ℕ → Bool) : LvlEdgeAt m n (restr n (prependWord (canonicalWord m ++ [false]) x)) (restr n (prependWord (canonicalWord m ++ [true]) x))

The level restrictions of an oriented GSGraph edge pair are level edges.

theorem G0Fusion.gsGraph_oriented {y z : ℕ → Bool} (h : GSGraph canonicalS y z) : ∃ (m : ℕ) (x : ℕ → Bool), y = prependWord (canonicalWord m ++ [false]) x ∧ z = prependWord (canonicalWord m ++ [true]) x ∨ y = prependWord (canonicalWord m ++ [true]) x ∧ z = prependWord (canonicalWord m ++ [false]) x

Every GSGraph canonicalS edge comes from a canonical word in one of the two orientations.

Witness words in Baire space

def G0Fusion.prepw (c : List ℕ) (w : ℕ → ℕ) : ℕ → ℕ

Prepend a finite ℕ-word to a point of Baire space.

Equations

• G0Fusion.prepw c w j = if j < c.length then c.getD j 0 else w (j - c.length)

theorem G0Fusion.prepw_apply_of_lt {c : List ℕ} {j : ℕ} (h : j < c.length) (w : ℕ → ℕ) : prepw c w j = c.getD j 0

theorem G0Fusion.prepw_apply_of_le {c : List ℕ} {j : ℕ} (h : c.length ≤ j) (w : ℕ → ℕ) : prepw c w j = w (j - c.length)

theorem G0Fusion.prepw_nil (w : ℕ → ℕ) : prepw [] w = w

theorem G0Fusion.continuous_prepw (c : List ℕ) : Continuous (prepw c)

theorem G0Fusion.prepw_append_head (c : List ℕ) (w : ℕ → ℕ) : (prepw (c ++ [w 0]) fun (j : ℕ) => w (j + 1)) = prepw c w

Splitting off the head of the tail extends the word.

theorem G0Fusion.getD_of_prefix {c d : List ℕ} (h : c <+: d) {j : ℕ} (hj : j < c.length) : d.getD j 0 = c.getD j 0

Witness-constraint sets

def G0Fusion.WitSet {α : Type u_1} {ι : Type u_2} (g : (ℕ → ℕ) → α × α) (u v : ι) (c : List ℕ) : Set (ι → α)

The set of assignments whose (u, v)-value pair is g-witnessed through the cylinder of the word c.

Equations

• G0Fusion.WitSet g u v c = {φ : ι → α | ∃ (w : ℕ → ℕ), g (G0Fusion.prepw c w) = (φ u, φ v)}

theorem G0Fusion.analyticSet_witSet {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {ι : Type u_2} [Countable ι] {g : (ℕ → ℕ) → α × α} (hg : Continuous g) (u v : ι) (c : List ℕ) : MeasureTheory.AnalyticSet (WitSet g u v c)

theorem G0Fusion.witSet_cover {α : Type u_1} {ι : Type u_2} {g : (ℕ → ℕ) → α × α} {u v : ι} {c : List ℕ} {Φ : Set (ι → α)} (hwit : ∀ φ ∈ Φ, φ ∈ WitSet g u v c) : Φ ⊆ ⋃ (k : ℕ), WitSet g u v (c ++ [k])

Witnessed families are covered by the one-step extensions of the witness word.

Pigeonhole over countable index types

theorem G0Fusion.exists_not_smallFam_inter' {α : Type u_1} [MeasurableSpace α] {G : Set (α × α)} {ι : Type u_2} {Φ : Set (ι → α)} (hΦ : ¬SmallFam G Φ) {κ : Type u_3} [Countable κ] [Nonempty κ] {Ψ : κ → Set (ι → α)} (hcov : Φ ⊆ ⋃ (c : κ), Ψ c) : ∃ (c : κ), ¬SmallFam G (Φ ∩ Ψ c)

Vertex shrinking

theorem G0Fusion.exists_smallOpens {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [Nonempty α] (n : ℕ) : ∃ (O : ℕ → Set α), (∀ (k : ℕ), MeasurableSet (O k)) ∧ (∀ (x : α), ∃ (k : ℕ), x ∈ O k) ∧ ∀ (k : ℕ), ∀ a ∈ O k, ∀ b ∈ O k, dist a b ≤ (1 / 2) ^ n

A countable cover of a separable metric space by measurable sets of diameter at most (1/2)^n.

theorem G0Fusion.exists_shrink {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [CompleteSpace α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {ι : Type u_2} [Finite ι] [Nonempty α] {Φ : Set (ι → α)} (hana : MeasureTheory.AnalyticSet Φ) (hpos : ¬SmallFam G Φ) (n : ℕ) : ∃ Φ' ⊆ Φ, MeasureTheory.AnalyticSet Φ' ∧ ¬SmallFam G Φ' ∧ ∀ φ ∈ Φ', ∀ φ' ∈ Φ', ∀ (u : ι), dist (φ u) (φ' u) ≤ (1 / 2) ^ n

Vertex shrinking: a positive analytic family can be refined to a positive analytic subfamily whose members are uniformly (1/2)^n-close at every vertex.

Witness extension fold

theorem G0Fusion.exists_extend_witnesses {α : Type u_1} [TopologicalSpace α] [PolishSpace α] [MeasurableSpace α] {ι : Type u_2} [Countable ι] [DecidableEq ι] {G : Set (α × α)} {g : (ℕ → ℕ) → α × α} (hg : Continuous g) (L : List (ι × ι)) (hnodup : L.Nodup) {Φ : Set (ι → α)} (hana : MeasureTheory.AnalyticSet Φ) (hpos : ¬SmallFam G Φ) (c₀ : ι × ι → List ℕ) (hwit : ∀ p ∈ L, ∀ φ ∈ Φ, φ ∈ WitSet g p.1 p.2 (c₀ p)) : ∃ (Φ' : Set (ι → α)) (c' : ι × ι → List ℕ), Φ' ⊆ Φ ∧ MeasureTheory.AnalyticSet Φ' ∧ ¬SmallFam G Φ' ∧ (∀ p ∈ L, c₀ p <+: c' p ∧ (c₀ p).length < (c' p).length ∧ ∀ φ ∈ Φ', φ ∈ WitSet g p.1 p.2 (c' p)) ∧ ∀ p ∉ L, c' p = c₀ p

Witness extension: given a positive analytic family whose tracked edge pairs are all witnessed at their current words, the family can be refined to a positive analytic subfamily with every tracked witness word properly extended.

The fusion recursion

def G0Fusion.combFun {α : Type u_1} (n : ℕ) (φ₀ φ₁ : (Fin n → Bool) → α) : (Fin (n + 1) → Bool) → α

The combination map: a pair of level-n assignments gives a level-(n + 1) assignment, sending each vertex to the value of the parent under the assignment selected by the last bit.

Equations

• G0Fusion.combFun n φ₀ φ₁ v = (if v (Fin.last n) = true then φ₁ else φ₀) (Fin.init v)

theorem G0Fusion.combFun_vals {α : Type u_1} (n : ℕ) (φ₀ φ₁ : (Fin n → Bool) → α) (v : Fin (n + 1) → Bool) : (∃ (i : Fin n → Bool), combFun n φ₀ φ₁ v = φ₀ i) ∨ ∃ (i : Fin n → Bool), combFun n φ₀ φ₁ v = φ₁ i

theorem G0Fusion.combFun_snoc {α : Type u_1} (n : ℕ) (φ₀ φ₁ : (Fin n → Bool) → α) (u : Fin n → Bool) (i : Bool) : combFun n φ₀ φ₁ (Fin.snoc u i) = (if i = true then φ₁ else φ₀) u

theorem G0Fusion.continuous_combFun {α : Type u_1} [MetricSpace α] (n : ℕ) : Continuous fun (p : ((Fin n → Bool) → α) × ((Fin n → Bool) → α)) => combFun n p.1 p.2

def G0Fusion.precw (n : ℕ) (cw : (Fin n → Bool) × (Fin n → Bool) → List ℕ) : (Fin (n + 1) → Bool) × (Fin (n + 1) → Bool) → List ℕ

The inherited witness words: a level-(n + 1) pair with agreeing last bits inherits the word of its parent pair; the fresh cross pair (differing last bits) starts at the empty word.

Equations

• G0Fusion.precw n cw p = if p.1 (Fin.last n) = p.2 (Fin.last n) then cw (Fin.init p.1, Fin.init p.2) else []

theorem G0Fusion.precw_of_last_eq {n : ℕ} {cw : (Fin n → Bool) × (Fin n → Bool) → List ℕ} {u v : Fin (n + 1) → Bool} (h : u (Fin.last n) = v (Fin.last n)) : precw n cw (u, v) = cw (Fin.init u, Fin.init v)

theorem G0Fusion.precw_of_last_ne {n : ℕ} {cw : (Fin n → Bool) × (Fin n → Bool) → List ℕ} {u v : Fin (n + 1) → Bool} (h : ¬u (Fin.last n) = v (Fin.last n)) : precw n cw (u, v) = []

theorem G0Fusion.precw_snoc {n : ℕ} (cw : (Fin n → Bool) × (Fin n → Bool) → List ℕ) (u v : Fin n → Bool) (i : Bool) : precw n cw (Fin.snoc u i, Fin.snoc v i) = cw (u, v)

structure G0Fusion.FusionStage {α : Type u_1} [MetricSpace α] [MeasurableSpace α] (G : Set (α × α)) (g : (ℕ → ℕ) → α × α) (n : ℕ) : Type u_1

A stage of the fusion construction: a positive analytic family of level-n assignments whose members are uniformly close at every vertex and uniformly g-witnessed through the tracked word at every level edge.

• fam : Set ((Fin n → Bool) → α)
• cw : (Fin n → Bool) × (Fin n → Bool) → List ℕ
• analytic : MeasureTheory.AnalyticSet self.fam
• positive : ¬SmallFam G self.fam
• close (φ : (Fin n → Bool) → α) : φ ∈ self.fam → ∀ φ' ∈ self.fam, ∀ (u : Fin n → Bool), dist (φ u) (φ' u) ≤ (1 / 2) ^ n
• witness (m : ℕ) (u v : Fin n → Bool) : LvlEdgeAt m n u v → ∀ φ ∈ self.fam, φ ∈ WitSet g u v (self.cw (u, v))
• wlen (m : ℕ) (u v : Fin n → Bool) : LvlEdgeAt m n u v → n ≤ canonicalLen m + 1 + (self.cw (u, v)).length

theorem G0Fusion.exists_fusionStage_zero {α : Type u_1} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {g : (ℕ → ℕ) → α × α} [Nonempty α] (hpos : ¬SmallFam G Set.univ) : Nonempty (FusionStage G g 0)

The base stage: the full family, shrunk once for the level-0 closeness control.

theorem G0Fusion.exists_fusionStage_succ {α : Type u_1} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {g : (ℕ → ℕ) → α × α} [Nonempty α] (hG : MeasureTheory.AnalyticSet G) (hg : Continuous g) (hrange : Set.range g = G) {n : ℕ} (S : FusionStage G g n) : ∃ (T : FusionStage G g (n + 1)), (∀ ψ ∈ T.fam, ∀ (v : Fin (n + 1) → Bool), ∃ φ ∈ S.fam, ψ v = φ (Fin.init v)) ∧ ∀ (m : ℕ) (u v : Fin n → Bool) (i : Bool), LvlEdgeAt m n u v → S.cw (u, v) <+: T.cw (Fin.snoc u i, Fin.snoc v i)

The one-step extension lemma: every fusion stage extends to the next level, with children's values among the parents' values and inherited witness words extending the parents' words. Combination (not_smallFam_comb_cross at fresh cross levels, not_smallFam_comb_pairs otherwise), then the witness-extension fold, then vertex shrinking.

noncomputable def G0Fusion.fusionTower {α : Type u_1} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] (G : Set (α × α)) (g : (ℕ → ℕ) → α × α) [Nonempty α] (hG : MeasureTheory.AnalyticSet G) (hg : Continuous g) (hrange : Set.range g = G) (hpos : ¬SmallFam G Set.univ) (n : ℕ) : FusionStage G g n

The tower of fusion stages.

Equations

• G0Fusion.fusionTower G g hG hg hrange hpos 0 = ⋯.some
• G0Fusion.fusionTower G g hG hg hrange hpos n.succ = ⋯.choose

theorem G0Fusion.fusionTower_spec {α : Type u_1} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {g : (ℕ → ℕ) → α × α} [Nonempty α] (hG : MeasureTheory.AnalyticSet G) (hg : Continuous g) (hrange : Set.range g = G) (hpos : ¬SmallFam G Set.univ) (n : ℕ) : (∀ ψ ∈ (fusionTower G g hG hg hrange hpos (n + 1)).fam, ∀ (v : Fin (n + 1) → Bool), ∃ φ ∈ (fusionTower G g hG hg hrange hpos n).fam, ψ v = φ (Fin.init v)) ∧ ∀ (m : ℕ) (u v : Fin n → Bool) (i : Bool), LvlEdgeAt m n u v → (fusionTower G g hG hg hrange hpos n).cw (u, v) <+: (fusionTower G g hG hg hrange hpos (n + 1)).cw (Fin.snoc u i, Fin.snoc v i)

theorem G0Fusion.exists_gsGraph_hom {α : Type u_1} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] {G : Set (α × α)} {g : (ℕ → ℕ) → α × α} [Nonempty α] (hG : MeasureTheory.AnalyticSet G) (hg : Continuous g) (hrange : Set.range g = G) (hpos : ¬SmallFam G Set.univ) (hsymm : ∀ (a b : α), (a, b) ∈ G → (b, a) ∈ G) : ∃ (φ : (ℕ → Bool) → α), Continuous φ ∧ ∀ (y z : ℕ → Bool), GSGraph canonicalS y z → (φ y, φ z) ∈ G

The fusion limit: a continuous map of Cantor space all of whose GSGraph canonicalS edge pairs land in G.