It is well known that every Borel set has the property of Baire. That is, for every Borel set $B$, there is an open set $U$ and a sequence of dense open sets $D_n$ such that for every $x\in \cap_n D_n$, $x\in B \iff x \in U$.

Also well known: every Borel set can be represented by a Borel code, a well-founded tree whose leaves encode open sets and whose inner nodes designate how to combine them (intersect, union, complement).

Taking a computability-theoretic view, it looks like starting from a Borel code $X$ of height $\alpha$, it will take about $\alpha$-many jumps of $X$ to compute open codes for such sets $U$ and $\{D_n\}_{n\in\omega}$.

Do you know of a reference where this (or the analogous fact, if I missed any detail) is already proved?

Similarly, is there any paper which has already analyzed the reverse math strength of the statement ``Every Borel set has the Property of Baire''?