The Posner-Robinson theorem states that, if $X$ is noncomputable, there is some $G$ such that $X\oplus G=G'$; that is, even though genuine jump inversion only works above $0'$, every (nontrivial) $X$ is "almost" the jump of something. There are a number of extensions and variations of the Posner-Robinson theorem; I'm interested in two, due to unpublished work of Hugh Woodin.
In multiple places - e.g. page 208 of "Proceedings of the 13th Asian Logic Conference" - we find the claim that Woodin proved the following higher-order analogues of the Posner-Robinson theorem:
If $X$ is not hyperarithmetic, then there is some $G$ such that $X\oplus G\equiv_T \mathcal{O}^G$.
(Assume $X^\#$ exists for every real $X$.) If $X$ is not constructible, then there is some $G$ such that $X\oplus G\equiv_T G^\#$.
My question is: are these proofs available anywhere?