Well-founded Borel evaluation codes

Fix a topological space $X$ and an enumerated basis $(U_n{)}_{n\in \mathbb{N}}$. Use the tree convention of Trees and their bodies and the Borel sigma-algebra of The countable Borel hierarchy and its limit convention. A Borel evaluation code is a nonempty tree $T\subseteq {\mathbb{N}}^{<\omega }$ with a label at each node, subject to the following rules:

• A node labelled $\mathrm{leaf}(n)$ has no children, with $n\in \mathbb{N}$.
• A node labelled $\mathrm{complement}$ has exactly the child $s^{⌢}0$.
• A node labelled $\mathrm{union}$ has any set of children $s^{⌢}k$ indexed by a subset of $\mathbb{N}$, including no children.

Require the immediate-child relation $tRs$ (meaning $t=s^{⌢}k\in T$ for some $k$) to be well-founded in the sense of Well-founded and setlike relations: every nonempty subset of $T$ has a member with no child in that subset. This is part of validity. Absence of a branch is not being substituted for it. The relation is setlike since its domain is a set.

The intended operations are a basis open at a leaf, complement relative to $X$, and union of child values. An empty union is intended to evaluate to $\mathrm{\varnothing }$, not to $X$. Existence and uniqueness of evaluation are a separate result. The empty underlying tree is invalid, whereas a one-node union code is valid: its child relation is empty and well-founded. A complement of that one-node union is also valid. All labelled trees under consideration form a set (labels are drawn from a fixed countable set), so no proper-class collection of codes is needed. No choice assumption occurs in this definition.