The analytic tree normal form (issue #10, Unit 0b)

The second half of the López–Escobar stop/go gate (audit v2, D3): every analytic subset of the structure space is the branch projection of a cylinder tree in (ℕ → Bool) × (ℕ → ℕ), through the query-code closed embedding —

c ∈ B ↔ ∃ g : ℕ → ℕ, ∀ n, (prefix (queryCode c) n, prefix g n) ∈ T n.

Mathlib's MeasureTheory.AnalyticSet is the continuous-image form (∅ or a continuous image of Baire space); the tree at level n is simply the set of length-n prefixes of graph points of the composed witness queryCode ∘ f, so the forward direction is the graph point itself and the converse chooses one graph point per prefix and passes to the coordinatewise limit: each coordinate is eventually fixed once the prefix length passes its index, so the chosen points converge to (queryCode c, g), continuity gives queryCode (f g) = queryCode c, and injectivity of the query code finishes. The empty analytic set is served by the branchless tree.

theorem FirstOrder.Language.exists_tree_of_analyticSet {L : Language} [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (hB : MeasureTheory.AnalyticSet B) : ∃ (T : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))), ∀ (c : L.StructureSpace), c ∈ B ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T n

The analytic tree normal form (audit v2, D3 — the stop/go gate): an analytic class of coded structures is the branch projection of a level-indexed cylinder tree along the query code.