I believe that Neeman’s claim was in error. This preprint contains a kind of counterexample.

In correspondence with Neeman, I learned that 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.

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.