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

Edge bookkeeping

Witness words in Baire space

Witness-constraint sets

Pigeonhole over countable index types

Vertex shrinking

Witness extension fold

The fusion recursion

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.