I guess I need to weigh in here on your message to Steel.
You then advertise Hugh’s new axiom as having 3 properties:
- It implies core existence.
- It suggests a way of developing fine-structure theory for the core.
- It may be consistent with all large cardinals.
Surely there is something missing here! Look at my paper with Peter Holy: “A quasi-lower bound on the consistency strength of PFA, to appear, Transactions American Mathematical Society“. (I spoke about it at the 1st European Set Theory meeting in 2007.)
We use a “formidable” argument to show that condensation with acceptability is consistent with essentially all large cardinals. As we use a reverse Easton iteration the models we build are the “cores” in your sense of their own set-generic multiverses. And condensation plus acceptability is a big step towards a fine-structure theory. It isn’t hard to put all of this into an axiom so our work fulfills the description you have above of Hugh’s axiom.
The condensation principle that you force (local club condensation) actually does not hold in fine-structural models for the finite levels of supercompact which have been constructed (assuming the relevant iteration hypothesis). There are new fine-structural phenomena which happen in the long-extender fine structure models and which do not have precursors in the theory of short-extender models. (These models are generalizations of the short-extender models with Jensen indexing, the standard parameters are solid etc.)
At the same time these models do satisfy other key condensation principles such as strong condensation at all small cardinals (and well past the least weakly compact). I believe that it is still open whether strong condensation can be forced even at all the ’s by set forcing. V = Ultimate L implies strong condensation holds at small cardinals and well past the least inaccessible.
Finally the fine structure models also satisfy condensation principles at the least limit of Woodin cardinals which imply that the Unique Branch Hypothesis holds (for strongly closed iteration trees) below the least limit of Woodin cardinals. If this could be provably set forced (without appealing to the Conjecture) then that would be extremely interesting since it would probably yield a proof of a version of the Unique Branch Hypothesis which is sufficient for all of these inner model constructions.