Thanks, that helps. But just to be clear, does imply the following statement?
If holds of in a #-generated outer model of which preserves then holds of in an inner model of .
I don’t see why it should.
The reason I ask is that for , the analogous statement (deleting #-generated) holds and is implied by .
Hugh, the HP is (primarily) a study of maximality criteria of the sort we have been discussing. As I have been trying to explain, it is essential to the programme to formulate, analyse, compare and synthesise different criteria, discovering their mathematical consequences. I referred to my formulation of the as “crude and uncut” as it may have to be modified later as we learn more. Changes in its formulation do not mean a defeat for the programme, but rather progress in our understanding of maximality.
So it makes no sense to assert that if a particular formulation of maximality coming out of the programme contradicts large cardinal existence then the programme is a failure and therefore irrelevant to the resolution of CH. Indeed the first HP criterion, the IMH, did contradict large cardinals, but it was later for compelling reasons synthesised with #-generation into the , which does not. It is not yet clear if the optimal maximality criterion will be compatible with large cardinal existence. It is certainly not the intention of the programme to take a stance on large cardinal existence “in advance” before seeing what maximality criteria are out there.