Laver preparation versus PFA bookkeeping

Laver preparation and the standard forcing of PFA share one input but have different jobs. A Laver anticipation function $\mathrm{\ell }:\kappa \to V_{\kappa }$ can make a chosen set appear as $j(\mathrm{\ell })(\kappa )$ for a suitable supercompactness embedding. Its existence from a supercompact cardinal is the content of Existence of a Laver function at a supercompact, with the exact anticipation convention in Laver anticipation functions.

The Laver preparation uses that function in an iteration designed to make $\kappa$ indestructibly supercompact under subsequent $<\kappa$-directed-closed set forcing, exactly within the class stated by Supercompact preparation interface. Its conclusion does not cover arbitrary proper forcing.

The PFA bookkeeping iteration instead uses $\mathrm{\ell }$ to anticipate names for proper partial orders and places each valid guess into a countable-support iteration. The anticipated posets need not be directed closed. The final embedding argument uses $j(\mathrm{\ell })(\kappa )$ to expose the requested proper forcing as the next factor of $j(P_{\kappa })$; it does not appeal to prior indestructibility. Indeed, the PFA iteration deliberately collapses cardinals so that the former supercompact $\kappa$ becomes ${\omega }_2$, and therefore does not preserve its supercompactness.

Thus the preparation theorem is comparison material, not a load-bearing premise of the PFA proof. No implication saying that proper forcing preserves a supercompact cardinal is asserted. All existence statements above retain their ZFC and supercompact hypotheses; ambient AC is supplied by The Axiom of Choice, and this comparison makes no fresh selection.