Supercompact preparation interface

Fixed-formula forcing, including class grounds. For a nonempty set preorder P with a top, write p<=q for stronger conditions. Give P the topology of downward-closed sets, and write r(U)=int(cl(U)) for an open U. The regular opens form a complete Boolean algebra: the join is r(union U_i), the meet is int(intersection U_i), and complement is int(P minus U). Here r is monotone and idempotent on opens; r(U intersect V)=r(U) intersect r(V), since two relatively dense open subsets of an open set have dense intersection. This identity also gives A intersect r(union U_i)=r(union(A intersect U_i)) for regular open A; hence finite meets distribute over arbitrary joins. Complement has meet empty and join P because U together with int(P minus U) is dense. These formulas prove all Boolean laws and the stated arbitrary bounds. The nonempty regular open e(p)=r(downarrow p) consists precisely of q such that every extension of q is compatible with p. Thus e(p) intersect e(q) is nonempty iff p,q have a common extension: from an element of the intersection first extend with p, then with q. If U is nonempty regular open, any p in U has nonzero e(p) contained in U. This proves dense completion directly, without importing an unbuilt regular-open-completion theorem. Its separative quotient identifies exactly the p,q with e(p)=e(q).

Translate P-names to Boolean names by recursively replacing p by e(p). Translate back by replacing a Boolean coefficient b by every p with e(p)<=b and recursively translating its subname. Both operations are set recursions on each name's descendant cone. A P-generic filter induces the Boolean filter generated by its e-images, and conversely a Boolean generic induces {p:e(p) is selected}. These correspond: the dense set of extensions below q or incompatible with q forces the original generic to contain q whenever an e-image in its generated filter lies below e(q). Density of e proves the same correspondence for every ground dense set. Induction on name rank now identifies the valuations of translated names, since b is selected precisely when some e(p)<=b is selected. The same argument applies to any dense inclusion and proves equality of the generic extensions up to these name translations. We continue to use the original conditions of P when discussing directed closure; no claim that its Boolean completion is itself directed closed is made.

For each fixed membership formula phi define p forces phi(tau) iff e(p)<=||phi(tau)||, using the translated names and the recursive values in F5. This is one defining formula for each fixed phi. Atomic equality is an equivalence in Boolean value, and substitution obeys ||s=t|| meet ||phi(s)|| <= ||phi(t)||: simultaneous induction on the sorted pair of name ranks proves it for membership/equality, by distributing a fixed meet over the defining joins and using the two inclusion clauses for equality; the finite formula induction gives negation, conjunction and the attained-value quantifiers. Consequently the usual first-order logical rules are valid in Boolean value. A condition decides phi on a dense set, because one of e(p) meet ||phi|| and e(p) meet not ||phi|| has a nonzero part with a dense e-image. F6's atomic rank induction and subsequent formula induction prove truth: phi of the valuations holds iff some p in the generic forces phi. Only ground set-sized families are used in those inductions.

These same arguments hold for a definable transitive class ground N satisfying ZFC, interpreted formula by formula, including the ambient ground itself. To check this extension rather than assuming it, the atomic recursion still takes place on a SET of descendants of its finitely many supplied names, inside N. Each existential attained-value collection is a subset of the SET Boolean algebra, formed by Separation in N using the already fixed matrix formula; there is no set or satisfaction predicate for all of N. Ground-family genericity and the same atomic induction apply to these sets. At the existential truth step, membership in the internally defined attained-value set gives a name in N by its defining existential formula. On the extension side each fixed formula is interpreted with quantifiers over valuations of N-names as an external formula schema. No assertion that N is definable inside a later generic extension is used. Thus the set-model truth proof extends with exactly these set-sized operations.

For clarity, ZFC preservation also extends by explicit names, not by a blanket appeal to set-model preservation. The empty name, pairs of names with coefficient one, and flattening two membership coefficients by their meet give Empty Set, Pairing and Union. Check omega gives Infinity and correct ground ordinals; transitivity gives Extensionality and Foundation, and the name-rank bound excludes new ordinals. For Separation use coefficients b meet ||phi(u)|| on each pair (u,b) of the input name. For Power Set, let D be its set of subnames and d_u the join of its coefficients at u; the names {(u,d_u meet v_u):u in D}, for all ground vectors v in B^D, cover exactly every extension subset, by taking v_u=||u in sigma|| for any name sigma of such a subset. For Replacement collect, for each u in D and each attained matrix value b, a witness name w_(u,b). Least witness ranks first bound this SET-indexed collection by one rank, then AC chooses names in that rank; the coefficients d_u meet b name the image. Totality selects an attained coefficient by the ground-join truth clause, and uniqueness makes this exactly the image. Finally a ground well-order of D gives, by its name evaluations, an ordinal-indexed list covering the input set; selecting the least representative by the already established Separation and Replacement well-orders that set in the extension. Applying this to a union gives Choice. These are precisely the individual name constructions of F7 and require only sets of N, so prove every ZFC instance also for the class-ground schema.

Mixing and maximum principle. For a ground antichain A in the Boolean algebra and names tau_a, put tau={(u,b meet a):a in A and (u,b) in tau_a}. Induction in the atomic equality clauses gives a<=||tau=tau_a||: below a all other antichain terms are zero and the remaining coefficients agree. For b=||exists x phi(x)||, the nonzero elements below some attained ||phi(tau)|| are dense below b. AC gives a maximal antichain of them; least witness ranks and then AC select its SET family of witness names. Mixing them gives a name attaining the entire value b, by substitution and maximality; add a fixed empty-name choice on not b if desired. Thus if p forces an existential assertion there is one name witnessing it below p. The P-name version is obtained by restricting each chosen name's coefficients to all common extensions with its antichain condition and taking the union. This also proves that a name for an element of a supplied set-name may be replaced, on an antichain, by names occurring as its subnames. Repeated mixtures flatten to a single mixture, by distributing coefficients. This is a set collection with a power-set cardinal bound in the old conditions and subnames, not the class of all names.

Two-step forcing. If 1_P forces that qdot is a nonempty preorder with top, take conditions (p,sigma), where p forces that sigma belongs to the underlying set of qdot, and sigma is chosen from the SET of mixtures of subnames of that underlying-set name, including a name of its top. This membership condition is part of the condition set; it ensures reflexivity and makes every forced comparison a comparison of members. Define (p,sigma)<=(q,tau) iff p<=q and p forces sigma<=tau. Membership and the maximum principle just proved show this is a dense presentation of all possible named conditions. A generic filter determines G on P and H on qdot_G. For a named dense subset of qdot, the pairs forcing their second component into it are dense in Pqdot by the maximum principle; hence H meets it. Conversely, given G and a V[G]-generic H, every ground dense D in Pqdot yields in V[G] a dense set of evaluated second components with first component in G: below a named condition, the first components of its D-extensions form a dense set below the given prefix. Thus G*H meets D. Upward closure and directedness in both directions follow by refining the two prefixes and forcing the required second-coordinate comparison. These prove both directions of generic factorization.

Name translation for this factorization is explicit. A (P*qdot)-name becomes in V[G] the qdot_G-name obtained recursively by retaining entries whose first-coordinate condition belongs to G and evaluating their second-coordinate condition names; evaluate subnames by the same recursion. Conversely, for a P-name of a qdot-name, select its set of possible subname entries and coefficient names by antichains in P, using the preceding maximum principle, and replace each selected entry by its pair condition. Rank recursion on these names transposes the nesting. At each step the valuation condition is exactly 'the prefix is in G and its evaluated tail is in H', so induction proves equality of the two valuations. All ranks and antichain-name sets are bounded before taking unions. This proves dense-presentation and two-step name invariance, including for each definable transitive class ground, since each construction is a fixed set operation there. Denote the forcing, truth, axiom-preservation, mixing and two-step facts just proved by FT.

Local A: closed inner targets and forcing. Suppose N is a transitive inner target of W, with the same ordinals, chi infinite, and every W-function chi to N belongs to N. Every W-set of at most chi elements of N then belongs to N: enumerate it, pad the enumeration, use closure, and take the range. We first remove any need to speak of N[K] as a definable class INSIDE W[K]. For a set preorder S in N define there T_0=empty, T_(alpha+1)=P(T_alpha times S), with entries interpreted as subname/coefficient pairs, and take unions at limits. These are sets of S-names, monotone in alpha. For every N-generic K, the set of their valuations is exactly V_alpha of N[K]. Induct on alpha. Successor names evaluate to subsets of the previous level. Conversely for such a subset x choose one N-name sigma; the name {(u,p):u in T_alpha and p forces_N u in sigma} evaluates exactly to x by FT and the induction hypothesis. Limit stages are unions, and alpha zero is empty. The set-name dot T_alpha={(tau,1):tau in T_alpha} therefore names this level for every generic. No simultaneous selection from a class of names has occurred.

Suppose S is the SAME set preorder in N and W and has W-size at most chi. For a common W-generic K, take f in W[K] of domain chi with values in N[K], and choose a W-name for f. Its rank bound gives a ground ordinal alpha exceeding the ranks of every value. The preceding paragraph then puts every actual f(i) in the valuation of the fixed N-set-name dot T_alpha. This is a set-coded predicate, so FT in W gives p in K forcing that assertion. Below p, for each i<chi choose a maximal antichain deciding f(i) equal to the valuation of some tau in T_alpha. These decisions are dense by the membership truth clause and maximum principle. Each antichain has size at most |S|, so the table of chosen conditions, names and indices has W-size at most chi and consists of elements of N. It belongs to N by closure; also p belongs to N. In N mix the names on each antichain below p, and assign empty elsewhere, then form the name of their chi-sequence. Its valuation is f in the actual generic containing p. This proves (N[K])^chi intersect W[K] is contained in N[K], with every witness bounded in the ground set T_alpha before the antichain choices.

If instead R in N is internally <=chi-closed, it is externally <=chi-closed in W: every descending sequence of its conditions of length at most chi belongs to N by the assumed closure, so its N-lower bound works in W. The same rank-level argument bounds all possible N-names for the entries of an actual f in W[L]. Below the condition forcing that bounded assertion, recursively strengthen to decide one T_alpha-name for each entry. At limits and after all chi decisions take a lower bound using external closure. The sequence of decided names is a W-sequence in N, hence belongs to N, and its sequence name evaluates to f below that final condition. Such deciding lower bounds are dense below the original condition, so a generic meets them. Consequently (N[L])^chi intersect W[L] is contained in N[L], without a size bound on R. The argument works below a condition of R and when internal directed closure supplies the chain lower bounds.

The same descending decision recursion, now for a name of a function from chi to a fixed ground set, proves that <=chi-closed forcing adds no such functions. At each stage choose a ground value and take a lower bound after chi stages; such final conditions form a dense set. Padding treats shorter domains. Hence it adds no subsets of a ground set of cardinality at most chi. Here '<a-directed closed' means every NONEMPTY downward-directed set of fewer than a conditions has a lower bound; a descending chain is such a set. The empty construction uses the top. All closure and size assertions are computed in their specified model.

Local supplier B: the exact reverse-Easton iteration Fix the supplied Laver function ℓ:κ→V_κ. Define P_α and stage names Q_α by recursion for α≤κ. At a limit δ take the direct limit when δ is an inaccessible cardinal of the ground model and the inverse limit otherwise. Equivalently, conditions have support bounded below every ground-model inaccessible δ≤α; at an inaccessible terminal α their whole support is bounded in α. Trivial coordinates can be omitted. At a successor use the ordinary two-step order: (p,σ)≤(q,τ) iff p≤q and p forces σ≤τ. Conditions are coherent sequences of stage names with this order on every restriction.

A stage γ<κ is nontrivial only if all of the following hold:

γ is inaccessible in the ground model and ℓ``γ⊆V_γ; ℓ(γ) is a pair (qdot,η) with η an ordinal; qdot is a P_γ-name and 1 forces that it is a nonempty <γ-directed-closed preorder with a top.

Then Q_γ=qdot; otherwise use the one-point forcing. No enumeration of all forcing notions is involved. The ordinal η is a gap marker. Whenever stage γ is active and γ<δ≤η, stage δ cannot be active: the closure condition ℓ``δ⊆V_δ would require the pair containing η to have rank less than δ, which is impossible. The same argument applies in the image iteration.

Set/name convention. Successor conditions need only use a set of names representing members of Q_γ, closed under mixing over antichains of P_γ. Start with the subnames occurring in the name for the underlying set of qdot, include the top, and take antichain mixtures. Admit (p,sigma) only when p forces sigma to belong to that underlying set, as in step 1.7. FT's membership and maximum principles show that these names give a dense presentation of the full two-step preorder. Mixing can be written directly as the union of restrictions of those names to Boolean coefficients; repeated mixing flattens to a single mixture. The set of mixtures has cardinal bounded by a power set of the product of the old condition set and the name set. Use this specific presentation throughout the recursion, so no class of all names enters P_α.

By induction |P_α|<κ and all conditions/name codes have rank below κ for α<κ: stage data have rank below κ; fewer than κ earlier sets of size less than κ have total size less than κ by regularity, and products/power sets of such sets have size less than κ by strong inaccessibility. The rank bounds follow from the same regularity and the finite-rank operations on names. At κ the direct limit is the union of κ earlier presentations, hence |P_κ|≤κ and P_κ⊆V_κ. More locally, if δ is inaccessible and ℓ``δ⊆V_δ, the same induction below δ gives |P_α|<δ for α<δ and |P_δ|≤δ.

Factorization, including names. The cuts needed here have a prefix of density at most a, all potentially nontrivial tail coordinates at least a, and all inaccessible support limits strictly above a still regular in the prefix extension. They include a closure-point cut α with a=α, and the cut after the anticipated stage κ with a=χ and a trivial gap through χ. Restriction is the first-coordinate projection. In a prefix extension recursively translate a name by replacing each coefficient condition with its tail when its prefix belongs to the generic, and omitting it otherwise; translate its subnames by the same rank recursion. Evaluation by a tail generic then equals evaluation of the original name by the combined generic, by induction on name rank. Successor-stage order assertions transfer by FT, giving the two-step order recursively.

Conversely let a prefix name be forced to be a tail condition. For each potentially occurring coordinate choose a name for its value, using the top when that coordinate is absent. At each ground inaccessible support limit δ>a, an antichain of at most a prefix conditions decides a bound below δ for that tail support. Regularity of δ bounds the union of these at most a possible bounds strictly below δ. Thus the set of all coordinates which can possibly occur is itself bounded below every such δ. At support limits at or below a there are no tail coordinates. This is the missing uniform support check: mixing possible coordinate values on prefix antichains cannot violate the support rule. At an inaccessible terminal stage use the same argument for its whole support. Recursively transpose the coordinate names from prefix-plus-earlier-tail names into full earlier-stage names; the rank recursion just described and the ordinary two-step name translation give this transposition at each successor. At limit stages the now-verified support bounds permit their assembly, with all coherent restrictions retained at inverse limits. The result is a full condition below the original prefix whose translated tail is the prescribed one. This proves the dense factorization at precisely the cuts used below. Its construction is definable from the iteration data, so elementarity carries it to j(P). Generic concatenation is interpreted through this dense equivalence, not as literal equality of arbitrary name encodings.

Tail closure. In a prefix extension in which every ground inaccessible δ above a cut a remains regular, a tail beginning at a whose stages are forced <γ-directed closed is <a-directed closed. Given a directed family D of size μ<a, union its supports. At each inaccessible δ>a, the union is bounded because δ is regular and μ<δ. At an inaccessible terminal stage the same reasoning applies. Construct a lower bound coordinate by coordinate. Having a common stronger prefix, the names for the D-coordinate values form a directed family in the forced stage order: for every two original conditions a third condition of D is below both, and the common prefix forces its coordinate to be a common stronger value. Stage directed closure gives a lower-bound name by FT. At limit coordinates use the permitted union support. The recursion therefore produces a condition below all of D. If there are no nontrivial stages at or below χ and the ground inaccessible support limits above χ remain regular, this argument works for |D|≤χ and gives ≤χ-directed closure. This proof uses directedness, not just pairwise compatibility.

In the applications the regularity premise is automatic: the prefix forcing has size at most a (or at most χ), hence preserves regular cardinals strictly above that bound. To verify this small-forcing fact, a name for a cofinal function from τ<δ into a regular δ has at each coordinate at most |S| possible ordinal values, by choosing an antichain deciding it. The union of τ·|S|<δ possible values is bounded. Thus no such cofinal function is added.

Local supplier C: κ remains an inaccessible cardinal after P_κ First P_κ is κ-cc. Take a hypothetical sequence of κ pairwise incompatible conditions p_α. A normal measure on κ concentrates on the inaccessible ordinals: derive it from a κ-closed supercompactness embedding; its target sees κ inaccessible, since it has the same small subsets/cardinal computations. For each inaccessible α, the direct-limit support condition makes supp(p_α)∩α bounded below α. Normality makes such a bound constant, say β, on a measure-one set. Since |P_β|<κ, κ-completeness makes p_α|α constant on a further measure-one set (a partition into fewer than κ pieces has a measure-one piece). Pick α<α' there with supp(p_α)⊂α'. Then p_α and p_α' agree on their common initial part, and the tail of p_α' above α' can be appended to p_α. Strengthening a prefix preserves every later name-order assertion, so this is a common extension. Contradiction.

A κ-cc forcing preserves regularity of κ: a name for a cofinal function τ→κ, τ<κ, has fewer than κ possible values at each coordinate, and regularity bounds their union. It also cannot identify κ with a smaller ordinal, since such a bijection would yield a cofinal map.

To verify the strong-limit clause, fix ξ<κ. If the nontrivial stages are bounded, the preparation is equivalent to a forcing of size less than κ, and its subset names for ξ have number less than κ by strong inaccessibility. Otherwise choose an active stage a>ξ. Its prefix has size at most a by supplier B, hence it adds at most (2^{a·ξ})^V<κ subsets of ξ. The tail starting at a is <a-directed closed: the prefix has size at most a and preserves every inaccessible support limit above a. Thus it adds no further subsets of ξ. Together with κ-cc and the old cardinal bound below κ, this proves 2^ξ<κ in the extension.

The same bounded-stage/unbounded-stage argument shows that any inaccessible closure point δ of ℓ remains inaccessible through P_δ: in the unbounded case use an active a between the length of a putative short cofinal map and δ. The small prefix cannot add such a cofinal map into the ground regular δ; the tail adds no sequences of that length. In the bounded case the whole prefix is small. For power sets use the identical cut argument. This local verification makes the stage test <γ-directed closure genuinely a regular-cardinal test at every active γ; it does not assume that every inaccessible below κ is Mahlo or that every P_γ is γ-cc.

Local supplier D: lifting an embedding through set forcing Let j:W→M be an elementary embedding with the existing definable-class/set-restriction convention. Let G⊆P be W-generic and K⊆j(P) be M-generic in a common outer universe, with j``G⊆K. Define

j*(val_G(τ)) = val_K(j(τ)).

If val_G(τ)=val_G(σ), FT supplies p∈G forcing τ=σ. Elementarity carries this to j(p) forcing j(τ)=j(σ), and j(p)∈K; hence the displayed definition is independent of the name. For any fixed formula φ and tuple of names, truth in W[G] gives a condition in G forcing φ, which transfers and gives truth in M[K]. Applying the same argument to ¬φ gives the converse. Thus j* is elementary formula by formula. Check names show it extends j. These are definable set operations on each bounded family of names; there is no uniform truth predicate or arbitrary class quantifier. Genericity of K is indispensable and is not inferred merely from containing j``G.

Local supplier E: master condition and bounded measure descent Suppose in W=V[G][H] the first lift j_0:V[G]→M[J] exists in a temporary outer extension, with J containing both G and H as the κ-stage factors. Suppose Q∈V[G] is <κ-directed closed, H⊆Q generic, and M[J] contains j_0H as a set of internal cardinality less than j(κ). Elementarity makes j_0(Q) internally <j(κ)-directed closed. Its subset j_0H is directed because H is a filter and j_0 preserves the order. Hence there is q* below every element of j_0H. Force over the current outer universe with the actual set preorder (j_0(Q))^{M[J]} below q*. Its generic K is M[J]-generic and contains j_0H after upward closure. Supplier D gives the second lift. This works for arbitrary Q; no unions-of-conditions or special Cohen presentation are assumed.

The set-membership premise has an explicit proof in the application. Choose a ground bound ν and a P-name for an enumeration e:ν→Q (allow repetitions). Its name belongs to M, and the old function j``ν belongs to M by closure. In M[J] both the original e and H are present, and j_0(e) is present by evaluation of j(e)'s name. Thus

{ j_0(e)(j(α)) : α<ν and e(α)∈H }

is exactly j_0``H and has an internal enumeration of length at most ν. This avoids treating j_0 itself as a set in its target.

For descent fix λ≥κ in W and let X=(P_κ(λ))^W. Suppose the temporary forcing after W is ≤χ-closed and W has |P(X)|≤χ. Derive

U = { A∈P(X)^W : j``λ ∈ j*(A) }.

The seed is in the target and has internal size at most λ<j(κ), by its old increasing enumeration, so it belongs to j*(X). Elementarity gives the ultrafilter laws and fineness. For a sequence of fewer than κ members of U, j fixes its index and the seed belongs to the intersection of their images, proving κ-completeness. For a selector f on a U-large subset of X with f(x)∈x, the value j*(f)(j``λ) is j(α) for some α<λ, so the corresponding constant fiber is U-large, proving normality. All these arguments concern W's sets and sequences. Finally U is a subset of the W-set P(X), whose size is at most χ; no-new-short-sequences from supplier A puts U in W. The temporary lift need not belong to W. The existence of U as a set in the outer extension is justified by the bounded-name construction in the final application below; it does not assume the ground class or the lifted embedding is definable there.

Preparation from the proved FT and local constructions Let P=P_κ as in B, and let G be generic. By C, κ remains inaccessible in V[G]. Take any further <κ-directed-closed set preorder Q in V[G] and its generic H. It suffices to prove λ-supercompactness for each ordinal λ≥κ: every cardinal in the final extension is an old ordinal. Add a top to Q and use a presentation with a fixed ordinal enumeration, without changing forcing equivalence.

Choose a P-name qdot and a condition p∈G forcing the required properties. To obtain a name forced correct by 1, mix qdot below the Boolean value of p with the one-point preorder on its complement. This agrees with Q in the actual extension containing p, is everywhere <κ-directed closed, and avoids an unjustified global forcing assertion about the originally chosen name. The same mixing supplies a total enumeration of its members from one sufficiently large ground ordinal, with repetitions and a top as fallback.

Choose an infinite ground cardinal ν≥κ,λ large enough for the transitive closures of these names and a dense presentation of P*qdot of size at most ν. Such a bound exists because these are sets; after an ordinal enumeration of Q's possible name values, conditions in a dense two-step presentation are pairs of a P-condition and an enumeration index. Set

μ=(2^ν)^V, θ=(2^μ)^V, χ=(θ^+)^V.

These are bounds chosen after Q's name and λ, before choosing the anticipation embedding. In W=V[G][H], all subsets of λ are evaluations of names coded by subsets of S×λ, with |S|≤ν, so there is an enumeration of P(λ)^W indexed by the ground ordinal μ. This follows by choosing antichains for the membership decisions; it does not assume the forcing has a smaller chain condition. Turn this into a surjection μ→X=(P_κ(λ))^W by retaining values of size less than κ and replacing other values by the empty set. Every subset of X is the image of its inverse image in μ. Subsets of μ in W in turn have names coded by subsets of S×μ, of which there are at most θ in V. Consequently W has |P(X)|≤θ<χ. The small forcing S preserves the regular cardinal χ. This explicit double-exponential bound includes subsets of the new P_κ(λ), not just old subsets of λ.

Apply the completed Laver theorem to the single target pair (qdot,χ), requesting χ-sequence closure. Obtain j:V→M with critical point κ, j(κ)>χ, M^χ∩V⊆M, and

j(ℓ)(κ)=(qdot,χ).

The initial κ stages of j(P) agree with P: j fixes the old stage data below κ, all their condition/name codes lie in V_κ, and the closure of M includes the relevant small subsets and cardinal computations. In particular the inaccessible/support tests below κ agree. At κ, M sees κ inaccessible and j(ℓ)``κ=ℓ⊆V_κ^M. It also sees that qdot is a P-name for <κ-directed-closed forcing. For this last assertion one can check downward absoluteness explicitly: a purported M-name for a <κ-sized directed family with no lower bound evaluates in a common V-generic extension to the same family in the same set Q, with the same order and the same possible lower bounds. That would contradict V's forced closure. Names for the underlying set, order, and ordinal enumeration belong to M by the chosen hereditary-size bound and χ-closure. Thus the stage-κ test succeeds.

The gap-marker argument makes every later stage at or below χ trivial. By B the image iteration therefore factors, up to its fixed dense name presentation, as

j(P) ≃ P * qdot * R,

where M[G][H] regards R as ≤χ-directed closed. The small prefix Pqdot has size at most ν<χ; it preserves regularity of all inaccessible support limits above χ, exactly the premise of B's tail-closure proof. For the common-small-forcing hypothesis of local A, use a ground name e:ν→qdot and the dense presentation S of pairs (p,α), with p∈P and α<ν; its order is defined by the Boolean value of the bounded comparison e(α)≤e(β). P and its full regular-open algebra are the same in M and V: their elements and subsets are present by χ-closure and |P|≤κ≤ν<χ. The atomic and bounded Boolean recursions on the common order/enumeration names are therefore identical. Thus S is the same set preorder in both models, of size at most ν. The common generic corresponds to GH by FT. Local A applies to this presentation, giving M[G][H] closure under χ-sequences in W and making R externally ≤χ-directed closed in W.

Temporarily force over W to add L⊆R. This is a specified set-forcing extension, not a claim that L already exists in W. The combined filter J=GHL is M-generic for j(P). Because every condition p of P has rank below κ, j(p)=p and its image in j(P) is its initial-segment inclusion, so j``G⊆J. Supplier D supplies

j_0:V[G]→M[J].

Supplier A's closed-forcing clause gives (M[J])^χ∩W[L]⊆M[J]. The enumeration argument in E puts j_0``H into M[J] with internal size at most ν<j(κ), and E supplies a master condition q* in j_0(Q).

In W[L], the actual set preorder (j_0(Q))^{M[J]} below q* is externally ≤χ-closed: any descending χ-sequence of its conditions belongs to M[J] by the just-proved closure, and internal <j(κ)-directed closure supplies a lower bound. Temporarily force below q* to obtain K. The two-step temporary forcing R*(j_0(Q) below q*) is ≤χ-closed, by the coordinate lower-bound argument in B (for two steps). Supplier D now gives

j*:W→M[J][K].

The old set jλ and its increasing enumeration remain in this target. Since κ remains a cardinal in W (C and the no-new-short-sequences property of Q), elementarity makes j(κ) a cardinal there, and the seed's enumeration length λ<j(κ) proves that the seed belongs to j*(X). To make the measure a SET before descent, choose in V an S-name xdot for X, and use the explicit power-set name construction from FT: there is a ground set T of names whose valuations cover exactly P(X)^W in the actual generic. Let Jhat denote the generic on j(S) obtained from J and K by the two-step name translation. The ground restriction j restricted to T is a set in V. In the outer extension form U={val_(G*H)(τ):τ∈T and jλ∈val_Jhat(j(τ))}. Replacement and Separation apply to the two supplied SETS T and j restricted to T and their generic valuations; no predicate for the ground universe, no definability of the full lifted class, and no class-choice principle is used. The lifting identities identify this set with the measure of local E, independently of duplicate names. That argument checks every ultrafilter, normality, fineness and short-family completeness clause on W sets. The previously proved |P(X)|≤θ<χ bound and <=χ-closed temporary forcing then put U in W. Hence W satisfies λ-supercompactness. This holds for every λ and every further <κ-directed-closed Q, of arbitrary set size. Taking Q trivial also proves that κ is supercompact already in V[G].

The construction P depends only on the ground Laver function. For each supplied P-generic G, every further directed-closed Q and every Q-generic H have been treated, with arbitrary final cardinal lambda. The measures descended above belong to V[G][H], so its own first-order supercompactness assertion holds; Q trivial gives supercompactness already in V[G]. The forcing and truth relations proved in FT express this as the fixed-formula forcing assertion that P prepares kappa. No choice of a single embedding or generic for all Q or lambda is required: each instance chooses its own set parameters, and every measure is formed from a bounded set of names. The zero-length iteration, omitted stages and one-point further forcing use their tops; all nonempty directed lower-bound and support arguments have explicitly stated cardinal bounds. This proves the exact semantic preparation target, keeping it separate from a formal Con transfer.