Analytic subsets of Baire space have tree projections

A basic neighbourhood of $(x,y)$ contains $N_{x\upharpoonright k}\times N_{y\upharpoonright l}$ for some $k,l$. Setting $n=\max (k,l)$ gives a contained product of equal-length cylinders. If $(x,y)\mathrm{\notin }[T]$, some paired prefix of length $n$ is absent; every point of that product cylinder has the same absent prefix. The complement of $[T]$ is therefore open, precisely as in the argument for F3.

Conversely, for closed $F\subseteq \mathcal{N}\times \mathcal{N}$, put $T=\{(x\upharpoonright n,y\upharpoonright n):(x,y)\in F,n\in \mathbb{N}\}$. Restrictions of witnessed pairs have the same witness, so $T$ is a synchronous tree and $F\subseteq [T]$. A point of $[T]\setminus F$ would have an equal-length product cylinder disjoint from $F$ by step 1.1's neighbourhood observation, but its paired prefix in $T$ supplies a point of $F$ in that cylinder. Thus $[T]=F$. For $F=\mathrm{\varnothing }$ the constructed tree is empty.

If $A$ is analytic, choose its one closed witness $F$ and apply step 2.1 to obtain $A=p[T]$. Conversely, if $A=p[T]$, step 1.1 makes $[T]$ a closed witness for analyticity. These choices concern one asserted witness and do not require AC.

For each fixed $x$, restricting a pair in $T$ proves prefix closure of $T_x$. For any $y$, the assertions $y\upharpoonright n\in T_x$ for all $n$ and $(x\upharpoonright n,y\upharpoonright n)\in T$ for all $n$ are identical. Existence of such $y$ is exactly $x\in p[T]=A$, proving the section equivalence. QED.