Iterating Neeman's forcing In the paper, "Forcing with sequences of models of two types," (MR3201836), Neeman claims that, using a supercompact and a weakly compact above, one can force with his pure side conditions poset twice to obtain the tree property at $\omega_2$ and $\omega_3$.
Question 1: Are the details of this written up anywhere?
Question 2: Does the second stage add reals?  (For a fairly simple reason?)
 A: I believe that Neeman’s claim was in error.  This preprint contains a kind of counterexample.
Version 1 of the paper, available under the link on the arxiv, contains a detailed attempt to prove Neeman‘s claim based on my discussions with him.  After writing it all up, I thought about the argument again and started to worry that there were some gaps/circularities in the proof of the main technical lemma, Lemma 32, and a mistake in the argument for the tree property at $\kappa$ near the end.  (The copy of $\omega^{<\omega}$ I built isn’t dense.)  After struggling to correct it, I gave up and started thinking in the other direction.
His claim included an answer to question 2 in the negative; the second stage should not add reals. My counterexample is to the published claim conjoined with that unpublished subclaim.  But maybe a completely different argument from what Neeman told me may prove the original claim.  The question is, what is that “special argument” for preserving $\omega_1$?
I told Neeman about this work, and he said that a modification of the forcing that directly avoids my counterexample should work.  (A Laver function is incorporated to bound the ordertypes of Magidor models.)  He says he will write it up.
