i added an answer and then realized it was a complete nonsense, i was getting at the following question.
Suppose kappa is a regular cardinal and every set in H_kappa has a sharp. Are there transitive models of ZFC, M and N, such that
- M and N have height kappa
- for some stationary in kappa set S, for every alpha in S, both M and N compute alpha^+ correctly,
- for some stationary set D, for every alpha in D, alpha is inaccessible in M
- N has no inaccessible cardinals.
i think the answer must be provably no. One can show that if the answer is yes then there is an inner model with a strong cardinal.
Assume M and N are as in the statement. Assume there is no inner model with a strong. Then clause 2 implies that K^M and K^N must coiterate (K is the core model). This means that K^N has stationary set of inaccessibles, so by Trevor's trick N must also have inaccessibles. So we must have covering fails in N which then implies that K^N doesn't exist.
I don't quite see how to get a Woodin. We need iterability to go upward, which is not obvious when there are Woodins.